Reduction

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Reduction: a method of proving properties of parallel programs

Full text

Pdf (453 KB)

Source

Communications of the ACM archive
Volume 18 , Issue 12 (December 1975) table of contents

Pages: 717 - 721

Year of Publication: 1975

ISSN:0001-0782

Author

Richard J. Lipton

Yale Univ., New Haven, CT

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 36, Downloads (12 Months): 131, Citation Count: 53

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

ABSTRACT

When proving that a parallel program has a given property it is often convenient to assume that a statement is indivisible, i.e. that the statement cannot be interleaved with the rest of the program. Here sufficient conditions are obtained to show that the assumption that a statement is indivisible can be relaxed and still preserve properties such as halting. Thus correctness proofs of a parallel system can often be greatly simplified.

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	Ashcroft, E.A. Proving assertions about parallel programs. Research Rep. CS-73-01, Dep. of Applied Analysis and Computer Sci., U. of Waterloo, 1973.
	2	Dijkstra, E.W. Cooperating sequential processes. In ProgrammingLanguages, F. Genuys (Ed.), Academic Press, 1968, pp. 43- 112.
	3	Floyd, R.W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Amer. Math. Soc., 1967, pp. 19-32.
	4	A. Nico Habermann, Synchronization of communicating processes, Communications of the ACM, v.15 n.3, p.171-176, March 1972 [doi>10.1145/361268.361277]
	5	Hugh Conrad Lauer, Correctness in operating systems, 1973
	6	Levitt, K.N, The application of program proving techniques to the verification of synchronization processes. AFIPS Conf. Proc., Vol. 41, Part 1, 1972 Fall Joint Computer Conference, AFIPS Press, Montvale, N.J., 1972, pp. 33-47.

