Proving Liveness Properties of Concurrent Programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Proving Liveness Properties of Concurrent Programs

Full text

Pdf (2.13 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 4 , Issue 3 (July 1982) table of contents

Pages: 455 - 495

Year of Publication: 1982

ISSN:0164-0925

Authors

Susan Owicki	Computer Systems Laboratory, Stanford Electronics Laboratories, Department of Electrical Engineering, Stanford University, Stanford, CA
Leslie Lamport	Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 91, Citation Count: 97

Additional Information:

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

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	BURSTALL, R.M. Program proving as hand simulation with a little induction. In Information Processing 74, Stockholm, 1974, pp. 308-312.
	2	Edsger W. Dijkstra, The structure of the “THE”-multiprogramming system, Communications of the ACM, v.11 n.5, p.341-346, May 1968 [doi>10.1145/363095.363143]
	3	FLON, L., AND SUZUKI, N. The total correctness of parallel programs. SIAM J. Comput. 10, 2 (May 1981), 227-246.
	4	FRANCEZ, N., AND PNUELI, A. A proof method for cyclic programs. Acta inf. 9, 2 (1978), 133- 158.
	5	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]
	6	HAREL, D., KOZEN, D., AND PARIKH, R. Process logic: Expressiveness, decidability, completeness. In Proceedings of the 21st Symposium on the Foundations of Computer Science, IEEE, Syracuse, N.Y., Oct. 1980, pp. 129-142.
	7	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]
	8	Yat-Sang Kwong, On the Absence of Livelocks in Parallel Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.172-190, July 02-04, 1979
	9	LAMPORT, L. The "Hoare logic" of concurrent programs. Acta Inf. 14, I (1980), 21-37.
	10	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 [doi>10.1145/567446.567463]
	11	LAMPORT, L. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE- 3, 2 (Mar. 1977), 125-143.
	12	Richard J. Lipton, On synchronization primitive systems, 1973
	13	Zohar Manna , Richard Waldinger, Is “sometime” sometimes better than “always”?: intermittent assertions in proving program correctness, Communications of the ACM, v.21 n.2, p.159-172, Feb. 1978 [doi>10.1145/359340.359353]
	14	OWlCKX, S., AND GRIt. S, D. An axiomatic proof technique for parallel programs. Acta Inf. 6, 4 (1976), 319-340.
	15	Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
	16	PNVr. LI, A. The temporal logic of programs. In Proceedings of the 18th Symposium on the Foundations of Computer Science, IEEE, Providence, Nov. 1977, pp. 46-57.
	17	V. R. Pratt, Process logic: preliminary report, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.93-100, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567761]
	18	PRATT, V.R. Semantical considerations on Floyd-Hoare logic. In 17th Symposium on Foundations of Computer Science, IEEE, Houston, Tex., Oct. 1976, pp. 109-121.

