Past exam of the computer science course of the University of Oxford / 2015 / Concurrency (A10405W1)

Solutions to all three questions of the examination dated 1 June 2015. The cover permits answers to two questions.^[ref]

Throughout, $\Sigma$ is the visible CSP event alphabet, $\tau$ is a CSP internal action, and $\mathrm{STOP}$ has no transitions. There is no successful termination event. Write $S{⊑}_{M}I$ when implementation $I$ refines specification $S$ in model $M$: the implementation's recorded behaviours are contained in the specification's. We use $T$, $F$ and $FD$ for the CSP traces model, CSP stable-failures model and CSP failures-divergences model.

The unique fixed point principle says that a suitably guarded recursion has a unique solution in the chosen CSP semantic model. In particular, for a guarded process expression $F(X)$,The same principle applies to a mutually recursive system: two tuples satisfying the same guarded equations are componentwise equal. Thus an algebraic proof may show that a candidate satisfies the defining equations, instead of comparing arbitrarily long executions individually.

A guarded recursion must make visible progress before re-entering its recursive dependency. For an equation built from CSP prefixing and CSP choice, the usual sufficient condition is that every recursive occurrence lies behind a visible CSP prefixing operation. For mutually recursive equations, every dependency cycle must pass such a guard. The guard must survive enclosing operators: an event subsequently removed by CSP hiding does not provide visible progress. Equivalently, in the usual semantic formulation the recursion functional must be contractive in observable depth. Merely seeing an arrow somewhere before the variable is insufficient.

Take a fresh CSP event $h$ and defineThe apparent guard is removed by CSP hiding. Each unfolding can perform a CSP internal action and return to the same situation without any visible CSP event. Operationally this is an infinite internal loop, a CSP divergence, so the equation is not a guarded recursion. This is precisely why a syntactic test that counts every occurrence of $\to$ would be wrong.

Let $X=P{}_{\{a,b,d\}}{\Vert }_{\{a,b,c\}}Q$. In this CSP alphabetized parallel composition, $a,b$ require both participants, $d$ belongs only to the left participant and $c$ only to the right participant. Expand the reachable states using CSP prefixing and CSP external choice:For example, after the synchronized $b$, the left participant is back at $P$ but the right participant is at $c\to Q$. The left participant's proposed $a$ is blocked until the right participant has performed $c$. Similarly, after $a,d$, only the synchronized $b$ is possible. Thus there is no extra interleaving to include.

Eliminating $Y,W,Z$ gives the guarded equationConsequently choose the sequential CSP processThe unique fixed point principle first establishes $R=X$.

Now let $E=X{\Theta }_{\{c\}}X$. The CSP exception operator follows its left operand until that operand performs $c$, includes this $c$ in the visible behaviour, and then switches to its right operand. Applying its CSP step law to the four-state expansion yieldsThe switch occurs exactly where the ordinary execution already returns to $X$. Therefore $E=X=R$. The answer uses neither a CSP exception operator nor a CSP parallel composition operator, and the argument gives equality in all three standard CSP semantic models.

Use a chain of identical storage cells, each retaining the first value it sees and passing later values to the next cell. On the return journey it passes the next cell's reversed output before emitting its own retained value. This turns the chain into a distributed LIFO stack.

Here is one cell template. Its ports $l,r$ carry incoming values towards the tail; $v,u$ carry returning values towards the front. Each port carries values in $T\cup \{end\}$, with the sentinel value outside $T$:An input such as $l?x:T$ abbreviates an indexed CSP external choice over the corresponding CSP events. An output $r!y$ is the CSP prefixing action $r.y$. There is no extra controller process.

For $n\ge 1$, take $n$ copies of this same template. Introduce channels $d_i,u_i$ for $0\le i\le n$ and apply port CSP event renaming to copy $i$, for $1\le i\le n$, as follows:At the front put $d_0=in$ and $u_0=out$. Adjacent cells synchronize on every shared $d_i$ or $u_i$ CSP event. The two tail channels $d_n,u_n$ are sentinel-only: $d_n.end$ and $u_n.end$ are local tail CSP events, with no other participant required. Disable all $d_n.x,u_n.x$ for $x\in T$. Formally, use a partial relational CSP event renaming for the last copy, omitting the pairs for its $r.x,v.x$ with $x\in T$; an unmapped transition is blocked. This explicitly prevents a fictitious tail from generating data.

