Some CSP Proof Techniques Applied to Virtual Channel Protocols

D.B. Carpenter

Department of Electronics and Computer Science, Southampton University, Southampton, S09 5NH

November 18, 1994

1 Models and Simulations: I. Simple and Extended Transition Systems

State transition models are very often used to give operational semantics to concurrent systems. Here transition models will be assume a less fundamental role—they simply encode particular CSP processes in a convenient way. The main advantage of a transition model representation is that it makes available the powerful technique of simulation (and bisimulation) for establishing relationships and equivalences between processes. A simulation is a binary relation between the state-spaces of two transition models, which has some commutative relationship with the transition behaviour of the models.

There is a great deal of freedom in the definition of state transition models, especially for encoding non-deterministic processes. From our viewpoint, all that really matters is that useful simulation results should exist between the types of model chosen. Three (???) different types of model will be considered here.

Simple Transition Models (TMs) are represented by a tuple (S, A, T) where S is a state space, A is an alphabet of events, and T is a transition function. T is a tertiary relation from S × A × S with the property

((i, e, i′) ∈ T ∧ (i, e, i′′) ∈ T) ⇒ i′ = i′′.

Usually T will regarded as a function from S to the space of partial functions from A to S. So T (i) denotes such a partial function—evidently (e ↦ i′) ∈ T (i) means that the system can move from state i to state i′ through occurence of event e.

Extended Transition Models (ETMs) are a generalisation of TMs which include unlabelled arcs. They are represented by a tuple (S, A, T, U). S, A and T have the same role as for a TM, whereas U is a binary relation on S. U will be treated as a function from S to Pow S. U(i) is a set of states to which i can move without engaging in any external event.

Acceptance Transition Models (ATMs) are a second generalisation of TMs, which introduce non-determinism in a different way. Represented by the tuple (S, A, T, W), S, A and T again follow their definitions for a TM. W is a function from S to Pow Pow A with the property

⋃_{w∈W (i)} w = dom T (i).

Informally, when an ATM is in state i, it has an associated hidden variable whose value is some element w of W (i). If the environment offers to engage in some event e from w, the ATM will accept that event and undergo the transition defined by i′ = T (i)(e) (and choose a new hidden value from W (i′)). But if the environment only offers events outside w, the ATM refuses these events, even if they are in dom T (i).

The semantics of these models, and their properties, will be discussed more fully in the following subsections. Before that, I’ll try to motivate working with such a variety of different types of model.

TMs are good for representing deterministic processes, or for representing prefix-closed sets of traces. Deterministic processes represented as TMs can be composed in parallel in a straightforward way to build new TMs; conversely a deterministic process will often factorise cleanly into two or more parallel deterministic processes. Equivalences between the trace-sets represented by two TMs can be established through a particularly simple type of simulation. For such reasons it seems wise to work with TMs whenever they suffice.

At some stage, however, an abstraction step is needed, where some internal events are concealed. This is where an ETM is needed. A TM yields an ETM in a very straightforward way upon concealment of some subset of its alphabet. Unfortunately, ETMs aren’t particularly easy to manipulate. Also, it isn’t very easy to show what specifications they satisfy. For example, their traces aren’t encoded in a simple way.

On the other hand, ATMs are relatively easy to work with—we will give simple rules for establishing that they satisfy certain specifications. In later subsections we give a simulation result which can be used for establishing that a process represented by an ETM implements a process represented by an ATM.

Notice, by the way, that the transition function, T, for both an ETM and an STM satisfies the same restriction as that for for a TM—one way in which non-determinism won’t be introduced here is by allowing more than one arc with the same event labelling to emerge from a state.

1.1 Simple Transition Models

A TM can be viewed as a device for encoding a prefix-closed set of traces: T , say. We have

T ⊂ A^{∗} ∧ ((s < s′ ∧ s′ ∈ T ) ⇒ s ∈ T ).

Suppose S is a function from T to some state space S. Define

S^{−1}(i) = \{\underline{s} | S(\underline{s}) = i\}

and

T (i) = \{(\underline{e}, \underline{j}) | ∃s : S^{−1}(i). sˆ ⟨\underline{e}⟩ ∈ S^{−1}(\underline{j})\}.  (1)

Now (S, A, T) is a simple transition model of T iff

∀i. ∀(e, j) : T (i). ∀s : S^{−1}(i). sˆ ⟨e⟩ ∈ S^{−1}(j)  (2)

In terms of the transition model, S^{−1}(i) is the set of traces leading the system to state i. (e, j) ∈ T (i) means that the system can move from state i to state j by executing event e. The requirement 1 states that if the system can get to state i after some history, then move to state j by executing e next, then any history leading to state i also allows this. In particular, this implies that T (i) is a partial function. S(⟨⟩) is the initial state for the transition model which generates T .

1.1.1 Specifications

Suppose S is a partial function from A^{∗} to S satisfying

S(⟨⟩) = i,
(sˆ ⟨e⟩ ↦ j) ∈ S ⇔ s ∈ dom S ∧ (e ↦ j) ∈ T (S(s)),

then the (deterministic) process generated by (A, S, T) from initial state i satisfies

tr ∈ dom S.

1.1.2 Simulations

Suppose (S, A, T) and (S′, A, T′) are two TMs. Also, suppose there exists a relation R from S to S′ such that

i R i′ ⇒ (∀(e, j) : T (i). (∃j′. (e, j′) ∈ T′(i′) ∧ j R j′)).  (3)

Then R is a simulation, and if i R i′ the trace set generated by (S, A, T) from initial state i is a subset of the trace set generated by (S′, A, T′) from initial state i. If R^{−1} is also a simulation, then R is a bisimulation, and the two trace sets are equal.

1.1.3 Trace predicates, and composition

A set of traces can be regarded as a predicate on traces. A very common form of specification takes the form of the conjunction of a set of predicates, each applied to the process’s trace restricted to some sub-alphabet. Suppose we have a specification of the form

⋀_{n}((tr ⊳ A_{n}) ∈ T_{n})

and (S_{n}, A_{n}, T_{n}) is a TM generating T_{n} from initial state i_{n}. Then the specification above is equivalent to

(tr ⊳ (⋃_{n} A_{n})) ∈ T

where T is generated by the TM (S, A, T) with

A = ⋃_{n} A_{n}
S = S_{1} × S_{2} × …
T (i_{1}, i_{2}, …) = \{(\underline{e} ↦ (\underline{j_{1}}, \underline{j_{2}}, …)) | ⋀_{n} Accept (A_{n}, T_{n}, \underline{e}, i_{n}, \underline{j_{n}})\}

from initial state (i_{1}, i_{2}, …). Here

Accept (A, T, e, i, j) ⇔ (if (e ∈ A) then (e ↦ j) ∈ T (i) else j = i)

It may be helpful to present an explicit procedure for constructing T (i_{1}, i_{2}, …). This procedure may be used in cases where not too many systems are being composed. Note that very often the transition function is only needed on some subset of the composite state space.

Construct the set D = dom T_{1}(i_{1}) ∪ dom T_{2}(i_{2}) ∪ …
For each e ∈ D:

if there is any k ∈ {1, 2, …} such that e ∈ A_{k} but e ∉ dom T_{k}(i_{k})

this e isn’t in dom T (i_{1}, i_{2}, …).

Otherwise

for each k,

if e ∈ A_{k} set j_{k} to T_{k}(i_{k})(e), or
if e ∉ A_{k} set j_{k} to i_{k}.
Add (e ↦ (j_{1}, j_{2}, …)) to T (i_{1}, i_{2}, …).

1.1.4 Association with deterministic CSP processes

In CSP, a deterministic process is completely determined by its traces, so it can also be determined by a TM which generates those traces from some initial state. In fact, the set of deterministic CSP process (one for each initial state in S) defined in this way by (S, A, T) is given by the mutual recursion

μX : A. (e : dom T (i) → X(T (i)(e)))

With this interpretation, the composition operation in the previous section is just CSP parallel composition.

1.2 Extended Transition Models

An ETM is a tuple (S, A, T, U). T is defined in the same way as for a simple TM. U is a nilpotent binary relation over S. The term “nilpotent” is used here in a weak sense meaning

