Distributed mutual exclusion on a ring of processes (Q1060005)

A set of processes called 'masters' are sharing a critical section on a mutual exclusion basis. A master communicates only with its private 'server'. The servers communicate with each other in a ring. Three solutions for solving the mutual exclusion problem are presented. They all rely on the presence of a unique privilege in the ring. The notation used extends CSP input and output commands with a Boolean primitive, the 'probe', which makes it possible to determine whether a communication action is pending on a channel. In the correctness proofs, the concept of 'trace' is introduced, i.e. a total ordering of actions corresponding to a possible interleaving of the atomic actions of a concurrent computation.