Specification and Implementation of Mutual Exclusion
Per Brinch Hansen, J�rgen Staunstrup · IEEE Transactions on Software Engineering · 1978
This paper presents a constructive approach to the problem of specifying, implementing, and verifying operations that will give concurrent processes exclusive access to a resource. The method eliminates the need for auxiliary variables and establishes the correctness of a whole class of solutions to the same problem. The solutions are derived directly from the specifications using a language construct called guarded regions. Several new solutions to well-known exclusion problems are presented.