∀i : S. ∃n : Nat. Ũ^{n}{i} = ∅

where ŨX = ⋃_{i∈X} U(i). We associate a set of CSP processes with an ETM, one for each element of S (any of which can be chosen as initial state) by the recursion

μX : A. P (U(i), dom T (i), T (i))(X)  (4)

where

P (u, v, t)(X) = \{ \begin{matrix}R(v, t)(X), & u = ∅ \\ Q(u)(X) ⊓ (Q(u)(X) □ R(v, t)(X)), & otherwise \end{matrix}
Q(u)(X) = \begin{matrix}⊓ \\ j ∈ u \end{matrix} X(j)
R(v, t)(X) = (e : v → X(t(e)))

This definition has been chosen specifically to ensure that concealment of events has a simple representation. The nilpotency of U ensures that the processes defined in 4 are divergence-free. Note that a simple TM, interpreted as a model for a deterministic process, is recovered by setting U = ∅.

1.2.1 Concealment

The semantics of the ETM is chosen to facilitate concealement. If Proc is the set of processes associated with an ETM (S, A, T, U), and

Proc′(i) = Proc (i) \ C

for some C ⊂ A, then (S, A, T′, U′) is an ETM for the system Proc′, where

T′(i) = (A − C) ⊲ T (i)
U′(i) = U(i) ∪ ran (C ⊲ T (i)).

1.2.2 Simulations

In this section we introduce a simulation relation wherebye the deterministic process associated with some simple TM can implement the process associated with some ETM. Of course, this is only possible if the latter system of processes is also deterministic (although this may not be obvious in the ETM representation). Suppose (S, A, T, U) is an ETM and (S′, A, T′) is a simple TM. The relation G from S to S′ is a simulation if

i G i′ ⇒ ((dom T (i) ⊂ dom T′(i′)) ∧
(∀e : dom T (i). T (i)(e) G T′(i′)(e)) ∧
(∀j : U(i). j G i′) ∧
(U(i) = ∅ ⇒ dom T (i) = dom T′(i′))).

If G is a simulation, and i G i′, and Proc is the system of processes associated with the ETM, and Proc′ is the set of process associated with the TM, then

Proc (i) ⊒ Proc′(i′)  (5)

This kind of simulation isn’t a direct generalisation of the traces-model simulation in section ??. The inequality here refers to the full refusals model. In fact, since Proc′ is deterministic, this inequality implies also equality (because deterministic processes are maximal in the refusals model), so in the special case U = ∅, this simulation is as strong as the previous bisimulation.

2 Channel Multiplexer Example

This section describes an application of the results of section 1, up to an including the results in 1.2. The application is to a system of communication channels. Each channel alternates transmission of forward and backward messages; it repeatedly accepts a forward message through an event label p, delivers it through an event labelled q, accepts a backward message through an event labelled r and delivers it through an event labelled s. In CSP the individual channel process can be written as

CHAN = μX. _{x}p.x → q.x → _{y}r.y → s.y → X

Sometimes the return message may be simply an acknowledgement, leading to an implementation of synchronous unidirectional channels. Often many logical channels have to be multiplexed over a single bidirectional line. We assume the availability of a line in each direction, each with an associated output queuing mechanism whose details are abstracted by regarding queue plus communication line as a FIFO. Messages accepted by the FIFO are labelled with the associated channel and the direction of the FIFO (f or b for forward and backward lines), superfixed with O or I according to whether the event is an output to the FIFO or and input from the FIFO.

FIFO (C, f, q) = ( _{c∈C} _{x}c.f^{O}.x → FIFO (C, f, qˆ ⟨c.f^{I}.x⟩)) □
(if q ≠ ⟨⟩ then q_{0} → FIFO (C, f, q′) else STOP)

Here C is the set of channels recognised and q is the set of messages currently in the fifo—represented here, for brevity, as a sequence of pending input events (recollect that STOP is the unit of □, so when q is empty, outputs remain possible). For each channel we introduce in output buffer and an input buffer

OBUF = μX. _{x}p.x → f^{O}.x → _{y}b^{I}.y → s.y → X
IBUF = μX. _{x}f^{I}.x → q.x → _{y}r.y → b^{O}.y → X

The aim is to show that the system of buffers and FIFOs implements the set of channels:

(( \begin{matrix}∥ \\ c ∈ Chans \end{matrix} c : OBUF) ∥ FIFO (Chans, f, ⟨⟩) ∥
( \begin{matrix}∥ \\ c ∈ Chans \end{matrix} c : IBUF) ∥ FIFO (Chans, b, ⟨⟩)) \ H = \begin{matrix}∥ \\ c ∈ Chans \end{matrix} c : CHAN

where H is the set of internal events { .f^{O}. , .f^{I}. , .b^{O}. , .b^{I}. }.

2.1 Transition systems for buffers and FIFOs

First we write down simple TMs for the (deterministic) components of the system ^{1}. The channel processes and the buffers can be modelled on the same state space

S^{B} = α_{0} | α_{1} of Values | α_{2} | α_{3} of Values

where Values is the set of values that can be transmitted on a channel. The transition functions for output and input buffers are

T_{c}^{O}(α_{0}) = \{(c.p.\underline{x} ↦ α_{1}(\underline{x}))\}
T_{c}^{O}(α_{1}(x)) = {(c.f^{O}.x ↦ α_{2})}
T_{c}^{O}(α_{2}) = \{(c.b^{I}.\underline{x} ↦ α_{3}(\underline{x}))\}
T_{c}^{O}(α_{3}(x)) = {(c.s.x ↦ α_{0})}
T_{c}^{I}(α_{0}) = \{(c.f^{I}.\underline{x} ↦ α_{1}(\underline{x}))\}
T_{c}^{I}(α_{1}(x)) = {(c.q.x ↦ α_{2})}
T_{c}^{I}(α_{2}) = \{(c.r.\underline{x} ↦ α_{3}(\underline{x}))\}
T_{c}^{I}(α_{3}(x)) = {(c.b^{O}.x ↦ α_{0})}.

A fifo has state space S^{F} = CV^{∗}, where CV = Chans × Values, and transition function

T_{f}^{F} (m) = \{(\underline{c}.f^{O}.\underline{x} ↦ mˆ ⟨(\underline{c}, \underline{x})⟩),
(\underline{c}.f^{I}.\underline{x} ↦ m′ | m ≠ ⟨⟩ ∧ m_{0} = (\underline{c}, \underline{x}))\}

1In principle one should prove that these systems model the CSP processes introduced above. This could be done by using CSP proof rules to determine the trace sets, then defining a mapping from traces to the state spaces, as explained in section 1.1. Such a degree of formality, when the correspondence is obvious anyway, seems inappropriate here.

According to section 1.1.3, the complete system can be represented on a state space which is the product of all the component state spaces. Where several of the components are closely related, and indexed by elements of some set such as Chans, it is convenient to group the associated factors together in a function on the index space. So the composite state space can be taken as

S^{MUX} = (Chans → S^{B}) × S^{F} × (Chans → S^{B}) × S^{F}

where the four factors correspond to output buffers, forward fifo, input buffers and backward fifo respectively. According to the expression in 1.1.3, the transition function on this system is given by

T^{MUX}(O, m, I, n) =

\{ \begin{matrix}(\underline{c}.p.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, m, I, n)) & | O(\underline{c}) = α_{0}, \\ (\underline{c}.f^{O}.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{2})\}, mˆ ⟨(\underline{c}, \underline{x})⟩, I, n)) & | O(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.f^{I}.\underline{x} ↦ (O, m′, I ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, n)) & | m ≠ ⟨⟩ ∧ m_{0} = (\underline{c}, \underline{x}) ∧ I(\underline{c}) = α_{0}, \\ (\underline{c}.q.\underline{x} ↦ (O, m, I ⊕ \{(\underline{c} ↦ α_{2})\}, n)) & | I(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.r.\underline{x} ↦ (O, m, (I ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, n)) & | I(\underline{c}) = α_{2}, \\ (\underline{c}.b^{O}.\underline{x} ↦ (O, m, I ⊕ \{(\underline{c} ↦ α_{0})\}, nˆ ⟨(\underline{c}, \underline{x})⟩)) & | I(\underline{c}) = α_{3}(\underline{x}), \\ (\underline{c}.b^{I}.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, m, I, n′)) & | n ≠ ⟨⟩ ∧ n_{0} = (\underline{c}, \underline{x}) ∧ O(\underline{c}) = α_{2}, \\ (\underline{c}.s.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{0})\}, m, I, n)) & | O(\underline{c}) = α_{3}(\underline{x}) \} \end{matrix}

