Verifying properties of parallel programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

Verifying properties of parallel programs: an axiomatic approach

Full text

Pdf (676 KB)

Source

Communications of the ACM archive
Volume 19 , Issue 5 (May 1976) table of contents

Pages: 279 - 285

Year of Publication: 1976

ISSN:0001-0782

Authors

Susan Owicki	Cornell Univ., Ithaca, NY
David Gries	Cornell Univ., Ithaca, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 142, Citation Count: 79

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/360051.360224 What is a DOI?

ABSTRACT

An axiomatic method for proving a number of properties of parallel programs is presented. Hoare has given a set of axioms for partial correctness, but they are not strong enough in most cases. This paper defines a more powerful deductive system which is in some sense complete for partial correctness. A crucial axiom provides for the use of auxiliary variables, which are added to a parallel program as an aid to proving it correct. The information in a partial correctness proof can be used to prove such properties as mutual exclusion, freedom from deadlock, and program termination. Techniques for verifying these properties are presented and illustrated by application to the dining philosophers problem.

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	Per Brinch Hansen, Concurrent Programming Concepts, ACM Computing Surveys (CSUR), v.5 n.4, p.223-245, Dec. 1973 [doi>10.1145/356622.356624]
	2	Cook, S. A. Axiomatic and interpretive semantics for an Algol fragment. Tech. Rep. 79, Dep. of Computer Sci., U. of Toronto, 1975.
	3	Gries, D. An exercise in proving properties of parallel programs. Lecture notes, Technical U. Munich.
	4	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	5	C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
	6	Hoare, C.A.R. Towards a theory of parallel programming. In Operating Systems Techniques, Hoare and Perott (Eds.), Academic Press, New York, 1972.
	7	Hugh Conrad Lauer, Correctness in operating systems, 1973
	8	Manna, Z. and Pnueli, A. Axiomatic approach to total correctness of programs. Acta lnformatica 3 (1974), 243-263.
	9	Susan Speer Owicki, Axiomatic proof techniques for parallel programs., 1975

