A New Approach to Proving the Correctness of Multiprocess Programs
- 1 January 1979
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 1 (1), 84-97
- https://doi.org/10.1145/357062.357068
Abstract
A new, nonassertional approach to proving multiprocess program correctness is described by proving the correctness of a new algorithm to solve the mutual exclusion problem. The algorithm is an improved version of the bakery algorithm. It is specified and proved correct without being decomposed into indivisible, atomic operations. This allows two different implementations for a conventional, nondistributed system. Moreover, the approach provides a sufficiently general specification of the algorithm to allow nontrivial implementations for a distributed system as well.Keywords
This publication has 6 references indexed in Scilit:
- Time, clocks, and the ordering of events in a distributed systemCommunications of the ACM, 1978
- A language for formal problem specificationCommunications of the ACM, 1977
- Concurrent reading and writingCommunications of the ACM, 1977
- Formal verification of parallel programsCommunications of the ACM, 1976
- Verifying properties of parallel programsCommunications of the ACM, 1976
- A new solution of Dijkstra's concurrent programming problemCommunications of the ACM, 1974