Let $C_i$ be the resulting port-renamed cell and $A_i$ its visible alphabet. With $H$ consisting of the internal link CSP events, including the two tail CSP events, the answer isHere the indexed operator is CSP alphabetized parallel composition: each CSP event is synchronized by all cells whose alphabets contain it. There are exactly $n$ storage-cell processes; port wiring and the sentinel-only tail adapt their interfaces, without adding a helper process. The local tail CSP events are hidden, as are all inter-cell communications.

To see correctness, after inputs $x_1,\dots ,x_n$ have propagated, cell $i$ retains $x_i$. The input sentinel value propagates to the tail. The last cell performs its two local tail CSP events, then returns $x_n,end$. Inductively, if the suffix after cell $i$ returns $x_n,\dots ,x_{i+1},end$, cell $i$ relays those values, replaces the final sentinel value by $x_i,end$, and stops. Hence the external output isand starts only after $in.end$. Shared links provide synchronization rather than an assumption that all cells take steps simultaneously. For the degenerate known-empty input, no storage is needed: the interface is simply $in.end\to out.end\to \mathrm{STOP}$.

In the displayed network, the first $k$ cells retain values and cell $k+1$ is still in its initial $\mathrm{Cell}$ state. It accepts only a value in $T$, so it cannot accept the incoming sentinel value. For $k=0$ the first cell blocks the external sentinel value; for $0<k<n$ a stored cell blocks while trying to pass it to an empty neighbour. ThusTo handle shorter inputs, add an empty-cell branch $l.end\to u.end\to \mathrm{STOP}$ to the initial state. An empty cell then terminates the downward scan and immediately returns an empty sequence. Earlier occupied cells append their retained values exactly as before; later cells need not participate. This works for every $0\le k\le n$, because the occupied prefix of the chain alone produces the required output. For $k=n$, the original sentinel-only tail still supplies the empty suffix. Every cell receives the same modification.

The obstruction is that the property is about where a transition originates, whereas the three standard CSP semantic models identify processes that can disagree about this fact. Take fresh $h\ne a$ and compareIn $G$, the only $a$ transition leaves a CSP stable state, so the property holds. Initially $B$ has both an $a$ transition to $\mathrm{STOP}$ and a CSP internal action to $a\to \mathrm{STOP}$. Its initial state is therefore not a CSP stable state, and its direct $a$ transition violates the property.

Nevertheless both have exactly the CSP traces $⟨⟩$ and $⟨a⟩$. Initially their possible stable observations offer exactly $a$, so their initial CSP stable failures are precisely $(⟨⟩,X)$ with $a\notin X$. After $a$, both can refuse every CSP event. Neither has a CSP divergence: the hidden $h$ can occur at most once. ThereforeNo CSP refinement test in one of these models can separate semantically equal operands. This also rules out placing the operand in a fixed context of ordinary CSP operators before the test, since those operators respect the model's equality. A model recording more about the interleaving of stability and acceptance, or an additional operator that explicitly observes stability, would be needed.

For a finite CSP trace $s$, let $L(s)$ be its sequence of values on $left$ and $O(s)$ its sequence of values on $right$, with channel names removed. Restrict the external alphabet to these two channels. The behavioural CSP trace specification for an unbounded FIFO buffer iswhere $⪯$ means prefix of a list, not merely subsequence. Outputs must therefore occur in input order, cannot duplicate or invent values, and cannot precede their inputs. Applying the condition to every CSP trace also checks every execution prefix.

For a legal $s$, write $L(s)=O(s)⌢q(s)$, so $q(s)$ is the pending FIFO queue content. Define the events that must remain available byIn addition to the CSP trace condition, require the behavioural CSP stable failure conditionThus an unbounded FIFO buffer cannot stably refuse any new input, and a nonempty FIFO buffer cannot stably refuse its oldest pending output. An empty FIFO buffer can refuse every output. Readiness of an input and readiness of an output are required together; the environment may choose either. These conditions do not require an output while the environment refuses to accept it. In a CSP failures-divergences model specification, also exclude CSP divergence; the stable-readiness condition alone does not rule out an implementation that loops internally forever without reaching a CSP stable state.