The initial state is ({( ↦ α_{0})}, ⟨⟩, {( ↦ α_{0})}, ⟨⟩). Concealing internal events gives

T^{MUX2}(O, m, I, n) =

\{ \begin{matrix}(\underline{c}.p.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, m, I, n)) & | O(\underline{c}) = α_{0}, \\ (\underline{c}.q.\underline{x} ↦ (O, m, I ⊕ \{(\underline{c} ↦ α_{2})\}, n)) & | I(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.r.\underline{x} ↦ (O, m, (I ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, n)) & | I(\underline{c}) = α_{2}, \\ (\underline{c}.s.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{0})\}, m, I, n)) & | O(\underline{c}) = α_{3}(\underline{x}) \} \end{matrix}

U^{MUX2}(O, m, I, n) =

\{ \begin{matrix}(O ⊕ \{(\underline{c} ↦ α_{2})\}, mˆ ⟨(\underline{c}, \underline{x})⟩, I, n) & | O(\underline{c}) = α_{1}(\underline{x}), \\ (O, m′, I ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, n) & | m ≠ ⟨⟩ ∧ m_{0} = (\underline{c}, \underline{x}) ∧ I(\underline{c}) = α_{0}, \\ (O, m, I ⊕ \{(\underline{c} ↦ α_{0})\}, nˆ ⟨(\underline{c}, \underline{x})⟩) & | I(\underline{c}) = α_{3}(\underline{x}), \\ (O ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, m, I, n′) & | n ≠ ⟨⟩ ∧ n_{0} = (\underline{c}, \underline{x}) ∧ O(\underline{c}) = α_{2} \} \end{matrix}

Now introduce the model

T^{CHANS}(C) =

\{ \begin{matrix}(\underline{c}.p.\underline{x} ↦ C ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}) & | C(\underline{c}) = α_{0}, \\ (\underline{c}.q.\underline{x} ↦ C ⊕ \{(\underline{c} ↦ α_{2})\}) & | C(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.r.\underline{x} ↦ C ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}) & | C(\underline{c}) = α_{2}, \\ (\underline{c}.s.\underline{x} ↦ C ⊕ \{(\underline{c} ↦ α_{0})\}) & | C(\underline{c}) = α_{3}(\underline{x}) \} \end{matrix}

Definition 2.1 The relationship (O, m, I, n) G C holds iff for any c one of the following (mutually exclusive) clauses obtains

C(c) = α_{0}∧
O(c) = α_{0} ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{0} ∧ n ⊳ {(c, )} = ⟨⟩,  (6)
C(c) = α_{1}(x)∧
O(c) = α_{1}(x) ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{0} ∧ n ⊳ {(c, )} = ⟨⟩,  (7)
C(c) = α_{1}(x)∧

O(c) = α_{2} ∧ m ⊳ {(c, )} = ⟨(c, x)⟩ ∧ I(c) = α_{0} ∧ n ⊳ {(c, )} = ⟨⟩,  (8)
C(c) = α_{1}(x)∧
O(c) = α_{2} ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{1}(x) ∧ n ⊳ {(c, )} = ⟨⟩,  (9)
C(c) = α_{2}∧
O(c) = α_{2} ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{2} ∧ n ⊳ {(c, )} = ⟨⟩,  (10)
C(c) = α_{3}(x)∧
O(c) = α_{2} ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{3}(x) ∧ n ⊳ {(c, )} = ⟨⟩,  (11)
C(c) = α_{3}(x)∧
O(c) = α_{2} ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{0} ∧ n ⊳ {(c, )} = ⟨(c, x)⟩,  (12)
C(c) = α_{3}(x)∧
O(c) = α_{3}(x) ∧ m ⊳ {(c, )} = ⟨⟩ ∧ I(c) = α_{0} ∧ n ⊳ {(c, )} = ⟨⟩  (13)

Suppose (O, m, I, n) G C, then the following lemmas hold

Lemma 2.2 . dom T^{MUX2}(O, m, I, n) ⊂ dom T^{CHANS}(C).

Proof: From the definition T^{MUX2}

dom T^{MUX2}(C) = \{ \begin{matrix}\underline{c}.p. | O(\underline{c}) = α_{0}, \\ \underline{c}.q.\underline{x} | I(\underline{c}) = α_{1}(\underline{x}), \\ \underline{c}.r. | I(\underline{c}) = α_{2}, \\ \underline{c}.s.\underline{x} | O(\underline{c}) = α_{3}(\underline{x}) \}. \end{matrix}

From the definition of G,

O(\underline{c}) = α_{0} ⇒ C(\underline{c}) = α_{0}
I(\underline{c}) = α_{1}(\underline{x}) ⇒ C(\underline{c}) = α_{1}(\underline{x})
I(\underline{c}) = α_{2} ⇒ C(\underline{c}) = α_{2}
O(\underline{c}) = α_{3}(\underline{x}) ⇒ C(\underline{c}) = α_{3}(\underline{x})

(each antecedent is only compatible with one of the eight clauses in definition 4.1—in order, clauses 1, 4, 5 and 8. The consequents are part of the respective clauses). From the definition T^{CHANS}

dom T^{CHANS}(C) = \{ \begin{matrix}\underline{c}.p. | C(\underline{c}) = α_{0}, \\ \underline{c}.q.\underline{x} | C(\underline{c}) = α_{1}(\underline{x}), \\ \underline{c}.r. | C(\underline{c}) = α_{2}, \\ \underline{c}.s.\underline{x} | C(\underline{c}) = α_{3}(\underline{x}) \} \end{matrix}

and the result follows.

Lemma 2.3 e ∈ dom T^{MUX2}(O, m, I, n) ⇒ T^{MUX2}(O, m, I, n)(e) G T^{CHANS}(C)(e).

Proof: There are four possibilities:

Firstly, e = c.p.x and O(c) = α_{0}. Clause 1 in definition 4.1 obtains so m ⊳ {(c, )} = ⟨⟩ and I(c) = α_{0} and n ⊳ {(c, )} = ⟨⟩. The new state of the MUX2 system, (O ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, m, I, n), is therefore related to the new state of the CHANS system, C ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, by clause 2.

Secondly, e = c.q.x and I(c) = α_{1}(x). Clause 4 in definition 4.1 obtains so O(c) = α_{2}, m ⊳ {(c, )} = ⟨⟩ and n ⊳ {(c, )} = ⟨⟩. Hence the new state of the MUX2 system, (O, m, I ⊕ \{(\underline{c} ↦ α_{2})\}, n), is related to the new state, C ⊕ \{(\underline{c} ↦ α_{2})\}, of the CHANS system by clause 5.

The third and fourth cases, e = c.r.x and e = c.s.x are handled in the same way.

Lemma 2.4 (O^{1}, m^{1}, I^{1}, n^{1}) ∈ U^{MUX2}(O, m, I, n) ⇒ (O^{1}, m^{1}, I^{1}, n^{1}) G C.

Proof: There are four ways for (O^{1}, m^{1}, I^{1}, n^{1}) ∈ U^{MUX2}(O, m, I, n) to be satisfied.

The first possibility is that for some c, O(c) = α_{1}(x). This is only possible if clause 2 in 4.1 holds. Thus C(c) = α_{1}(x), m ⊳ {(c, )} = ⟨⟩ and I(c) = α_{0} and n ⊳ {(c, )} = ⟨⟩. Consequently (O^{1}, m^{1}, I^{1}, n^{1}) = (O ⊕ \{(\underline{c} ↦ α_{2})\}, mˆ ⟨(\underline{c}, \underline{x})⟩, I, n). is related to C by clause 3 in definition 4.1.

