A New Approach to Proving the Correctness of Multiprocess Programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A New Approach to Proving the Correctness of Multiprocess Programs

Full text

Pdf (828 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 1 , Issue 1 (July 1979) table of contents

Pages: 84 - 97

Year of Publication: 1979

ISSN:0164-0925

Author

Leslie Lamport

SRI International, 333 Ravenswood Avenue, 415 Menlo Park, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 71, Citation Count: 19

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/357062.357068 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Irene Greif, A language for formal problem specification, Communications of the ACM, v.20 n.12, p.931-935, Dec. 1977 [doi>10.1145/359897.359904]
	2	Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
	3	LAMPORT, L. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. SE.3, 7 (March 1977), 125-143.
	4	Leslie Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, v.17 n.8, p.453-455, Aug. 1974 [doi>10.1145/361082.361093]
	5	Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
	6	Leslie Lamport, Concurrent reading and writing, Communications of the ACM, v.20 n.11, p.806-811, Nov. 1977 [doi>10.1145/359863.359878]
	7	Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]

CITED BY 19

	Frank D. Anger, On Lamport's interprocessor communication model, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.3, p.404-417, July 1989
	J. Misra, Axioms for memory access in asynchronous hardware systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.1, p.142-153, Jan. 1986
	George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985
	James H. Anderson, Lamport on mutual exclusion: 27 years of planting seeds, Proceedings of the twentieth annual ACM symposium on Principles of distributed computing, p.3-12, August 2001, Newport, Rhode Island, United States
	Leslie Lamport, The mutual exclusion problem: part I—a theory of interprocess communication, Journal of the ACM (JACM), v.33 n.2, p.313-326, April 1986
	Amy L. Lansky , Susan S. Owicki, GEM: A tool for concurrency specification and verification, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.198-212, August 17-19, 1983, Montreal, Quebec, Canada
	Michael J. Quinn , Narsingh Deo, Parallel graph algorithms, ACM Computing Surveys (CSUR), v.16 n.3, p.319-348, Sept. 1984
	Gregory R. Andrews, Parallel programs: proofs, principles, and practice, Communications of the ACM, v.24 n.3, p.140-145, March 1981
	Laura K. Dillon , George S. Avrunin , Jack C. Wileden, Constrained expressions: toward broad applicability of analysis methods for distributed software systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.374-402, July 1988
	Leslie Lamport, win and sin: predicate transformers for concurrency, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.396-428, July 1990
	Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada
	Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada
	James H. Anderson , Yong-Jik Kim , Ted Herman, Shared-memory mutual exclusion: major research trends since 1986, Distributed Computing, v.16 n.2-3, p.75-110, September 2003
	Uri Abraham, Self-stabilizing timestamps, Theoretical Computer Science, v.308 n.1-3, p.449-515, 3 November 2003
	Denis Gopan , Thomas Reps , Mooly Sagiv, A framework for numeric analysis of array operations, ACM SIGPLAN Notices, v.40 n.1, p.338-350, January 2005
	G.-C. Roman , K. C. Cox, A Declarative Approach to Visualizing Concurrent Computations, Computer, v.22 n.10, p.25-36, October 1989
	Leslie Lamport, How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor, IEEE Transactions on Computers, v.46 n.7, p.779-782, July 1997
	Lisa Higham , Lillanne Jackson , Jalal Kawash, Specifying memory consistency of write buffer multiprocessors, ACM Transactions on Computer Systems (TOCS), v.25 n.1, p.1-es, February 2007
	Sibsankar Haldar , K. Vidyasankar, On specification of Read/Write shared variables, Journal of the ACM (JACM), v.54 n.6, p.31-es, December 2007