Arbitration without common modifiable variables

Summary

The binary arbitration problem (or, the problem of mutual exclusion between two competitors) is the problem of preventing two competitors from simultaneously possessing the same token. A solution to this problem is presented together with a formal correctness proof. The solution is specific in that it combines the absence of common modifiable variables with the absence of auxiliary activities. Hence, its implementation does not require an arbiter on a lower level or a degree of concurrency of more than two. The solution is generalized for any arbitrary number of competitors by applying the binary solution in a binary arbitration tree.