Issue No.05 - September (1978 vol.4)
P.B. Hansen , Department of Computer Science, University of Southern California
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.
transition commands, Concurrent programs, guarded regions, mutual exclusion, program implementation, program specification, program verification
P.B. Hansen, "Specification and Implementation of Mutual Exclusion", IEEE Transactions on Software Engineering, vol.4, no. 5, pp. 365-370, September 1978, doi:10.1109/TSE.1978.233856