The second possibility is that m ≠ ⟨⟩ ∧ m_{0} = (c, x) ∧ I(c) = α_{0}. The only clause which allows m ⊳ {(c, )} ≠ ⟨⟩ is clause 3. So C(c) = α_{1}(x), O(c) = α_{2} and m ⊳ {(c, )} = ⟨(c, x)⟩ (so m′ ⊳ {(c, )} = ⟨⟩, since m_{0} = (c, x)) and n ⊳ {(c, )} = ⟨⟩. Hence (O^{1}, m^{1}, I^{1}, n^{1}) = (O, m′, I ⊕ \{(\underline{c} ↦ α_{1}(x))\}, n) satisfies clause 4, and this state is indeed related to C.

The other two cases in the definition of U^{MUX2} are treated similarly.

Lemma 2.5 U^{MUX2}(O, m, I, n) = ∅ ⇒ dom T^{MUX2}(O, m, I, n) = dom T^{CHANS}(C).

Proof: According to discussion in the proof of the previous lemma, we can assume that for no c do clauses 2, 3, 6 or 7 hold, otherwise U^{MUX2}(O, m, I, n) would not be empty. So for each c one of clauses 1, 4, 5 or 8 obtains. The result then follows from the discussion in the proof of lemma 2.2.

These lemmas establish that G is a simulation. Hence the multiplexor system implements the channel system.

3 Models and Simulations: II. Acceptance-Transition Systems

In the models described in section 1, the only structures associated with a state were transition functions (labelled or unlabelled). In this section we add a set of “acceptances” for each state.

3.1 Acceptance-Transition Models

An ATM is a generalisation of a simple TM, characterised by a tuple (S, A, T, W). S, A and T are defined as for a TM. W associates set of “acceptances” with each state. An acceptance (in a state i) is some subset of dom T (i). The acceptances W (i) can be thought of as a set of “substates” of the state i. There is no external way of telling which substate is active—this is selected non-deterministically by the system whenever it enters a new state. If an acceptance w ∈ W (i) is active, the system is prepared to engage in any of the transitions in w ⊲ T (i), but it will refuse any event outside w. From this discussion we see that W is in S → Pow Pow A. It is convenient to require that

⋃_{w∈W (i)} w = dom T (i).

ie, there are no redundant transitions in T (i) which the system never offers to engage in.

ATMs are very closely related to the Acceptance Trees of [?], but we have no requirement that W (i) be convex closed or closed under union. Those conditions are necessary if every process must have a unique representation (as in a semantic domain), but less important here, where an ATM is just one amongst many possible parametrisations of a process.

The system of CSP processes associated with an ATM is defined as the (least) solution of

Proc (i) = \begin{matrix}⊓ \\ w ∈ W (i) \end{matrix} (e : w → Proc (T (i)(e))) = \begin{matrix}⊓ \\ w ∈ W (i) \end{matrix} R(w, T (i))(Proc)

Both ETMs and ATMs can express non-determinism. In fact, any divergence-free CSP process can be modelled both by an ATM and by an ETM—often, by many. The advantage of the ETM has already been illustrated—it emerges naturally when internal events are concealed. The advantage of an ATM is that one can show much more directly that it meets a particular CSP specification.

3.1.1 Specifications

Suppose S is the partial function from A^{∗} to S which maps the possible traces of the model, generated from an inital state i, to the state of the model after engaging in that trace. The process associated with i satisfies

tr ∈ dom S ∧ (∃w : W (S(tr)). w ∩ ref = ∅)

3.1.2 Simulations

We give a simulation from ETMs to ATMs. This can be used to show that an ETM arising from event-concealment implements a system modelled by an ATM. This generalises the simulation given in ?? to the case where the processes involved aren’t necessarily deterministic.

Definition 3.1 Suppose (S, A, T, U) is an ETM and (S′, A, T′, W′) is an ATM. The relation G from S to S′ is a simulation if whenever i G i′ the following clauses hold

dom T (i) ⊂ dom T′(i′),  (1)
∀e : dom T (i). T (i)(e) G T′(i′)(e),  (2)
∀j : U(i). j G i′,  (3)
U(i) = ∅ ⇒ (∃w′ : W′(i′). dom T (i) ⊃ w′)  (4)

Theorem 3.2 If G is a simulation in this sense, and Proc is the system of processes associated with the ETM, and Proc′ is the set of process associated with the ATM, then i G i′ implies

Proc (i) ⊒ Proc′(i′)

The proof is deferred to appendix A.

3.2 Extended Acceptance-Transition Models

Finally, suppose we are given a system modelled by an acceptance-transition model, and are required to conceal some events in its alphabet. The ATM can be generalised to an extendeded acceptance-transition model (EATM), in much the same way as the TM was generalised to the ETM, to take account of this.

An EATM is a tuple (S, A, T, U, V), where S, A, T and U have the same properties as for an ETM, and V associates a set of pairs with each state in S. Each pair consists of a set of unlabelled transitions and an acceptance set. A pair can be regarded as a sub-state of the visible state, in the same sense that an acceptance was a sub-state in the ETM. Hence V ∈ Pow (Pow S × Pow A). V is constrained by

⋃_{(u,w)∈V (i)} w = dom T (i), ⋃_{(u,w)∈V (i)} u = U(i).

The system of CSP processes associated with an EATM is defined as the (least) solution of

Proc (i) = \begin{matrix}⊓ \\ (u, w) ∈ W (i) \end{matrix} P (u, w, T (i))(Proc).

3.2.1 Concealment

If Proc is the set of processes associated with an ATM (S, A, T, W), and

Proc′(i) = Proc (i) \ C

for some C ⊂ A, then (S, A, T′, V′) is an AETM for the system Proc′, where

T′(i) = (A − C) ⊲ T (i)
V′(i) = \{(ran ((\underline{w} ∩ C) ⊲ T (i)), \underline{w} − C) | \underline{w} ∈ W (i)\}

3.2.2 Simulations

We give a simulation from EATMs to ATMs. This can be used to show that an EATM arising from event-concealment implements a system modelled by an ATM.

Definition 3.3 Suppose (S, A, T, U, V) is an EATM and (S′, A, T′, W′) is an ATM. The relation G from S to S′ is a simulation if whenever i G i′ the following clauses hold

dom T (i) ⊂ dom T′(i′),  (1)
∀e : dom T (i). T (i)(e) G T′(i′)(e),  (2)
∀j : U(i). j G i′,  (3)
∀(u, w) : V (i). u = ∅ ⇒ (∃w′ : W′(i′). w ⊃ w′)  (4)

Theorem 3.4 If G is a simulation in this sense, and Proc is the system of processes associated with the EATM, and Proc′ is the set of process associated with the ATM, then i G i′ implies

Proc (i) ⊒ Proc′(i′)

The proof is deferred to appendix A.

4 Models for message-routers.

A message delivery system is regarded as a process which accepts messages from a system of user processes, and delivers messages to the user system. A few properties are desirable a priori. For example, the system shouldn’t deliver messages which it hasn’t previously accepted—it shouldn’t generate spurious messages. Similarly, I’ll assume that it doesn’t duplicate messages—for each message accepted, at most one is delivered. Needless to say, many useful message delivery systems don’t guarantee either of these properties.

However they do seem to be reasonable requirements in the context of tightly-coupled MIMD systems. It isn’t difficult for hardware-assisted routing systems to implement these specifications.

Ignoring, for the moment only, liveness properties of the message delivery system, the simplest structure which meets these requirements is the bag [1]. Assume the set of message types is Values. The alphabet of the bag is

αBag = \{\underline{v}^{O} | \underline{v} ∈ Values, \underline{v}^{I} | \underline{v} ∈ Values\}.

The event v^{O} corresponds to output of a message holding value v from the user to the delivery system. v^{I} corresponds to it’s input (delivery of the message). According to the discussion in the previous paragraph any trace tr of Bag should satisfy

∀v : Values. tr ↓ {v^{O}} ≥ tr ↓ {v^{I}}

