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

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.