Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/concurrency/3/a/solution

Use the intended nontrivial ring network, with , and let . A CSP event is one synchronized transfer from the predecessor to receiver , rather than a separate enqueue and dequeue. Let be the Boolean saying whether node is active. For , define
Initially the node is active:
The CSP external choice in 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 is retained until the second-round message has been forwarded. Neither the forwarding prefix nor 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.

New to topics? Read the docs here!