In fact, so far as traces are concerned, this is the strongest specification needed to yield a workable message delivery system. One can also give a state transition model of this trace set. The state space is

Bstat = Values → Nat

A state B in this space associates a non-negative value with each message type—B(v) is the number of messages of type v presently in transit. The transition function is

T^{Bstat}(B) = \{(\underline{v}^{O} ↦ B ⊕ (\underline{v} ↦ B(\underline{v}) + 1)),
(\underline{v}^{I} ↦ B ⊕ (\underline{v} ↦ B(\underline{v}) − 1)) | B(\underline{v}) ≠ 0\}.

The important property of this transition function is that an event v^{I} can only occur when there are some messages of type v in transit. The required trace set is generated from the initial state B = 0. To show that this system meets the specification above, one can use the result in section 1.1.1 with

dom S = \{\underline{s} | ∀s. s ≤ \underline{s} ⇒ (∀v.B_{s}(v) ≥ 0)\}
S(s) = B_{s}, if s ∈ dom S

where B_{s}(v) = s ↓ {v^{O}} − s ↓ {v^{I}}.

This specification of the system’s traces embodies the “safety” properties demanded in the opening paragraph of this section. It says nothing about “liveness”. The ideal router would be a deterministic process with the specified traces. This system would never refuse any event offered by the enviroment so long as the event was engagable according to the trace specification. The only events it ever refused would be those inputs corresponding to messages which hadn’t yet been sent. It would always accept any output, and at any time it would be prepared to deliver any message it currently held (at least, it would deliver any such message in bounded time, without conditions on whether the user was refusing to input some other set of messages also in transit). No real message delivery system has these properties because they depend on the availability of infinite buffering. Infinite buffering can be approximated, up to a point, by, say, having large buffers permanently allocated, which is costly in memory, or by dynamically allocating memory to buffers as required, which is costly in processor time. This rules out such schemes out for the purposes of this article.

What is the minimal set of liveness properties for a useful delivery system? Certainly, if the delivery system is empty (no message in transit), we would expect it to be prepared to accept any message. It might sometimes refuse to accept outputs if there are messages in transit, because some buffers may have filled up. Secondly, if there are messages in transit, we would expect it to be willing to deliver at least one of them ^{2}. However, we will accept that delivery of some messages in transit may be deferred pending delivery of some other messages, also in transit, due to some internal forwarding buffers being occupied.

These minimal requirements are embodied in the (failures model) specification

tr ∈ traces (Bag) ∧ (if (∀v : Values. tr ↓ {v^{O}} = tr ↓ {v^{I}}) then
(∀v : Values. v^{O} ∉ ref) else
(∃v : Values. tr ↓ {v^{O}} > tr ↓ {v^{I}} ∧ v^{I} ∉ ref))

This asserts that the traces of the system are those described above, and that if there are no messages in transit, no refusal state refuses any output event; otherwise, in any refusal state there is (at least) one input event corresponding to a message in transit which won’t be refused.

An acceptance transition model defining a process which satisfies this specification is (αBag, Bstat, T^{Bstat}, W^{Bstat}) where

W^{Bstat}(B) = \{\{\underline{v}^{I}\} | B(\underline{v}) > 0, \{\underline{\underline{v}}^{I} | B(\underline{\underline{v}}) > 0, \underline{\underline{v}}^{O}\}\}

(ie, W^{Bstat}(B) contains singleton sets corresponding to each input event for which B(v) > 0, and a set containing all input events satisfying the same condition together with all output events). This can be proven immediately using the result in section ??.

4.1 “Virtual Channels” Implemented on a Message-Router

Suppose

Message = \{\underline{c}.f.\underline{x} | \underline{c} ∈ Chans ∧ \underline{x} ∈ Values, \underline{c}.b.\underline{x} | \underline{c} ∈ Chans ∧ \underline{x} ∈ Values\}.

Consider the following putative implementation of a virtual channel system:

(( \begin{matrix}∥ \\ c ∈ Chans \end{matrix} c : OBUF) ∥
( \begin{matrix}∥ \\ c ∈ Chans \end{matrix} c : IBUF) ∥ BAG ) \ H

The system of input and output buffers is modelled by the TM (A^{IO}, S^{IO}, T^{IO}), where

A^{IO} = \{\underline{c}.p.\underline{x}, \underline{c}.f.\underline{x}^{O}, \underline{c}.f.\underline{x}^{I}, \underline{c}.q.\underline{x}, \underline{c}.r.\underline{x}, \underline{c}.b.\underline{x}^{O}, \underline{c}.b.\underline{x}^{I}, \underline{c}.s.\underline{x}\}
S^{IO} = (Chans → S^{O}) × (Chans → S^{I})

and

T^{IO}(O, I) =

\{ \begin{matrix}(\underline{c}.p.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, I)) & | O(\underline{c}) = α_{0}, \\ (\underline{c}.f.\underline{x}^{O} ↦ (O ⊕ \{(\underline{c} ↦ α_{2})\}, I)) & | O(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.f.\underline{x}^{I} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\})) & | I(\underline{c}) = α_{0}, \\ (\underline{c}.q.\underline{x} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{2})\})) & | I(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.r.\underline{x} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\})) & | I(\underline{c}) = α_{2}, \\ (\underline{c}.b.\underline{x}^{O} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{0})\})) & | I(\underline{c}) = α_{3}(\underline{x}), \\ (\underline{c}.b.\underline{x}^{I} ↦ (O ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, I)) & | O(\underline{c}) = α_{2}, \\ (\underline{c}.s.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{0})\}, I)) & | O(\underline{c}) = α_{3}(\underline{x}) \} \end{matrix}

2This property may not be satisfied if the delivery system is prone to internal deadlock.

The initial state is ({( ↦ α_{0})}, {( ↦ α_{0})}). Hence

dom T^{IO}(O, I) =

\{ \begin{matrix}\underline{c}.p.\underline{x} & | O(\underline{c}) = α_{0}, \\ \underline{c}.f.\underline{x}^{O} & | O(\underline{c}) = α_{1}(\underline{x}), \\ \underline{c}.f.\underline{x}^{I} & | I(\underline{c}) = α_{0}, \\ \underline{c}.q.\underline{x} & | I(\underline{c}) = α_{1}(\underline{x}), \\ \underline{c}.r.\underline{x} & | I(\underline{c}) = α_{2}, \\ \underline{c}.b.\underline{x}^{O} & | I(\underline{c}) = α_{3}(\underline{x}), \\ \underline{c}.b.\underline{x}^{I} & | O(\underline{c}) = α_{2}, \\ \underline{c}.s.\underline{x} & | O(\underline{c}) = α_{3}(\underline{x}) \}. \end{matrix}

Now we need to calculate dom T^{IO}(O, I) [A^{IO} ⊓ A^{BAG}] w for each w in the set

W^{BAG}(B) =

\{ \{\underline{c}.f.\underline{x}^{I}\} | B(\underline{c}.f.\underline{x}) > 0, \{\underline{c}.b.\underline{x}^{I}\} | B(\underline{c}.b.\underline{x}) > 0, dom T^{BAG}(B) \}.

where

dom T^{BAG}(B) =
\{ \underline{c}.f.\underline{x}^{I} | B(\underline{c}.f.\underline{x}) > 0, \underline{c}.b.\underline{x}^{I} | B(\underline{c}.b.\underline{x}) > 0, \underline{c}.f.\underline{x}^{O}, \underline{c}.b.\underline{x}^{O} \}.

The result is

W^{ROUT}(O, I, B) =

\{ \begin{matrix}w^{EXT}(O, I) ∪ \{\underline{c}.f.\underline{x}^{I}\} & | B(\underline{c}.f.\underline{x}) > 0 ∧ I(\underline{c}) = α_{0}, \\ w^{EXT}(O, I) & | B(\underline{c}.f.\underline{x}) > 0 ∧ I(\underline{c}) ≠ α_{0}, \\ w^{EXT}(O, I) ∪ \{\underline{c}.b.\underline{x}^{I}\} & | B(\underline{c}.b.\underline{x}) > 0 ∧ O(\underline{c}) = α_{2}, \\ w^{EXT}(O, I) & | B(\underline{c}.b.\underline{x}) > 0 ∧ O(\underline{c}) ≠ α_{2}, \\ dom T^{ROUT}(O, I, B) \}, \end{matrix}