First define the ordinary unbounded FIFO buffer:Now use CSP internal choice to permit an immediate stop:An execution choosing the first branch can perform every legal CSP trace satisfying the prefix of a list condition in part (a). Conversely that condition excludes all other CSP traces, so no process satisfying it can have more CSP traces. The second branch adds no new CSP trace, since the empty CSP trace is already present.

The second branch does add the CSP stable failure $(⟨⟩,\{left.x\})$ for any $x\in T$. This violates mandatory input readiness. Therefore the process has the maximum possible CSP trace set and fails the CSP stable failure specification. The qualification is $T\ne \varnothing$, as is implicit for a useful FIFO buffer; with an empty value type there is no input-readiness event to violate. Maximizing the number of CSP traces does not pick a unique process in the finer models: other processes with the same complete legal CSP trace set and extra refusals also qualify.

If $f$ is injective, the equation is true:For a CSP event $a\in A$, the original CSP parallel composition permits $a$ exactly when both operands can perform $a$. After CSP event renaming, the corresponding rule requires the same image $f(a)$ in both operands. Injectivity ensures that matching images came from the same event, and that an event outside $A$ cannot acquire the image of one inside $A$. Independent transitions remain independent, and CSP internal actions are unchanged. Matching these transition rules gives a strong bisimulation, hence equality in all three standard CSP semantic models.

For a non-injective $f$, the equation need not hold. LetOn the left, both events require synchronization but the other operand offers the wrong event, so $P\underset{A}{\Vert }Q=\mathrm{STOP}$. On the right, both renamed operands offer $c$, which can synchronize:The failure is already visible in the CSP traces model. A particular non-injective CSP event renaming may still preserve a particular composition; it is the unrestricted equivalence that fails.

Write $J_A(P,Q)=P{△}_{A}Q$. The following five CSP operational semantics rules suffice, with $a$ always visible:Thus a CSP internal action of either operand preserves the wrapper. A visible action outside $A$ by the left operand also preserves it, whereas such an action by the right operand performs an ordinary CSP interrupt and discards the left operand. An action in $A$ requires both operands and advances both without discarding either. If both can perform the same event outside $A$, there are two transitions with the same visible label and potentially different derivatives; neither should be deleted. The paper excludes successful termination, so no extra termination rules are needed.

Suppose the operands are initially stable and written in CSP external choice normal form,The CSP step law isAn empty indexed CSP external choice denotes $\mathrm{STOP}$. A label appearing in both of the first two lines must retain both continuations: after that common label the result is the CSP internal choice between the continuations. A label in $A$ appears only in the third line and only if both operands offer it. These are exactly the three visible-transition rules from part (d); the two CSP internal action rules handle operands that are not initially stable.

As a check, for the paper's example the initial shared $a$ leads to $J_{\{a\}}(b\to \mathrm{STOP},c\to \mathrm{STOP})$. Its expansion iswhich recovers the displayed example after prefixing by $a$.

Use fresh event tags to tell apart an action by $P$ and an interrupting action by $Q$. Put $B=\Sigma \setminus A$ and introduce a disjoint copy $B^{\prime }=\{a^{\prime }:a\in B\}$. Let $f$ fix $A$ and map each $a\in B$ to $a^{\prime }$, and put $S=A\cup B^{\prime }$. Define a process that always accepts an event from $S$ byand an ordinary CSP interrupt handler byFinally let $g$ fix every original event and send $a^{\prime }$ back to $a$. A simulation containing no occurrence of the new operator isHere $△$ is the ordinary CSP interrupt, and the CSP event renaming $g$ is applied after the CSP parallel composition. It is non-injective, so part (c) explains why moving it inside would be unsafe.