CITED BY 79

	Ashok R. Saxena , Thomas H. Bredt, Verification of a monitor specification, Proceedings of the 2nd international conference on Software engineering, p.53-59, October 13-15, 1976, San Francisco, California, United States
	John Howard , Shmuel Katz, Reconciliations, Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.14-21, August 14-17, 1994, Los Angeles, California, United States
	Michael J. Quinn , Narsingh Deo, Parallel graph algorithms, ACM Computing Surveys (CSUR), v.16 n.3, p.319-348, Sept. 1984
	J. P. Benson , S. H. Saib, A software quality assurance experiment, ACM SIGSOFT Software Engineering Notes, v.3 n.5, p.87-91, November 1978
	Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993
	Krzysztof R. Apt, Formal Justification of a Proof System for Communicating Sequential Processes, Journal of the ACM (JACM), v.30 n.1, p.197-216, Jan. 1983
	Thomas W. Doeppner, Jr., Parallel program correctness through refinement, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.155-169, January 17-19, 1977, Los Angeles, California
	Paul Ammann , Sushil Jajodia , Indrakshi Ray, Applying formal methods to semantic-based decomposition of transactions, ACM Transactions on Database Systems (TODS), v.22 n.2, p.215-254, June 1997
	Laura K. Dillon, Verifying General Safety Properties of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.16 n.1, p.51-63, January 1990
	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
	Krithivasan Ramamritham , Robert M. Keller, Specifying and proving properties of sentinel processes, Proceedings of the 5th international conference on Software engineering, p.374-382, March 09-12, 1981, San Diego, California, United States
	Laura K. Dillon, Using symbolic execution for verification of Ada tasking programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.4, p.643-669, Oct. 1990
	Jonathan S. Ostroff, Composition and refinement of discrete real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.1, p.1-48, Jan. 1999
	Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980
	Jorge V. Phillips , Thomas H. Bredt, Design and verification of real-time systems, Proceedings of the 2nd international conference on Software engineering, p.124-131, October 13-15, 1976, San Francisco, California, United States
	M. P. Herlihy , J. M. Wing, Axioms for concurrent objects, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.13-26, January 21-23, 1987, Munich, West Germany
	Leslie Lamport, A New Approach to Proving the Correctness of Multiprocess Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.84-97, July 1979
	David P. Reed , Rajendra K. Kanodia, Synchronization with eventcounts and sequencers, Communications of the ACM, v.22 n.2, p.115-123, Feb. 1979
	Edmund Melson Clarke, Jr., Synthesis of resource invariants for concurrent programs, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.211-221, January 29-31, 1979, San Antonio, Texas
	Brain A. Rudolph, Self-assessment procedure XXI: a self-assessment procedure on concurrency, Communications of the ACM, v.33 n.5, p.563-576, May 1990
	D. Garlan , S. Jha , D. Notkin , J. Dingel, Reasoning about implicit invocation, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.209-221, Nov. 1998
	Gregory R. Andrews, Parallel programs: proofs, principles, and practice, Communications of the ACM, v.24 n.3, p.140-145, March 1981
	Brent Hailpern , Susan Owicki, Modular verification of concurrent programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.322-336, January 25-27, 1982, Albuquerque, Mexico
	Gregory R. Andrews , Fred B. Schneider, Concepts and Notations for Concurrent Programming, ACM Computing Surveys (CSUR), v.15 n.1, p.3-43, March 1983
	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
	Krzysztof Kuchcinski , Bogdan Wiszniewski, Path analysis of distributed programs, Proceedings of the 1988 ACM sixteenth annual conference on Computer science, p.320-328, February 1988, Atlanta, Georgia, United States
	Daniel Schwabe, Formal specification and verification of a connection establishment protocol, ACM SIGCOMM Computer Communication Review, v.11 n.4, p.11-26, October 1981
	Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990
	A. Moitra , S. S. Iyengar , F. B. Bastani , I. L. Yen, Multilevel Data Structures: Models and Performance, IEEE Transactions on Software Engineering, v.14 n.6, p.858-867, June 1988
	W. Damm, A Microprogramming Logic, IEEE Transactions on Software Engineering, v.14 n.5, p.559-574, May 1988
	Jerome A. Feldman, High level programming for distributed computing, Communications of the ACM, v.22 n.6, p.353-368, June 1979
	Simon S. Lam , A. Udaya Shankar, A Relational Notation for State Transition Systems, IEEE Transactions on Software Engineering, v.16 n.7, p.755-775, July 1990
	Tilak Agerwala , Yong-Chai Choed-Amphai, A synthesis rule for concurrent systems, Proceedings of the 15th conference on Design automation, p.305-311, June 19-21, 1978, Las Vegas, Nevada, United States
	D. E. Shasha , A. Pnueli , W. Ewald, Temporal verification of carrier-sense local area network protocols, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-65, January 15-18, 1984, Salt Lake City, Utah, United States
	J. W. de Bakker , J. I. Zucker, Denotational semantics of concurrency, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.153-158, May 05-07, 1982, San Francisco, California, United States
	Scott D. Carson , Paul F. Reynolds, Jr., The geometry of semaphore programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.1, p.25-53, Jan. 1987
	Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990
	Jeannette M. Wing , Mark R. Nixon, Extending Ina Jo with Temporal Logic, IEEE Transactions on Software Engineering, v.15 n.2, p.181-197, February 1989
	Franklyn T. Bradshaw , George W. Ernst , Raymond J. Hookway, Use of data abstraction in process specification, ACM SIGSOFT Software Engineering Notes, v.7 n.3, p.16-21, July 1982
	Michael F. Kilian, A conditional critical region pre-processor for C based on the Owicki and Gries scheme, ACM SIGPLAN Notices, v.20 n.4, April 1985
	Barry K. Rosen, Applications of high level control flow, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-47, January 17-19, 1977, Los Angeles, California
	Awadhesh Kumar Singh , Anup Kumar Bandyopadhyay, Verifying mutual exclusion and liveness properties with split preconditions, Journal of Computer Science and Technology, v.19 n.6, p.795-802, November 2004
	Viktor Vafeiadis , Maurice Herlihy , Tony Hoare , Marc Shapiro, Proving correctness of highly-concurrent linearisable objects, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA
	Doug Goldson , Brijesh Dongol, Concurrent program design in the extended theory of Owicki and Gries, Proceedings of the 2005 Australasian symposium on Theory of computing, p.41-50, January 01, 2005, Newcastle, Australia
	B. Meandzija, Archetype: A Unified Method for the Design and Implementation of Protocol Architectures, IEEE Transactions on Software Engineering, v.14 n.6, p.822-837, June 1988
	C. Mohan, Survey of recent operating systems research, designs and implementations, ACM SIGOPS Operating Systems Review, v.12 n.1, p.53-89, January 1978
	J. C. M. Baeten, A brief history of process algebra, Theoretical Computer Science, v.335 n.2-3, p.131-146, 23 May 2005
	Gudmund Grov, Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	Piotr Nienaltowski, Efficient data race and deadlock prevention in concurrent object-oriented programs, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
	A. P. Moore, The Specification and Verified Decomposition of System Requirements Using CSP, IEEE Transactions on Software Engineering, v.16 n.9, p.932-948, September 1990
	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
	R. K. Shyamsundar , J. W. Thatcher, Language Constructs for Specifying Concurrency in CDL, IEEE Transactions on Software Engineering, v.15 n.8, p.977-993, August 1989
	K. Culik, On formal and informal proofs for program correctness, ACM SIGPLAN Notices, v.18 n.1, p.23-28, January 1983
	Magne Haveraaen, Machine and collection abstractions for user-implemented data-parallel programming, Scientific Programming, v.8 n.4, p.231-246, December 2000
	C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983
	N. Soundararajan, Axiomatic semantics of communicating sequential processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.647-662, Oct. 1984
	Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, May, 2007
	Alexey Gotsman , Josh Berdine , Byron Cook , Mooly Sagiv, Thread-modular shape analysis, ACM SIGPLAN Notices, v.42 n.6, June 2007
	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
	Beverly A. Sanders , KyungHee Kim, Assertional reasoning about data races in relaxed memory models, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, February 20-23, 2008, Salt Lake City, UT, USA
	Georges Gardarin , Michel A. Melkanoff, Proving consistency of database transactions, Proceedings of the fifth international conference on Very Large Data Bases, p.291-298, October 03-05, 1979, Rio de Janeiro, Brazil
	Stephen Brookes, A semantics for concurrent separation logic, Theoretical Computer Science, v.375 n.1-3, p.227-270, May, 2007
	Cengiz Erbas , Murat M. Tanik, Modeling And Verification Of Real-Time Systems, Journal of Integrated Design & Process Science, v.7 n.3, p.11-37, August 2003
	Edmund Clarke, Jr., Synthesis of Resource Invariants for Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.338-358, July 1980
	Paul Ammann , Sushil Jajodia , Indrakshi Ray, Using Formal Methods to Reason about Semantics-Based Decompositions of Transactions, Proceedings of the 21th International Conference on Very Large Data Bases, p.218-227, September 11-15, 1995
	David M. Goldschlag, A Mechanization of Unity in PC-NQTHM-92, Journal of Automated Reasoning, v.23 n.3, p.445-498, November 1999
	Aleksandar Nanevski , Paul Govereau , Greg Morrisett, Towards type-theoretic semantics for transactional concurrency, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA
	Mark-Oliver Stehr, Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types Interpretation, Fundamenta Informaticae, v.82 n.4, p.311-340, February 2008
	Sandip Ray , Warren A. Hunt, Jr. , John Matthews , J. Strother Moore, A Mechanical Analysis of Program Verification Strategies, Journal of Automated Reasoning, v.40 n.4, p.245-269, May 2008
	Nels E. Beckman , Kevin Bierhoff , Jonathan Aldrich, Verifying correct usage of atomic blocks and typestate, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Ali Ebnenasir , Rasoul Beik, Developing parallel programs: A design-oriented perspective, Proceedings of the 2009 ICSE Workshop on Multicore Software Engineering, p.1-8, May 18-18, 2009
	Thomas Ridge, Verifying distributed systems: the operational approach, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Tayfun Elmas , Shaz Qadeer , Serdar Tasiran, A calculus of atomic actions, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Ariel Cohen , Kedar S. Namjoshi, Local proofs for global safety properties, Formal Methods in System Design, v.34 n.2, p.104-125, April 2009
	Yinghai Lu , Hai Zhou , Li Shang , Xuan Zeng, Multicore parallel min-cost flow algorithm for CAD applications, Proceedings of the 46th Annual Design Automation Conference, July 26-31, 2009, San Francisco, California
	Masahiro Hirata , Toshio Nishimura, A prover for parallel processes, Proceedings of the 6th international joint conference on Artificial intelligence, p.384-389, August 20-23, 1979, Tokyo, Japan
	Jacob Burnim , Koushik Sen, Asserting and checking determinism for multithreaded programs, Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, August 24-28, 2009, Amsterdam, The Netherlands
	Mark A. Hillebrand , Dirk C. Leinenbach, Formal Verification of a Reader-Writer Lock Implementation in C, Electronic Notes in Theoretical Computer Science (ENTCS), 254, p.123-141, October, 2009
	N. R. Hall , S. Preiser, Combined network complexity measures, IBM Journal of Research and Development, v.28 n.1, p.15-27, January 1984

INDEX TERMS

Keywords:
concurrent processes, correctness proofs, deadlock, mutual exclusion, program verification, structured multiprogramming, synchronization

Collaborative Colleagues:

Susan Owicki: colleagues

David Gries: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player