where

w^{EXT}(O, I) =

\{ \begin{matrix}\underline{c}.p.\underline{x} & | O(\underline{c}) = α_{0}, \\ \underline{c}.q.\underline{x} & | I(\underline{c}) = α_{1}(\underline{x}), \\ \underline{c}.r.\underline{x} & | I(\underline{c}) = α_{2}, \\ \underline{c}.s.\underline{x} & | O(\underline{c}) = α_{3}(\underline{x}) \} \end{matrix}

and

dom T^{ROUT}(O, I, B) =

w^{EXT}(O, I) ∪ \{ \begin{matrix}\underline{c}.f.\underline{x}^{I} & | B(\underline{c}.f.\underline{x}) > 0 ∧ I(\underline{c}) = α_{0}, \\ \underline{c}.b.\underline{x}^{I} & | B(\underline{c}.b.\underline{x}) > 0 ∧ O(\underline{c}) = α_{2}, \\ \underline{c}.f.\underline{x}^{O} & | O(\underline{c}) = α_{1}(\underline{x}), \\ \underline{c}.b.\underline{x}^{O} & | I(\underline{c}) = α_{3}(\underline{x}) \}. \end{matrix}

Completing the definition of T^{ROUT}: T^{ROUT}(O, I, B) =

\{ \begin{matrix}(\underline{c}.p.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, I, B)) & | O(\underline{c}) = α_{0}, \\ (\underline{c}.f.\underline{x}^{O} ↦ (O ⊕ \{(\underline{c} ↦ α_{2})\}, I, B ⊕ \{(\underline{c}.f.\underline{x} ↦ B(\underline{c}.f.\underline{x}) + 1)\})) & | O(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.f.\underline{x}^{I} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, B ⊕ \{(\underline{c}.f.\underline{x} ↦ B(\underline{c}.f.\underline{x}) − 1)\})) & | I(\underline{c}) = α_{0} ∧ B(\underline{c}.f.\underline{x}) ≠ 0, \\ (\underline{c}.q.\underline{x} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{2})\}), B) & | I(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.r.\underline{x} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}), B) & | I(\underline{c}) = α_{2}, \\ (\underline{c}.b.\underline{x}^{O} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{0})\}, B ⊕ \{(\underline{c}.b.\underline{x} ↦ B(\underline{c}.b.\underline{x}) + 1)\})) & | I(\underline{c}) = α_{3}(\underline{x}), \\ (\underline{c}.b.\underline{x}^{I} ↦ (O ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, I, B ⊕ \{(\underline{c}.b.\underline{x} ↦ B(\underline{c}.b.\underline{x}) − 1)\})) & | O(\underline{c}) = α_{2} ∧ B(\underline{c}.b.\underline{x}) ≠ 0, \\ (\underline{c}.s.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{0})\}, I, B)) & | O(\underline{c}) = α_{3}(\underline{x}) \}, \end{matrix}

yields the ATM (A^{IO}, S^{IO} × S^{BAG}, T^{ROUT}, W^{ROUT}) describing the combined system. Next, we conceal the internal events to yield an EATM.

T^{ROUT2}(O, I, B) =

\{ \begin{matrix}(\underline{c}.p.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, I, B)) & | O(\underline{c}) = α_{0}, \\ (\underline{c}.q.\underline{x} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{2})\}), B) & | I(\underline{c}) = α_{1}(\underline{x}), \\ (\underline{c}.r.\underline{x} ↦ (O, I ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}), B) & | I(\underline{c}) = α_{2}, \\ (\underline{c}.s.\underline{x} ↦ (O ⊕ \{(\underline{c} ↦ α_{0})\}, I, B)) & | O(\underline{c}) = α_{3}(\underline{x}) \}, \end{matrix}

U^{ROUT2}(O, I, B) =

\{ \begin{matrix}(O ⊕ \{(\underline{c} ↦ α_{2})\}, I, B ⊕ \{(\underline{c}.f.\underline{x} ↦ B(\underline{c}.f.\underline{x}) + 1)\}) & | O(\underline{c}) = α_{1}(\underline{x}), \\ (O, I ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, B ⊕ \{(\underline{c}.f.\underline{x} ↦ B(\underline{c}.f.\underline{x}) − 1)\}) & | I(\underline{c}) = α_{0} ∧ B(\underline{c}.f.\underline{x}) ≠ 0, \\ (O, I ⊕ \{(\underline{c} ↦ α_{0})\}, B ⊕ \{(\underline{c}.b.\underline{x} ↦ B(\underline{c}.b.\underline{x}) + 1)\}) & | I(\underline{c}) = α_{3}(\underline{x}), \\ (O ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, I, B ⊕ \{(\underline{c}.b.\underline{x} ↦ B(\underline{c}.b.\underline{x}) − 1)\}) & | O(\underline{c}) = α_{2} ∧ B(\underline{c}.b.\underline{x}) ≠ 0 \}, \end{matrix}

V^{ROUT2}(O, I, B) =

\{ \begin{matrix}(w^{EXT}(O, I), \{(O, I ⊕ \{(\underline{c} ↦ α_{1}(\underline{x}))\}, B ⊕ \{(\underline{c}.f.\underline{x} ↦ B(\underline{c}.f.\underline{x}) − 1)\}))\} & | I(\underline{c}) = α_{0} ∧ B(\underline{c}.f.\underline{x}) ≠ 0, \\ (w^{EXT}(O, I), ∅) & | I(\underline{c}) ≠ α_{0} ∧ B(\underline{c}.f.\underline{x}) ≠ 0, \\ (w^{EXT}(O, I), \{(O ⊕ \{(\underline{c} ↦ α_{3}(\underline{x}))\}, I, B ⊕ \{(\underline{c}.b.\underline{x} ↦ B(\underline{c}.b.\underline{x}) − 1)\}))\} & | O(\underline{c}) = α_{2} ∧ B(\underline{c}.b.\underline{x}) ≠ 0, \\ (w^{EXT}(O, I), ∅) & | O(\underline{c}) ≠ α_{2} ∧ B(\underline{c}.b.\underline{x}) ≠ 0, \\ (w^{EXT}(O, I), U^{ROUT2}(O, I, B)) \}. \end{matrix}

Finally, we have to show that the EATM (A^{CHANS}, S^{ROUT}, T^{ROUT2}, U^{ROUT2}), V^{ROUT2}) simulates the TM (A^{CHANS}, S^{CHANS}, T^{CHANS}). We define the relation G from S^{ROUT} to S^{CHANS} as follows:

Definition 4.1 The relationship (O, m, I, n) G C holds iff for any c one of the following (mutually exclusive) clauses obtains for some x

C(c) = α_{0}∧
O(c) = α_{0} ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{0} ∧ (∀y. B(c.b.y) = 0),  (5)
C(c) = α_{1}(x)∧
O(c) = α_{1}(x) ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{0} ∧ (∀y. B(c.b.y) = 0),  (6)
C(c) = α_{1}(x)∧
O(c) = α_{2} ∧ (∀y. B(c.f.y) = δ_{xy}) ∧ I(c) = α_{0} ∧ (∀y. B(c.b.y) = 0),  (7)
C(c) = α_{1}(x)∧
O(c) = α_{2} ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{1}(x) ∧ (∀y. B(c.b.y) = 0),  (8)
C(c) = α_{2}∧
O(c) = α_{2} ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{2} ∧ (∀y. B(c.b.y) = 0),  (9)

C(c) = α_{3}(x)∧
O(c) = α_{2} ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{3}(x) ∧ (∀y. B(c.b.y) = 0), (10)
C(c) = α_{3}(x)∧
O(c) = α_{2} ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{0} ∧ (∀y. B(c.b.y) = δ_{xy}),  (11)
C(c) = α_{3}(x)∧
O(c) = α_{3}(x) ∧ (∀y. B(c.f.y) = 0) ∧ I(c) = α_{0} ∧ (∀y. B(c.b.y) = 0)  (12)