Before the interrupt, $P$'s events in $A$ synchronize with $f(Q)$ on the same events. Its events outside $A$ are unprimed and do not synchronize with $f(Q)$. Meanwhile $Q$'s events outside $A$ are primed; they synchronize with $I$ and thereby interrupt and discard $P$. After the first such event, the left operand is $\mathrm{RUN}(S)$, so it imposes no further restriction on $f(Q)$; final CSP event renaming then yields exactly the remaining behaviour of $Q$.

For a formal strong bisimulation, relate a pre-interrupt state $J_A(P_0,Q_0)$ toand an already-interrupted state $Q_0$ toThe three visible cases match the rules in part (d), including both transitions when both operands offer the same event outside $A$. A CSP internal action of $Q_0$ never activates $I$, while a CSP internal action of $P_0$ remains possible exactly until the interrupt. The controller adds no CSP internal actions. Thus transitions match in both directions and related derivatives remain related.

Consequently this simulation is stronger than merely CSP trace equivalent:It preserves CSP stable states, their enabled-event sets and their CSP stable failures, and matches every possible infinite run of CSP internal actions. In particular, it introduces neither a premature commitment nor a new CSP divergence. A different simulation that guesses an interrupt with a hidden handshake would need a separate refusal analysis; the visible tagging construction above needs no hidden handshake.

Use the intended nontrivial ring network, with $N\ge 2$, and let $n\oplus 1=(n+1)\mathrm{mod}N$. A CSP event $ring.n.b$ is one synchronized transfer from the predecessor to receiver $n$, rather than a separate enqueue and dequeue. Let $s$ be the Boolean saying whether node $n$ is active. For $1\le n<N$, defineInitially the node is active:The CSP external choice in $\mathrm{Free}$ always offers both possible incoming message values as well as the permitted status change. Thus a decision to change status cannot internally withdraw readiness to receive a message. When the first message arrives, an active node forces its forwarded bit to false; an idle node preserves the bit. The status $s$ is retained until the second-round message has been forwarded. Neither the forwarding prefix nor $\mathrm{Second}$ offers status-change events, enforcing the protocol's freeze. On a false second-round message the node resumes its previous status; on a true one it forwards the bit before announcing shutdown.

The coordinator has the following states:ThusThe coordinator starts a round only while idle and sends true to node $1$. After the first returning message it sends exactly the received bit on the second round, without modifying it. The second return is required before its own shutdown; if the attempt failed it remains idle and may try again or become active. It offers no status-change event between starting and finishing the protocol. The two round states are essential: the first $ring.0.\mathrm{true}$ means that the first survey succeeded, whereas the next one acknowledges the circulating decision.

As in part (a), the choices between observable events are expressed using CSP external choice. Execution is nondeterministic, but there is no hidden irrevocable decision to become active while refusing a message. This keeps the readiness required by the question.

For each node letThe required CSP alphabetized parallel composition isEach message CSP event belongs to exactly the sender's and receiver's alphabets and synchronizes those two processes. A status signal belongs only to its own node. Using the common set of all message events as an all-node synchronization alphabet would be incorrect: unrelated nodes would then have to participate in each point-to-point transfer. The initial definitions in parts (a) and (b) make every node active. Keep the message CSP events visible here; later checks can apply CSP hiding as needed.

This is a safety property: a bad shutdown or a later reactivation has a finite bad CSP trace. Use the CSP traces model. Let $V=\{0,\dots ,N-1\}$, let $A\subseteq V$ track active nodes, and let $D\subseteq V$ track nodes that have announced shutdown. Let $\mathrm{Ring}$ contain every message CSP event. Define the following specification over the status-signal alphabet:Use the CSP refinement checkThe specification offers a shutdown only if the active set is empty, and offers no activation once $D$ is nonempty. A trace violating either requirement is therefore absent from the specification. Recording $D$ also prevents duplicate shutdowns and any status change by an already shut-down node. CSP hiding removes message details irrelevant to this finite bad-prefix check; a CSP traces model check alone does not assert eventual progress.

