Theory Introduction
chapter‹Context›
theory Introduction
imports HOLCF
begin
section‹Preface›
text‹
This is a formalization in Isabelle/HOL of the work of Hoare and Roscoe
on the denotational semantics of the Failure/Divergence Model of CSP.
It follows essentially the presentation of CSP in Roscoe's
Book "Theory and Practice of Concurrency" @{cite "roscoe:csp:1998" }
and the semantic details in a joint Paper of Roscoe and Brooks
"An improved failures model for communicating processes"
@{cite "brookes-roscoe85"}.
The original version of this formalization, called HOL-CSP 1.0
@{cite "tej.ea:corrected:1997"}, revealed minor, but omnipresent foundational errors
in key concepts like the process invariant. A correction was
proposed slightly before the apparition of Roscoe's book (all three authors were
in e-mail contact at that time).
›
text‹
In recent years, a team of authors undertook the task to port HOL-CSP 1.0
to modern Isabelle/HOL and structured proof techniques. This results in the
present version are called HOL-CSP 2.0.
The effort is motivated by the following assets of CSP:
▪ the theory is interesting in itself, and reworking its formal
structure might help to make it more widely accessible, given
that it is a particularly advanced example of the shallow embedding
technique using the denotational semantics of a language,
▪ it is interesting to ∗‹compare› the ancient, imperative, ML-heavy
proof style to the more recent declarative one in Isabelle/Isar;
this comparison (not presented here) gives a source of empirical
evidence that such proofs are more stable wrt. the constant
changes in the Isabelle itself,
▪ the ∗‹semantic› presentation of CSP lends itself to a semantically
clean and well-understood ∗‹combination› of specification languages,
which represents a major step to our longterm goal of heterogenuous,
yet semantically clean system specifications consisting of
different formalisms describing components or system aspects separately,
▪ the resulting HOL-CSP environment could one day be used as a tool that
certifies traces of other CSP model-checkers such as FDR4 or PAT.
›
text‹
In contrast to HOL-CSP 1.0, which came with
an own fixpoint theory partly inspired by previous work of Alberto Camilieri under
HOL4 @{cite"Camilleri91"}, it is the goal of the redesign of HOL-CSP 2.0 to reuse
the HOLCF theory that emmerged from Franz Regensburgers work and was substantially
extended by Brian Huffman. Thus, the footprint of the HOL-CSP 2.0
theory should be reduced drastically. Moreover, all proofs
have been heavily revised or re-constructed to reflect the
drastically improved state of the art of interactive
theory development with Isabelle. ›
section‹Introduction›
text‹DRAWN FROM THE PAPER @{cite "tej.ea:corrected:1997"}›
text‹
In his invited lecture at FME'96, C.A.R. Hoare presented his view on the status
quo of formal methods in industry. With respect to formal proof methods, he ruled
that they "are now sufficiently advanced that a [...] formal methodologist could
occasionally detect [...] obscure latent errors before they occur in practice"
and asked for their publication as a possible "milestone in the acceptance of formal
methods" in industry.
In this paper, we report of a larger verification effort as part of the UniForM project
@{cite "KriegBrueckner95"}. It revealed an obscure latent error that was not detected
within a decade. It cannot be said that the object of interest is a "large software
system" whose failure may "cost millions", but it is a well-known subject in the center
of academic interest considered foundational for several formal methods tools: the
theory of the failure- divergence model of CSP (@{cite "Hoare:1985:CSP:3921"},
@{cite "brookes-roscoe85"}). And indeed we hope that this work may further encourage the use
of formal proof methods at least in the academic community working on formal methods.
Implementations of proof support for a formal method can roughly be divided into two
categories. In direct tools like FDR @{cite "FDRTutorial2000"}, the logical rules of a
method (possibly integrated into complex proof techniques) are hard-wired into the code of
their implementation. Such tools tend to be difficult to modify and to formally reason
about, but can possess enviable automatic proof power in specific problem domains
and comfortable user interfaces.
The other category can be labelled as logical embeddings. Formal methods such as CSP
or Z can be logically embedded into an LCF-style tactical theorem prover such as HOL
@{cite "gordon.ea:hol:1993"} or Isabelle@{cite "nipkow.ea:isabelle:2002"}. Coming with
an open system design going back to Milner, these provers allow for user-programmed
extensions in a logically sound way. Their strength is flexibility, generality and
expressiveness that makes them to symbolic programming environments.
In this paper we present a tool of the latter category (as a step towards a future
combination with the former). After a brief introduction into the failure divergence
semantics in the traditional CSP-literature, we will discuss the revealed problems
and present a correction. Although the error is not "mathematically deep", it stings
since its correction affects many definitions. It is shown that the corrected CSP
still fulfils the desired algebraic laws. The addition of fixpoint-theory and
specialised tactics extends the embedding in Isabelle/HOL to a formally proven
consistent proof environment for CSP. Its use is demonstrated in a final example.
›
section‹An Outline of Failure-Divergence Semantics›
text‹
A very first approach to give denotational semantics to CSP is to view it as a kind
of a regular expression. This way, it can be understood as an automata and the
denotations are just the language of the automaton; this way, synchronization
and concurrency can be basically understood as the construction of a product automaton
with potential interleaving. The semantics becomes compositional, and internal communication
between sub-components of a component can be modeled by the concealment operator.
Hoares work @{cite "Hoare:1985:CSP:3921"} was strongly inspired by this initial idea.
However, it became quickly clear that the simplistic automata vision is not a satisfying
paradigm for all aspects of concurrency. Particularly regarding the nature of communication,
where one "sends" actively information and the other "receives" it, the bi-directional
product construction seems to be misleading. Furthermore, it is an obvious difference
if a group of processes remains in a passive deadlock because all possible communications
contradict each other, or if a group of processes is too busy with internal chatter and
never reaches the point where this component is again ready for communication.
Hoare solved these apparent problems by presenting a multi-layer approach, in which the
denotational models were refined more and more allowing to distinguish the above
critical situations. An ingenious concept in the overall scheme is to distinguish
∗‹non-deterministic› choice from ∗‹deterministic› one ⁋‹which in itself produces
problems with recursion which had to be overcome by some restrictions on its use.› in order to
solve the sender/receiver problem.
Hoare proposed 3 denotational semantics for CSP:
▪ the ∗‹trace› model, which is basically the above naive automata model not allowing
to distinguish non-deterministic choice from deterministic one, neither to distinguish deadlock
from infinite internal chatter,
▪ the ∗‹failure› model is able to distinguish non-deterministic choice from deterministic one by
different maximum refusal sets, which is however cannot differentiate deadlock from infinite
internal chatter,
▪ the ∗‹failure-divergence› model overcomes additionally the unresolved problem of failure model.
In the sequel, we explain these two problems in more detail, giving some
motivation for the daunting complexity of the latter model.
It is this complexity which finally raises general interest in a
formal verification.
›
subsection‹Non-Determinism›
consts dummyPrefix :: "'a::cpo ⇒ 'b::cpo ⇒ 'b::cpo"
consts dummyDet :: "'a::cpo ⇒ 'b::cpo ⇒ 'b::cpo"
consts dummyNDet :: "'a::cpo ⇒ 'b::cpo ⇒ 'b::cpo"
consts dummyHide :: "'b::cpo ⇒ 'a ⇒ 'b::cpo"
notation dummyPrefix (infixr "→" 50)
notation dummyDet (infixr "□" 50)
notation dummyNDet (infixr "⊓" 50)
notation dummyHide (infixr "∖" 50)
text‹
Let a and b be any two events in some set of events @{term "Σ"}. The two processes
➧ @{term "(a → Stop) □ (b → Stop)"} \hspace{7cm} (1)
and
➧ @{term "(a → Stop) ⊓ (b → Stop)"} \hspace{7cm} (2)
›
text‹
cannot be distinguished under the trace semantics, in which both processes
are capable of performing the same sequences of events, i.e. both have the
same set of traces @{term "{{},{a},{b}}"}. This is because both processes can either
engage in @{term "a"} and then @{term "Stop"}, or engage in @{term "b"} and
then @{term "Stop"}. We would, however, like to distinguish between @{term "a"}
∗‹deterministic› choice of @{term "a"} or @{term "b"} (1) and @{term "a"}
∗‹non-deterministic› choice of @{term "a"} or @{term "b"} (2).
This can be done by considering the events that a process can refuse to engage
in when these events are offered by the environment; it cannot refuse either,
so we say its maximal refusal set is the set containing all elements of @{term "Σ"} other
than @{term "a"} and @{term "b"}, written @{term "Σ-{a,b}"}, i.e. it can
refuse all elements in @{term "Σ"} other than @{term "a"} or @{term "b"}. In the case
of the non-deterministic process (2), however, we wish to express that if the environment
offers the event @{term "a"} say, the process non-deterministically chooses either to engage in
@{term "a"}, to refuse it and engage in @{term "b"} (likewise for @{term "b"}). We say
therefore, that process (2) has two maximal refusal sets, @{term "Σ-{a}"} and
@{term "Σ-{b}"}, because it can refuse to engage in either @{term "a"} or
@{term "b"}, but not both. The notion of refusal sets is in this way used to distinguish
non-determinism from determinism in choices.
›
subsection‹Infinite Chatter›
text‹
Consider the infinite process @{term "μ X. a → X"}
which performs an infinite stream of @{term "a"}'s. If one now conceals the event a in
this process by writing
➧ @{term "(μ X. a → X) ∖ a"} \hspace{7.8cm} (3)
›
text‹
it no longer becomes possible to distinguish the behaviour of this process
from that of the deadlock process Stop. We would like to be able to make such
a distinction, since the former process has clearly not stopped but is engaging
in an unbounded sequence of internal actions invisible to the environment. We say
the process has diverged, and introduce the notion of a divergence set to denote
all sequences events that can cause a process to diverge. Hence, the process Stop
is assigned the divergence set @{term "{}"}, since it can not diverge, whereas the process
(3) above diverges on any sequence of events since the process begins to diverge
immediately, i.e. its divergence set is @{term "Σ⇧*"} , where @{term "Σ⇧*"} denotes the
set of all sequences with elements in @{term "Σ"}. Divergence is undesirable and so
it is essential to be able to express it to ensure that it is avoided.
›
subsection‹The Global Architecture of HOL-CSP 2.0›
text‹
The global architecture of HOL-CSP 2.0 has been substantially simplified compared
to HOL-CSP 1.0: the fixpoint reasoning is now entirely based on HOLCF (which meant that
the continuity proofs for CSP operators had basically been re-done).›
text‹
The theory ▩‹Process› establishes the basic common notions for events, traces, ticks and
tickfree-ness, the type definitions for failures and divergences as well as the
global constraints on them (called the "axioms" in Hoare's Book.) captured in a
predicate ▩‹is_process›. On this basis, the set of failures and divergences satisfying
▩‹is_process› is turned into the type ▩‹'a process› via a type-definition
(making ▩‹is_process› as the central data invariant). In the sequel, it is shown that
▩‹'a process› belongs to the type-class @{class "cpo"} stemming from @{theory HOLCF} which
makes the concepts of complete partial order, continuity, fixpoint-induction and general
recursion available to all expressions of type ▩‹'a process›. ›
text‹
The theory ▩‹Process› also establishes the two partial orderings @{term "P ≤ P'"} for
refinements and @{term "P ⊑ P'"} for the approximation on processes used to give semantics
to recursion. The latter is well-known to be logically weaker than the former.
Note that, unfortunately, the use of these two symbols in HOL-CSP 2.0, where the
latter is already used in the @{theory HOLCF}-theory, is just the other way round as
in the literature. ›
text‹
Each CSP operator is described in an own theory which comprises:
▪ The denotational core definition in terms of a pair of Failures and Divergences
▪ The establishment of ▩‹is_process› for the Failures and Divergences in the
range of the given operator (thus, the invariance of ▩‹is_process› for this operator)
▪ The proof of the projections ▩‹T› and ▩‹F› and ▩‹D› for this operator
▪ The proof of continuity of the operator (which is always possible except for
hide if applied to infinite hide-sets).›
text‹
Finally, the theory CSP contains the "Laws" of CSP, i.e. the derived rules
allowing abstractly to reason over CSP processes. The overall dependency graph
is shown in \autoref{fig:fig1}.›
text‹
\begin{figure}[ht]
\centering
\includegraphics[width=0.9\textwidth]{session_graph}
\caption{The HOL-CSP 2.0 Theory Graph}
\label{fig:fig1}
\end{figure}›
no_notation dummyPrefix (infixr "→" 50)
no_notation dummyDet (infixr "□" 50)
no_notation dummyNDet (infixr "⊓" 50)
no_notation dummyHide (infixr "∖" 50)
end