The first three properties needed to establish that G is a simulation are proved in exactly the same way as in lemmas ?? to ??. The last lemma needed is, assuming (O, m, I, n) G C

Lemma 4.2 ((w, u) ∈ V^{MUX2}(O, m, I, n) ∧ u = ∅) ⇒ (w ⊃ dom T^{CHANS}(C)).

Proof: A priori, there are five cases to consider:

1. I(c) = α_{0} ∧ B(c.f.x) ≠ 0 and u = {(O, I ⊕ {(c ↦ α_{1}(x))}, B ⊕ {(c.f.x ↦ B(c.f.x) − 1)}))}.

2. I(c) ≠ α_{0} ∧ B(c.f.x) ≠ 0 and u = ∅.

3. O(c) = α_{2} ∧ B(c.b.x) ≠ 0 and u = {(O ⊕ {(c ↦ α_{3}(x))}, I, ⊕{(c.b.x ↦ B(c.b.x) − 1)})}.

4. O(\underline{c}) ≠ α_{2} ∧ B(\underline{c}.b.\underline{x}) ≠ 0 and u = ∅.

5. u = U^{ROUT2}(O, I, B).

In case 1, u = ∅ is false, so the implication is valid.

The precondition of case 2 contradicts the assumption that (O, I, B) is in the range of G (none of the clauses in the definition is consistent with this condition). So this case doesn’t need further consideration.

Case 3 is like case 1.

Case 4 is like case 2.

In case 5 the implication is established as for lemma ??.

5 Discussion

5.1 Working with deterministic models

The example given in the previous section was sufficiently simple that we could afford to simply combine the non-deterministic delivery system with the IO buffer system in one step, then immediately conceal internal events in the composite model and verify a simulation from the result to a model of the specification.

In general it may be more convenient to go through intermediate simulations (“refinements”) between the composition step and the concealment (“abstraction”) step. Moreover, in some of the steps it may be possible to ignore the non-determinism in one or more of the original components. Note

P = P ∥ P^{det}

where P^{det} is the deterministic process with the same traces as P. In terms of our transition models, it can be represented by the TM obtained from any generalised transition model standing for P by ignoring any U, V or W fields. Evidently, life is simpler if one can work with this system rather than the original non-deterministic one.

Suppose P is being composed with some system Q. According to the observation above, if we can show

P^{det} ∥ Q ⊒ R

then it follows by monotonicity of ∥ that

P ∥ Q ⊒ P ∥ R

The value of this theorem is that R may be more tractable than Q, so that composing it with the full P is simpler than direct use of R. On the other hand, the establishing the precondition is simplified because P^{det} is a deterministic process. For example, in the virtual channel example of section ??, composing the deterministic part of the delivery system with the IO buffer system yields the TM (A^{IO}, T^{ROUT}). Then, by a straightforward TM to TM simulation one can show equivalence of this system to the more concise deterministic system

\begin{matrix}∥ \\ c ∈ Chans \end{matrix} c : IOBUF

where

IOBUF = μX. _{x}p.x → f^{O}.x → _{y}f^{I}.y → q.y _{z}r.z → b^{O}.z _{w}b^{I}.w → s.w → X

Now this system is combined with the full non-deterministic model for the router, and the rest of the calculation can proceed essentially as before. In this case the simplification obtained in this way is not enormous (which is why this logical step was skipped in the earlier presentation). In general, there may be significant advantages to be gained by organising the proof in this way ^{3}.

5.2 Eagerness

Low-level message delivery systems for multi-processors often come with a guarantee that they are “deadlock-free, provided the user processes are eager readers”. The intuitive idea of a process being an “eager reader” is that it never refuses to accept any message that has been sent to it (or, at least, it only defers this acceptance for a bounded time, while it may be engaging in some internal activity).

Intuitively, eager readership seems to be an important concept. In this section we will try to give a more precise characterisation of eagerness. In this analysis, the slightly mysterious promise about deadlock freedom quoted in the previous paragraph could be replaced by: “the message delivery system is effectively deterministic provided the system of user processes is an eager reader” ^{4}.

So, suppose pending (tr) is a function on traces which returns the set of message-input events the delivery system may engage in (according to its traces) after the system as a whole has executed a trace tr. In the bag model this is just

pending (tr) = \{\underline{m}^{I} | tr ↓ \{\underline{m}^{O}\} > tr ↓ \{\underline{m}^{I}\}\}

3In passing, note that the clarity of the proof in section ?? would also have benefitted from inserting a further intermediate simulation between composition with the non-deterministic router and concealment of events—eliminating many redundant states before rather than after concealment

4The replacement, here, of individual “user processes” by the system as a whole recognises the fact that eagerness must be a global property—there is no implication that an individual process should always be waiting to accept notional messages which haven’t actually been sent to it (by one of the other user processes).

Now, if P is the message delivery system, and Q is the system of user processes, Q is an eager-reading system if it satisfies

∀s : traces (P ∥ Q). ∀X : refusals (Q/s ⊳ αQ). pending (s) ∩ X = ∅

This says that Q never refuses any pending messages (***remark on appearance of P —— Q here***). Now one can easily proof the following quite striking theorem

Theorem 5.1 If P′ is any process with the same traces as P which satisfies the liveness property in section ??, then

(P′ ∥ Q) \ \{\underline{m}^{I}\} = (P ∥ Q) \ \{\underline{m}^{I}\}

In particular one can take P′ = P^{det}. So if Q is an eager reader we can replace the message delivery system by its deterministic counterpart, and after the abstraction step of hiding message inputs, we end up with the same process as if we had used the full non-deterministic definition of P.

This appears to be a powerful result. It seems obvious that the system of independent IOBUF processes is an eager-reading system, so we can just hide inputs in that model without ever worrying about acceptances of the message delivery system, and get the proof that the system meets it’s specification that much more easily.

In general, unfortunately, proving that a system has the eager readership property may itself be non-trivial, and the simplification implied here may be slightly illusory. Still, this is a proof technique which deserves investigation.

Incidentally, we have only given the simplest possible definition of eagerness here, in the context of a bag-like message router. Needless to say, the idea can be generalised in several directions, and similar theorems proved.

5.3 More structured models of message-delivery systems

The “bag” model of a message delivery system is useful for illustrative purposes, but it doesn’t capture much of the structure of a typical message delivery systems. There is no inherent idea of locality—messages are inserted into the system and removed from it without any association with a point (in “processor space”) from which they are originating or to which they are being delivered. Also, many delivery systems provide guarantees on sequencing of messages which are passed “between the same points”— messages emerge from the delivery system in order which they inserted.

These shortcomings can be addressed by adding “ports” to the delivery system. Logical channels exist between any pair of ports, and message delivery across any particular channel is sequence-preserving. Each port may be associated with a particular processor (there may be one or many ports per processor)

The alphabet of the new system is

αMsys = \{\underline{M}^{O}.\underline{v} | \underline{M} ∈ Ports^{2} ∧ \underline{v} ∈ Messages, \underline{M}^{I}.\underline{v} | \underline{M} ∈ Ports^{2} ∧ \underline{v} ∈ Messages,

where Ports is the space of ports. The traces associated with the system now satisfy

∀(P, Q) : Ports^{2}. tr ↓ {(P, Q)^{O}} > tr ↓ {(P, Q)^{I}}

In fact, so far as traces are concerned, this is the strongest specification needed to yield a workable message delivery system. One can also give a state transition model of this trace set. The state space is

Mstat = Ports^{2} → Values^{∗}

A state B in this space associates a non-negative value with each message type—B(v) is the number of messages of type v presently in transit. The transition function is

T^{Msys}(M) = \{((\underline{P} , \underline{Q})^{O}.\underline{v} ↦ M ⊕ ((\underline{P} , \underline{Q}) ↦ M(\underline{P} , \underline{Q})ˆ ⟨\underline{v}⟩)),

((\underline{P} , \underline{Q})^{I}.\underline{v} ↦ M ⊕ ((\underline{P} , \underline{Q}) ↦ M(\underline{P} , \underline{Q})′))M(\underline{P} , \underline{Q})′) ≠ ⟨⟩ ∧ \underline{v} = M(\underline{P} , \underline{Q})_{0}\}.