CITED BY 97

	C. S. Jutla , E. Knapp , J. R. Rao, A predicate transformer approach to semantics of parallel programs, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.249-263, June 1989, Edmonton, Alberta, Canada
	Leslie Lamport, Reasoning about nonatomic operations, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.28-37, January 24-26, 1983, Austin, Texas
	Michael J. Quinn , Narsingh Deo, Parallel graph algorithms, ACM Computing Surveys (CSUR), v.16 n.3, p.319-348, Sept. 1984
	Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992
	Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States
	Ching Tsun Chou , Eli Gafni, Understanding and verifying distributed algorithms using stratified decomposition, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.44-65, August 15-17, 1988, Toronto, Ontario, Canada
	Joylyn Reed , Raymond T. Yeh, Specification and verification of liveness properties of cyclic, concurrent processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.1, p.156-177, Jan. 1988
	Paris C. Kanellakis , Scott A. Smolka, On the analysis of cooperation and antagonism in networks of communicating processes, Proceedings of the fourth annual ACM symposium on Principles of distributed computing, p.23-38, August 1985, Minaki, Ontario, Canada
	Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993
	Paul K. Harter, Jr., Response times in level-structured systems, ACM Transactions on Computer Systems (TOCS), v.5 n.3, p.232-248, Aug. 1987
	Richard Alan Karp, Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.239-253, April 1984
	E. A. Emerson , T. Sadler , J. Srinivasan, Efficient temporal reasoning (extended abstract), Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-178, January 11-13, 1989, Austin, Texas, United States
	Allen Emerson , Jai Srinivasan, A decidable temporal logic to reason about many processes, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.233-246, August 22-24, 1990, Quebec City, Quebec, Canada
	Pierpaolo Degano , Ugo Montanari, Liveness properties as convergence in metric spaces, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.31-38, December 1984
	M. G. Gouda , C. K. Chang, A technique for proving liveness of communicating finite state machines with examples, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.38-49, August 27-29, 1984, Vancouver, British Columbia, Canada
	Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas
	Zohar Manna , Amir Pnueli, A hierarchy of temporal properties (invited paper, 1989), Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.377-410, August 22-24, 1990, Quebec City, Quebec, Canada
	Shmuel Katz , Gadi Taubenfeld, What processes know: Definitions and proof methods, Proceedings of the fifth annual ACM symposium on Principles of distributed computing, p.249-262, August 11-13, 1986, Calgary, Alberta, Canada
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	C. H. Kung, On verification of database temporal constraints, ACM SIGMOD Record, v.14 n.4, p.169-179, May 1985
	Leslie Lamport, The mutual exclusion problem: partII—statement and solutions, Journal of the ACM (JACM), v.33 n.2, p.327-348, April 1986
	Paul C. Attie, Liveness-preserving simulation relations, Proceedings of the eighteenth annual ACM symposium on Principles of distributed computing, p.63-72, May 04-06, 1999, Atlanta, Georgia, United States
	Bengt Jonsson, Compositional specification and verification of distributed systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.2, p.259-303, March 1994
	Sanjai Narain , Jeff Rothenberg, Proving temporal properties of hybrid systems, Proceedings of the 22nd conference on Winter simulation, p.250-256, December 09-12, 1990, New Orleans, Louisiana, United States
	Ernst-Rüdiger Olderog , Krzysztof R. Apt, Fairness in parallel programs: the transformational approach, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.420-455, July 1988
	E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986
	Leslie Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems (TOCS), v.5 n.1, p.1-11, Feb. 1987
	Amir Pnueli, On the extremely fair treatment of probabilistic algorithms, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.278-290, December 1983
	K. R. Apt , N. Francez , S. Katz, Appraising fairness in distributed languages, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.189-198, January 21-23, 1987, Munich, West Germany
	Joseph Y. Halpern, A little knowledge goes a long way: simple knowledge-based derivations and correctness proofs for a family of protocols, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.269-280, August 10-12, 1987, Vancouver, British Columbia, Canada
	David Harel, On visual formalisms, Communications of the ACM, v.31 n.5, p.514-530, May 1988
	Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983
	A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993
	Paul F. Reynolds, Jr. , Craig Williams , Raymond R. Wagner, Jr., Isotach Networks, IEEE Transactions on Parallel and Distributed Systems, v.8 n.4, p.337-348, April 1997
	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
	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986
	Bowen Alpern , Fred B. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.147-167, Jan. 1989
	Amir Pnueli , Lenore Zuck, Verification of multiprocess probabilistic protocols, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.12-27, August 27-29, 1984, Vancouver, British Columbia, Canada
	Joseph Y. Halpern , Lenore D. Zuck, A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols, Journal of the ACM (JACM), v.39 n.3, p.449-478, July 1992
	Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989
	Martín Abadi , Zohar Manna, Nonclausal deduction in first-order temporal logic, Journal of the ACM (JACM), v.37 n.2, p.279-317, April 1990
	Angelo Morzenti , Pierluigi San Pietro, Object-oriented logical specification of time-critical systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.1, p.56-98, Jan. 1994
	V. Carchiolo , A. Di Stefano , A. Faro , G. Pappalardo, ECCS and LIPS: two languages for OSI systems specification and verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.2, p.284-329, April 1989
	Ana R. Cavalli, A method of automatic proof for the specification and verification of protocols, ACM SIGCOMM Computer Communication Review, v.14 n.2, p.100-106, June 1984
	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
	Shlomit S. Pinter , Pierre Wolper, A temporal logic for reasoning about partially ordered computations (Extended Abstract), Proceedings of the third annual ACM symposium on Principles of distributed computing, p.28-37, August 27-29, 1984, Vancouver, British Columbia, Canada
	Krithivasan Ramamritham, Resource controller tasks in ADA: Their structure and semantics, Proceedings of the 7th international conference on Software engineering, p.67-76, March 26-29, 1984, Orlando, Florida, United States
	Tom Henzinger , Zohar Manna , Amir Pnueli, Temporal proof methodologies for real-time systems, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.353-366, January 21-23, 1991, Orlando, Florida, United States
	Mohammed G. Gouda , Chung-Kuo Chang, Proving liveness for networks of communicating finite state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.1, p.154-180, Jan. 1986
	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
	Bengt Jonsson, Modular verification of asynchronous networks, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.152-166, August 10-12, 1987, Vancouver, British Columbia, Canada
	Cristina Videira Lopes , Paul Dourish , David H. Lorenz , Karl Lieberherr, Beyond AOP: toward naturalistic programming, Companion of the 18th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 26-30, 2003, Anaheim, CA, USA
	Salvatore La Torre , Margherita Napoli, Finite automata on timed ω-trees, Theoretical Computer Science, v.293 n.3, p.479-505, 9 February 2003
	Panagiotis Manolios , Richard Trefler, A lattice-theoretic characterization of safety and liveness, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.325-333, July 13-16, 2003, Boston, Massachusetts
	Cristina Videira Lopes , Paul Dourish , David H. Lorenz , Karl Lieberherr, Beyond AOP: toward naturalistic programming, ACM SIGPLAN Notices, v.38 n.12, December 2003
	Rajeev Alur , Thomas A. Henzinger, A really temporal logic, Journal of the ACM (JACM), v.41 n.1, p.181-203, Jan. 1994
	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
	Richard D. Schlichting , Fred B. Schneider, Fail-stop processors: an approach to designing fault-tolerant computing systems, ACM Transactions on Computer Systems (TOCS), v.1 n.3, p.222-238, August 1983
	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
	G. Balbo , G. Chiola , S. C. Bruell , P. Chen, An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm, IEEE Transactions on Parallel and Distributed Systems, v.3 n.2, p.221-240, March 1992
	Edgar Knapp, An exercise in the formal derivation of parallel programs: maximum flows in graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.203-223, April 1990
	Ichiro Suzuki , Harngdar Lu, Temporal Petri Nets and Their Application to Modeling and Analysis of a Handshake Daisy Chain Arbiter, IEEE Transactions on Computers, v.38 n.5, p.696-704, May 1989
	Paul W. King, Formalization of Protocol Engineering Concepts, IEEE Transactions on Computers, v.40 n.4, p.387-403, April 1991
	Che-Fn Yu , V. D. Gligor, A Specification and Verification Method for Preventing Denial of Service, IEEE Transactions on Software Engineering, v.16 n.6, p.581-592, June 1990
	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
	Gerald M. Karam , Raymond J. A. Buhr, Temporal Logic-Based Deadlock Analysis for Ada, IEEE Transactions on Software Engineering, v.17 n.10, p.1109-1125, October 1991
	Christos N. Nikolaou , Edmund M. Clarke , Nissim Francez , Stephen A. Schuman, A methodology for verifying request processing protocols, ACM SIGCOMM Computer Communication Review, v.13 n.2, April 1983
	Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
	Joseph Y. Halpern, A note on knowledge-based programs and specifications, Distributed Computing, v.13 n.3, p.145-153, July 2000
	G. Manduchi , M. Moro, Automatic verification for a class of distributed systems, Distributed Computing, v.13 n.3, p.127-143, July 2000
	Boutheina Chetali, Formal Verification of Concurrent Programs Using the Larch Prover, IEEE Transactions on Software Engineering, v.24 n.1, p.46-62, January 1998
	Arcot Sowmya , S. Ramesh, Extending Statecharts with Temporal Logic, IEEE Transactions on Software Engineering, v.24 n.3, p.216-231, March 1998
	Howard Barringer , Ruurd Kuiper , Amir Pnueli, A really abstract concurrent model and its temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.173-183, January 01, 1986, St. Petersburg Beach, Florida
	Ronald Fagin , Joseph Y. Halpern , Yoram Moses , Moshe Y. Vardi, Knowledge-based programs, Distributed Computing, v.10 n.4, p.199-225, July 1997
	Rajeev Alur , Gadi Taubenfeld, Fast timing-based algorithms, Distributed Computing, v.10 n.1, p.1-10, July 1996
	Shmuel Katz , Doron Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing, v.6 n.2, p.107-120, September 1992
	Simon S. Lam , A. Udaya Shankar, Specifying modules to satisfy interfaces: a state transition system approach, Distributed Computing, v.6 n.1, p.39-63, July 1992
	Luc Moreau , Peter Dickman , Richard Jones, Birrell's distributed reference listing revisited, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1344-1395, November 2005
	Pradeep Jain , Simon S. Lam, Specification of Real-Time Broadcast Networks, IEEE Transactions on Computers, v.40 n.4, p.404-422, April 1991
	Keith Marzullo , Laura S. Sabel, Efficient detection of a class of stable properties, Distributed Computing, v.8 n.2, p.81-91, October 1994
	Hugh C. Lauer, Long computations, Proceedings of the 3rd workshop on ACM SIGOPS European workshop: Autonomy or interdependence in distributed systems?, p.1-4, September 18-21, 1988, Cambridge, United Kingdom
	H. Gao , J. F. Groote , W. H. Hesselink, Lock-free parallel and concurrent garbage collection by mark&sweep, Science of Computer Programming, v.64 n.3, p.341-374, February, 2007
	Arun Kejariwal , Hideki Saito , Xinmin Tian , Milind Girkar , Wel Li , Utpal Banerjee , Alexandru Nicolau , Constantine D. Polychronopoulos, Lightweight lock-free synchronization methods for multithreading, Proceedings of the 20th annual international conference on Supercomputing, June 28-July 01, 2006, Cairns, Queensland, Australia
	Karun N. Biyani , Sandeep S. Kulkarni, Assurance of dynamic adaptation in distributed systems, Journal of Parallel and Distributed Computing, v.68 n.8, p.1097-1112, August, 2008
	Stephen Brookes, A semantics for concurrent separation logic, Theoretical Computer Science, v.375 n.1-3, p.227-270, May, 2007
	E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States
	Van Nguyen , David Gries , Susan Owicki, A model and temporal proof system for networks of processes, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.121-131, January 14-16, 1985, New Orleans, Louisiana, United States
	Leslie Lamport , Fred B. Schneider, Constraints: a uniform approach to aliasing and typing, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.205-216, January 14-16, 1985, New Orleans, Louisiana, United States
	Clare Dixon, Temporal resolution using a breadth-first search, Annals of Mathematics and Artificial Intelligence, v.22 n.1-2, p.87-115, 1998
	David Chenho Kung, A Temporal Framework for Database Specification and Verification, Proceedings of the 10th International Conference on Very Large Data Bases, p.91-99, August 27-31, 1984
	Z. Manna , A. Pnueli, Specification and verification of concurrent programs by A∀automata, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-2, January 21-23, 1987, Munich, West Germany
	Anup Kumar Bandyopadhyay, Modeling fairness and starvation in concurrent systems, ACM SIGSOFT Software Engineering Notes, v.32 n.6, November 2007
	Anup Kumar Bandyopadhyay, Weakest precondition based verification tool that models spatial ordering, ACM SIGSOFT Software Engineering Notes, v.33 n.2, March 2008
	Anup Kumar Bandyopadhyay, Fairness and conspiracy concepts in concurrent systems, ACM SIGSOFT Software Engineering Notes, v.34 n.2, March 2009
	Claudia Szabo , Yong Meng Teo, An Approach for Validation of Semantic Composability in Simulation Models, Proceedings of the 2009 ACM/IEEE/SCS 23rd Workshop on Principles of Advanced and Distributed Simulation, p.3-10, June 22-25, 2009