The system satisfies the check. After the first message has passed nodes $1,\dots ,i$, its bit is the Boolean conjunction of their being idle when sampled. Every sampled node is then frozen until it forwards the second-round decision. A true bit returning to node $0$ therefore means that every non-coordinator is idle and still frozen; the coordinator has itself remained idle. A true decision consequently reaches only idle nodes, each of which proceeds to shutdown rather than returning to $\mathrm{Free}$. No node can subsequently become active. A false decision permits no shutdown at all.

The trigger is specifically the first-round reception $ring.0.\mathrm{true}$. A CSP trace restriction cannot by itself guarantee progress after this event, because a finite prefix is compatible with both completion and an indefinitely delayed completion. We need to exclude both a stable refusal to continue and CSP divergence, so use the CSP failures-divergences model.

Here is an explicit conditional check that imposes no progress requirement before the trigger. Build the reachable labelled transition system of $\mathrm{System}$ and observe coordinator rounds with a two-phase monitor: it starts in the first-return phase and toggles on each $ring.0.b$. Collect the set $\mathcal{H}$ of system derivatives immediately after a true return in the first-return phase. This distinguishes the survey's return from the decision's return, without changing any system transitions. For fixed finite $N$, the set is finite. DefineHere $\sqcap$ denotes CSP internal choice. Perform the single CSP refinement checkEquivalently, check each post-trigger derivative $H$ individually against $\mathrm{Finish}(\varnothing )$ after the displayed CSP hiding. If the trigger is unreachable, the conditional property is vacuously true and there is no post-trigger check to perform.

The CSP internal choice in $\mathrm{Finish}$ deliberately permits any next shutdown, including an implementation that offers only one of the remaining shutdowns. It forbids a stable refusal of all remaining shutdowns, has no CSP divergence, and permits at most $N$ distinct shutdowns before $\mathrm{STOP}$. A CSP external choice over all remaining nodes would instead demand simultaneous readiness for every remaining shutdown and would unnecessarily reject the protocol's sequential delivery.

After hiding all other actions, endless internal work becomes a CSP divergence and a blocked unfinished state becomes a forbidden CSP stable failure. Since there are only $N$ possible shutdown actions and duplicates are excluded by CSP traces, every maximal progressing execution must complete all $N$. As usual for untimed CSP, this progress claim assumes the environment allows shutdown signals to occur; it supplies no wall-clock deadline. No fairness assumption requiring the coordinator eventually to initiate a survey has been smuggled into this conditional check.

For the defined system the check succeeds. Immediately after the trigger all statuses are idle and frozen. The only message work left is the second round: node $0$ sends the decision to node $1$, nodes $1$ through $N-1$ forward it, and node $0$ receives it. These are exactly $N$ more message transfers. Each node then has its one shutdown action, and the message can advance even while an earlier node's shutdown is pending. Thus there are no remaining status changes, no message cycle, and no unfinished global state in which every action is blocked. The measurestarts at $2N$, is nonnegative, and decreases on every subsequent transition. This excludes any hidden infinite run; before all shutdowns finish there is either an enabled message transfer or an enabled shutdown signal. The operational argument proves the conditional claim for every $N\ge 2$; finite state enumeration is only a supporting check.

For a general ring, no. Being idle at the instant the coordinator starts is not the same as remaining idle until sampled. A downstream node that has not yet received the first-round message is still in its $\mathrm{Free}$ state and may become active.

For a concrete $N=3$ example, first perform $idle.0,idle.1,idle.2$, so all nodes are idle. Then take this CSP trace:At the first displayed event the coordinator has started and all nodes are idle. Node $1$ has received true and is frozen, but node $2$ can still activate before receiving the token. It forwards false, so the entire second round carries false and nobody shuts down. After the final $idle.2$, all nodes are idle again. The coordinator may then perform $active.0,idle.0$ forever without starting another survey. This is an infinite execution with no shutdown and no assumption of fairness that would exclude it.

ThereforeThis does not contradict part (e): its stronger trigger, the true first-round return, never occurs in the failed survey. For the special $N=2$ ring, starting by $ring.1.\mathrm{true}$ already samples and freezes the only non-coordinator. If both nodes are idle at that event, this particular counterexample is impossible and the successful-survey progress argument applies. The general claim in the question must cover larger rings, where the unsampled downstream node exists.