A Proof of simulations

All our simulation results can be regarded as special cases of the result in section 3.2.2. That result is proved here. First we need an auxilliary lemma.

Lemma A.1 Suppose W and W′ are both sets of subsets of A (ie, elements of Pow Pow A) where the set A indexes a set of processes \{P\underline{e} | \underline{e} ∈ A\}. If the union of the elements of W contains the union of the elements of W′

( ⋃_{w′∈W′} w′) ⊂ ( ⋃_{w∈W} w),

and any w′ in W′ contains some w from W, ie ^{5}

∀w′ : W′. ∃w : W. w′ ⊃ w

then

( \begin{matrix}⊓ \\ w′ ∈ W′ \end{matrix} \begin{matrix}□ \\ e′ ∈ w′ \end{matrix} P_{e}) ⊒ ( \begin{matrix}⊓ \\ w ∈ W \end{matrix} \begin{matrix}□ \\ e ∈ w \end{matrix} P_{e})

Proof: First we show

a □ b ⊒ a ⊓ (a □ b □ c)  (1)

This follows because

a ⊒ a ⊓ (a □ c)
b ⊒ a ⊓ b

both of which are due to A ⊒ A ⊓ B. Then monotonicity of □ gives

a □ b ⊒ (a ⊓ (a □ c)) □ (a ⊓ b) = a ⊓ ((a □ c) □ b)

where the equality depends on distribution of ⊓ over □. This yields 1. Now, introduce w_{1} and W satisfying w_{1} ⊂ w′ ⊂ W, and identify

a = \begin{matrix}□ \\ e ∈ w_{1} \end{matrix} P_{e}
b = \begin{matrix}□ \\ e ∈ w′ − w_{1} \end{matrix} P_{e}
c = \begin{matrix}□ \\ e ∈ W − w′ \end{matrix} P_{e}.

1 becomes

\begin{matrix}□ \\ e ∈ w′ \end{matrix} P_{e} ⊒ ( \begin{matrix}□ \\ e ∈ w_{1} \end{matrix} P_{e}) ⊓ ( \begin{matrix}□ \\ e ∈ W \end{matrix} P_{e}).  (2)

5This condition is sometimes [?] written as W′ ⊂⊂ W

If w_{1} ∈ W,

\begin{matrix}□ \\ e ∈ w_{1} \end{matrix} P_{e} ⊒ ( \begin{matrix}⊓ \\ w ∈ W \end{matrix} \begin{matrix}□ \\ e ∈ w \end{matrix} P_{e})

because A ⊒ A ⊓ B. If, also, W = ⋃_{w∈W} w,

\begin{matrix}□ \\ e ∈ W \end{matrix} P_{e} = ( \begin{matrix}□ \\ w ∈ W \end{matrix} \begin{matrix}□ \\ e ∈ w \end{matrix} P_{e}) ⊒ ( \begin{matrix}⊓ \\ w ∈ W \end{matrix} \begin{matrix}□ \\ e ∈ w \end{matrix} P_{e})

because A □ B ⊒ A ⊓ B. Subsituting these two results in 2, using monotonicity and idempotence of ⊓, gives

\begin{matrix}□ \\ e ∈ w′ \end{matrix} P_{e} ⊒ ( \begin{matrix}⊓ \\ w ∈ W \end{matrix} \begin{matrix}□ \\ e ∈ w \end{matrix} P_{e}).

This inequality depended only on the assumptions that there existed w_{1} ∈ W such that w_{1} ⊂ w′, and that w′ ⊂ ⋃_{w∈W} w. Monotoniciy and idempotence of ⊓ now establish the lemma.

Now, suppose G is a simulation in the sense of definition 3.3 from the EATM (S, A, T, U, V) to the ATM (S′, A, T′, W′).

Lemma A.2 There exists a function I^{U} : S → Nat such that

∀j : U(i). I^{U}(j) < I^{U}(i)

Proof: I^{U} can be constructed as

I^{U}(i) = min{n | Ũ^{n}{i} = ∅}

Well-definedness of this function is guaranteed by the nilpotence of U. The required property (which will be used in a proof by complete induction) follows easily.

Definition A.3 For any i′ in ran G define

X′(i′) = \begin{matrix}⊓ \\ j G i′ \end{matrix} Proc (j)

Lemma A.4 If i G i′,

Proc(i) ⊒ X′(i′).

Proof: From the law A ⊒ A ⊓ B.

Corollary A.5 If i G i′,

R(w, T (i))(Proc) ⊒ R(w, T′(i′))(X′)

for any w ⊂ dom T (i).

Proof: By clauses 1 and 2 in 3.3, T (i)(e) G T′(i′)(e) for and e in dom T (i). So, by the lemma

Proc (T (i)(e)) ⊒ X′(T′(i′)(e))

The definition of R, and monotonicity of the choice operation, then imply the corollary.

We can now derive the principle lemma needed to prove theorem 3.4:

Lemma A.6 If i G i′ then

Proc (i) ⊒ \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′)

Proof: We use complete induction. The induction hypothesis is that the lemma is satisfied for all states j in dom G with I^{U}(j) < n, and we must show that it holds for any state i with I^{U}(i) = n. First we show

P (u, w, T (i))(Proc) ⊒ \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′)  (1)

for any (u, w) ∈ V (i). There are two cases to consider: u = ∅ and u ≠ ∅.

Case I: P reduces to R, and

\begin{aligned}R(w, T (i))(Proc) ⊒ & R(w, T′(i′))(X′) ⊒ \\ & \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′) \end{aligned}

where the first inequality follows from lemma A.5 and the second inequality uses final clause in the definition of G, together with lemma A.1, choosing W = {w}.

Case II: P contains two terms. First

Q(u)(Proc) = \begin{matrix}⊓ \\ j ∈ u \end{matrix} Proc (j) ⊒

\begin{matrix}⊓ \\ j ∈ u \end{matrix} \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′) =

\begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′)

The first inequality follows because, according to the third clause in the definition of G, for each term in the left-hand side j G i′. So, by the properties of I^{U}, the induction hypothesis is applicable to the individual terms—the inequality then follows from monotonicity of ⊓. The subsequent equality is due to idempotence of ⊓. The second term in P is

Q(u)(Proc) □ R(w, T (i))(Proc) ⊒

( \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′)) □ R(w, T′(i′))(X′) =

\begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′ ∪ w, T′(i′))(X′) ⊒

\begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′)

The first inequality depends on monotonicity of □, using the result above and corollary A.5. The middle equality follows from the definition of R, using the fact that □ distributes over ⊓. The final inequality is an application of A.1 with W = \{\underline{w}′ ∪ w | \underline{w}′ ∈ W′(i′)\}. In P, these two terms are combined non-deterministically. Due to the monotonicity and idempotence of ⊓, P satisfies the same inequality as its two terms. This establishes 1, and the induction step follows from the equation satisfied by Proc(i), namely

Proc (i) = \begin{matrix}⊓ \\ (u, w) ∈ W (i) \end{matrix} P (u, w, T (i))(Proc),

using monotonicity and idempotence of □.

Now, from the definition A.3, lemma A.6, and the monotonicity and idempotence of ⊓,

X′(i′) ⊒ \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(X′)

On the other hand, by definition, the system Proc′ is the least solution of

Proc′(i′) = \begin{matrix}⊓ \\ w′ ∈ W′(i′) \end{matrix} R(w′, T′(i′))(Proc′)

Since least fixpoints are also least pre-fixpoints^{6}, we can conclude that

X′(i′) ⊒ Proc′(i′)

Theorem 3.4 follows from lemma A.4.

References

[1] C.A.R. Hoare and He Jifeng, “Design and Proof of a Mail Service”, in “Developments in Concurrency and Communication” edited by C.A.R. Hoare, Addison Wesley (1990).

6A pre-fixpoint of F satisfies X ⊐ F X