CITED BY 53

	Eugene W. Stark, Semaphore primitives and starvation-free mutual exclusion, Journal of the ACM (JACM), v.29 n.4, p.1049-1072, Oct. 1982
	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
	Abraham Silberschatz, Serializability in multi-level monitor environments, Proceedings of the 1978 annual conference, p.855-861, January 1978
	Cormac Flanagan , Shaz Qadeer, Types for atomicity, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004
	Kaisa Sere , Marina Waldén, Verification of a distributed algorithm (abstract), Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.391, August 14-17, 1994, Los Angeles, California, United States
	Thomas W. Doeppner, Jr., On abstractions of parallel programs, Proceedings of the eighth annual ACM symposium on Theory of computing, p.65-72, May 03-05, 1976, Hershey, Pennsylvania, United States
	Paolo A. G. Sivilotti, A class of synchronization systems that permit the use of large atomic blocks, Proceedings of the 1998 conference of the Centre for Advanced Studies on Collaborative research, p.21, November 30-December 03, 1998, Toronto, Ontario, Canada
	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994
	Ratan Nalumasu , Ganesh Gopalakrishnan, An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation, Formal Methods in System Design, v.20 n.3, p.231-247, May 2002
	Ratan Nalumasu , Ganesh Gopalakrishnan, Deriving Efficient Cache Coherence Protocols Through Refinement, Formal Methods in System Design, v.20 n.1, p.107-125, January 2002
	Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Ernie Cohen, Asynchronous progress, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
	Jayadev Misra, A reduction theorem for concurrent object-oriented programs, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
	Liqiang Wang , Scott D. Stoller, Accurate and efficient runtime detection of atomicity errors in concurrent programs, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA
	Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, ACM SIGPLAN Notices, v.39 n.1, p.245-255, January 2004
	Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, ACM SIGPLAN Notices, v.39 n.1, p.256-267, January 2004
	Toshimi Minoura , S. Sitharama Iyengar, Data and Time Abstraction Techniques for Analyzing Multilevel Concurrent Systems, IEEE Transactions on Software Engineering, v.15 n.1, p.47-59, January 1989
	Gregor Bochmann, Delay-Independent Design for Distributed Systems, IEEE Transactions on Software Engineering, v.14 n.8, p.1229-1237, August 1988
	Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Rushikesh K. Joshi , Subash Rajaa, Modeling VP operation: the Diwali Festival Problem, ACM SIGOPS Operating Systems Review, v.39 n.2, p.51-53, April 2005
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting purity for atomicity, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Hans W. Barz, Implementing semaphores by binary semaphores, ACM SIGPLAN Notices, v.18 n.2, p.39-45, February 1983
	Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA
	Wim H. Hesselink, Eternity variables to prove simulation of specifications, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.175-201, January 2005
	J. Plosila , K. Sere , M. Waldén, Asynchronous system synthesis, Science of Computer Programming, v.55 n.1-3, p.259-288, March 2005
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting Purity for Atomicity, IEEE Transactions on Software Engineering, v.31 n.4, p.275-291, April 2005
	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
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005
	Liqiang Wang , Scott D. Stoller, Static analysis of atomicity for programs with non-blocking synchronization, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA
	Stephen F. Siegel , George S. Avrunin, Modeling wildcard-free MPI programs for verification, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA
	Rahul Agarwal , Amit Sasturkar , Liqiang Wang , Scott D. Stoller, Optimized run-time race detection and atomicity checking using partial discovered types, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	Michael F. Ringenburg , Dan Grossman, AtomCaml: first-class atomicity via rollback, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Mandana Vaziri , Frank Tip , Julian Dolby, Associating synchronization constraints with data in an object-oriented language, ACM SIGPLAN Notices, v.41 n.1, p.334-345, January 2006
	Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, ACM SIGPLAN Notices, v.41 n.6, June 2006
	W. F. Ogden , W. E. Riddle , W. C. Round, Complexity of expressions allowing concurrency, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.185-194, January 23-25, 1978, Tucson, Arizona
	Wim H. Hesselink, Simulation Refinement for Concurrency Verification, Electronic Notes in Theoretical Computer Science (ENTCS), 214, p.3-23, June, 2008
	Lindsay Groves, Verifying Michael and Scott's lock-free queue algorithm using trace reduction, Proceedings of the fourteenth symposium on Computing: the Australasian theory, January 01-01, 2008, Wollongong, NSW, Australia
	Scott D. Stoller , Ernie Cohen, Optimistic synchronization-based state-space reduction, Formal Methods in System Design, v.28 n.3, p.263-289, May 2006
	Byron Cook , Andreas Podelski , Andrey Rybalchenko, Proving thread termination, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Bohuslav Krena , Zdenek Letko , Rachel Tzoref , Shmuel Ur , Tomáš Vojnar, Healing data races on-the-fly, Proceedings of the 2007 ACM workshop on Parallel and distributed systems: testing and debugging, July 09-09, 2007, London, United Kingdom
	Martin Büchi , Emil Sekerinski, A Foundation for Refining Concurrent Objects, Fundamenta Informaticae, v.44 n.1-2, p.25-61, January 2000
	Cormac Flanagan , Stephen N. Freund , Marina Lifshin , Shaz Qadeer, Types for atomicity: Static checking and inference for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-53, July 2008
	Cormac Flanagan , Stephen N. Freund , Jaeheon Yi, Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Scott D. Stoller , Ping Yang , C R. Ramakrishnan , Mikhail I. Gofman, Efficient policy analysis for administrative role based access control, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA
	Christian Hammer , Julian Dolby , Mandana Vaziri , Frank Tip, Dynamic detection of atomic-set-serializability violations, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Cormac Flanagan , Stephen N. Freund, Atomizer: A dynamic atomicity checker for multithreaded programs, Science of Computer Programming, v.71 n.2, p.89-109, April, 2008
	Lindsay Groves, Trace-based Derivation of a Lock-Free Queue Algorithm, Electronic Notes in Theoretical Computer Science (ENTCS), 201, p.69-98, March, 2008
	Chang-Seo Park , Koushik Sen, Randomized active atomicity violation detection in concurrent programs, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Nels E. Beckman , Kevin Bierhoff , Jonathan Aldrich, Verifying correct usage of atomic blocks and typestate, ACM SIGPLAN Notices, v.43 n.10, September 2008
	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
	Liqiang Wang , Scott D. Stoller, Runtime Analysis of Atomicity for Multithreaded Programs, IEEE Transactions on Software Engineering, v.32 n.2, p.93-110, February 2006