Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 3

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.