Specifying Concurrent Program Modules

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Specifying Concurrent Program Modules

Full text

Pdf (2.03 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 5 , Issue 2 (April 1983) table of contents

Pages: 190 - 222

Year of Publication: 1983

ISSN:0164-0925

Author

Leslie Lamport

Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 82, Citation Count: 89

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/69624.357207 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	BOCHMANN, G., AND SUNSHINE, C. Formal methods in comnmnication protocol design. IEEE Trans. Commun. Com-28, 4 (Apr. 1980), 624-631.
	2	HAILPERN, B.T., AND OWICKI, S.S. Verifying network protocols using temporal logic. In Proceedings Trends and Applications 1980: Computer Network Protocols. IEEE Computer Society, 1980, pp. 18-28.
	3	Otthein Herzog, Static Analysis of Concurrent Processes for Dynamic Properties Using Petri Nets, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.66-90, July 02-04, 1979
	4	INTERNATIONAL ORGANIZATION FOR STANDARDIZATION TC97/SC16/WG1 SUBGROUP B ON STATE MACHINES. A FDT based on an extended state transition model. Working draft of tech. rep., Dec. 1981.
	5	LAMPORT, L. The "Hoare logic" of concurrent programs. Acta inf. 14, i (June 1980), 21-37.
	6	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]
	7	Leslie Lamport, Concurrent reading and writing, Communications of the ACM, v.20 n.11, p.806-811, Nov. 1977 [doi>10.1145/359863.359878]
	8	Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
	9	PNUELI, A. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, R.I., Oct. 31-Nov. 2, 1977, pp. 46-57.
	10	SCHWARTZ, R., AND MELLIAR-SMITH, P.M. From state machines to temporal logic: Specification methods for protocol standards. IEEE Trans. Commun. Corn-30, 11 (Nov. 1982).
	11	SCHWARTZ, R.L., AND MELLIAR-SMITH, P.M. Temporal logic specification of distributed systems. In Proceedings of the 2nd International Conference on Distributed Computing Systems. IEEE Computer Society Press, 1981, pp. 446-454.

CITED BY 89

	James Peters , William Hankley, Proving specifications of tasking systems using Ada/TL, Proceedings of the conference on TRI-ADA '90, p.4-13, December 03-06, 1990, Baltimore, Maryland, United States
	Maurice Herlihy, A methodology for implementing highly concurrent data objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.5, p.745-770, Nov. 1993
	A. Udaya Shankar, Verified data transfer protocols with variable flow control, ACM Transactions on Computer Systems (TOCS), v.7 n.3, p.281-316, Aug. 1989
	Ling Liu , Robert Meersman, The building blocks for specifying communication behavior of complex objects: an activity-driven approach, ACM Transactions on Database Systems (TODS), v.21 n.2, p.157-207, June 1996
	Nancy Lynch , Hagit Attiya, Using mappings to prove timing properties, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.265-280, August 22-24, 1990, Quebec City, Quebec, Canada
	A. Birrell , J. Guttag , J. Horning , R. Levin, Synchronization primitives for a multiprocessor: a formal specification, ACM SIGOPS Operating Systems Review, v.21 n.5, p.94-102, Nov. 1987
	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
	Martin Abadi , Gordon Plotkin, A logical view of composition and refinement, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.323-332, January 21-23, 1991, Orlando, Florida, United States
	Nils Klarlund , Mogens Nielsen , Kim Sunesen, Automated logical verification based on trace abstractions, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.101-110, May 23-26, 1996, Philadelphia, Pennsylvania, United States
	Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993
	Manfred Broy, Functional specification of time-sensitive communicating systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.1, p.1-46, Jan. 1993
	Thomas A. Henzinger , Orna Kupferman , Sriram K. Rajamani, Fair simulation, Information and Computation, v.173 n.1, p.64-81, February 25, 2002
	Nalini Venkatasubramanian , Carolyn Talcott, Reasoning about meta level activities in open distributed systems, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.144-152, August 20-23, 1995, Ottowa, Ontario, Canada
	M. Herlihy, A methodology for implementing highly concurrent data structures, ACM SIGPLAN Notices, v.25 n.3, p.197-206, Mar. 1990
	Jennifer L. Welch , Leslie Lamport , Nancy Lynch, A lattice-structured proof of a minimum spanning, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.28-43, August 15-17, 1988, Toronto, Ontario, Canada
	B. Jonsson, A fully abstract trace model for dataflow networks, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.155-165, January 11-13, 1989, Austin, Texas, United States
	Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984
	Michael Fisher , Clare Dixon , Martin Peim, Clausal temporal resolution, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.12-56, Jan. 2001
	Manfred Broy, Compositional refinement of interactive systems, Journal of the ACM (JACM), v.44 n.6, p.850-891, Nov. 1997
	Maurice P. Herlihy, Impossibility and universality results for wait-free synchronization, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.276-290, August 15-17, 1988, Toronto, Ontario, Canada
	Philippas Tsigas , Yi Zhang, A simple, fast and scalable non-blocking concurrent FIFO queue for shared memory multiprocessor systems, Proceedings of the thirteenth annual ACM symposium on Parallel algorithms and architectures, p.134-143, July 2001, Crete Island, Greece
	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
	Oscar Nierstrasz , Michael Papathomas, Viewing object as patterns of communicating agents, ACM SIGPLAN Notices, v.25 n.10, p.38-43, Oct. 1990
	Maurice Herlihy, Wait-free synchronization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.1, p.124-149, Jan. 1991
	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
	C. Huizing , R. Gerth , W. P. deRoever, Full abstraction of a real-time denotational semantics for an OCCAM-like language, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.223-236, January 21-23, 1987, Munich, West Germany
	Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada
	Leslie Lamport, The mutual exclusion problem: partII—statement and solutions, Journal of the ACM (JACM), v.33 n.2, p.327-348, April 1986
	Rob Gerth, Transition logic: How to reason about temporal properties in a compositional way, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.39-50, December 1984
	A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993
	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
	Greg Barnes, A method for implementing lock-free shared-data structures, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.261-270, June 30-July 02, 1993, Velen, Germany
	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
	Maged M. Michael , Michael L. Scott, Simple, fast, and practical non-blocking and blocking concurrent queue algorithms, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.267-275, May 23-26, 1996, Philadelphia, Pennsylvania, United States
	Hagit Brit , Shlomo Moran, Wait-freedom vs. bounded wait-freedom in public data structures (extended abstract), Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.52-60, August 14-17, 1994, Los Angeles, California, United States
	Maurice P. Herlihy , J. E. B. Moss, Lock-free garbage collection for multiprocessors, Proceedings of the third annual ACM symposium on Parallel algorithms and architectures, p.229-236, July 21-24, 1991, Hilton Head, South Carolina, United States
	Orna Kupferman , Moshe Y. Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.87-128, Jan. 2000
	Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989
	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
	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994
	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
	Yehuda Afek , Dalia Dauber , Dan Touitou, Wait-free made fast, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.538-547, May 29-June 01, 1995, Las Vegas, Nevada, United States
	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
	Martin D. Fraser , Kuldeep Kumar , Vijay K. Vaishnavi, Strategies for incorporating formal specifications in software development, Communications of the ACM, v.37 n.10, p.74-86, Oct. 1994
	S. Prakash , Yann Hang Lee , T. Johnson, A Nonblocking Algorithm for Shared Queues Using Compare-and-Swap, IEEE Transactions on Computers, v.43 n.5, p.548-559, May 1994
	Hagit Brit , Shlomo Moran , Gadi Taubenfeld, Public data structures: counters as a special case, Theoretical Computer Science, v.289 n.1, p.401-423, 23 October 2002
	M. Agrawala , D. L. Jain, Comments on 'Temporal Logic-Based Deadlock Analysis for Ada' by G.M. Karam and R.J.A. Burh, IEEE Transactions on Software Engineering, v.19 n.2, p.198-199, February 1993
	Theodore Johnson, Characterizing the Performance of Algorithms for Lock-Free Objects, IEEE Transactions on Computers, v.44 n.10, p.1194-1207, October 1995
	Cristina Videira Lopes , Paul Dourish , David H. Lorenz , Karl Lieberherr, Beyond AOP: toward naturalistic programming, ACM SIGPLAN Notices, v.38 n.12, December 2003
	R. Kurki-Suonio, Action systems in incremental and aspect-oriented modeling, Distributed Computing, v.16 n.2-3, p.201-217, September 2003
	Jeannette M. Wing, Beyond functional behavior: combining methods to specify different classes of properties of large systems, ACM SIGSOFT Software Engineering Notes, v.10 n.4, August 1985
	A. Udaya Shankar , Simon S. Lam, A stepwise refinement heuristic for protocol construction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.3, p.417-461, July 1992
	M. G. Staskauskas, Formal Derivation of Concurrent Programs: An Example from Industry, IEEE Transactions on Software Engineering, v.19 n.5, p.503-528, May 1993
	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
	M. P. Herlihy , J. E. B. Moss, Lock-Free Garbage Collection for Multiprocessors, IEEE Transactions on Parallel and Distributed Systems, v.3 n.3, p.304-311, May 1992
	Ichiro Suzuki, Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets, IEEE Transactions on Software Engineering, v.16 n.11, p.1273-1281, November 1990
	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
	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
	Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999
	Daniel L. Rosenband , Arvind, Modular scheduling of guarded atomic actions, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
	Arcot Sowmya , S. Ramesh, Extending Statecharts with Temporal Logic, IEEE Transactions on Software Engineering, v.24 n.3, p.216-231, March 1998
	Rob Strom , Shaula Yemini, The NIL distributed systems programming language: a status report, ACM SIGPLAN Notices, v.20 n.5, May 1985
	Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990
	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
	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
	Nancy A. Lynch , Hagit Attiya, Using mappings to prove timing properties, Distributed Computing, v.6 n.2, p.121-139, September 1992
	Shlomi Dolev , Frank Stomp, Safety assurance via on-line monitoring, Distributed Computing, v.16 n.4, p.269-277, December 2003
	Gregor Gössler , Joseph Sifakis, Composition for component-based modeling, Science of Computer Programming, v.55 n.1-3, p.161-183, March 2005
	Bengt Jonsson , Amir Pnueli , Camilla Rump, Proving refinement using transduction, Distributed Computing, v.12 n.2/3, p.129-149, June 1999
	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
	Riccardo Pucella, Logical verification and equational verification, ACM SIGACT News, v.36 n.2, June 2005
	Jacob Brunekreef , Joost-Pieter Katoen , Ron Koymans , Sjouke Mauw, Design and analysis of dynamic leader election protocols in broadcast networks, Distributed Computing, v.9 n.4, p.157-171, February 1996
	Mark Moir , Daniel Nussbaum , Ori Shalev , Nir Shavit, Using elimination to implement scalable and lock-free FIFO queues, Proceedings of the seventeenth annual ACM symposium on Parallelism in algorithms and architectures, July 18-20, 2005, Las Vegas, Nevada, USA
	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
	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
	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
	Guojing Cong , David A. Bader, Designing irregular parallel algorithms with mutual exclusion and lock-free protocols, Journal of Parallel and Distributed Computing, v.66 n.6, p.854-866, June 2006
	John Giacomoni , Tipp Moseley , Manish Vachharajani, FastForward for efficient pipeline parallelism: a cache-optimized concurrent lock-free queue, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, February 20-23, 2008, Salt Lake City, UT, USA
	Leslie Lamport, What it means for a concurrent program to satisfy a specification: why no one has specified priority, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.78-83, 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
	Ling Liu , Robert Meersman, Activity Model: A Declarative Approach for Capturing Communication Behavior in Object-Oriented Databases, Proceedings of the 18th International Conference on Very Large Data Bases, p.481-493, August 23-27, 1992
	Manfred Broy, A Functional Rephrasing of the Assumption/Commitment Specification Style, Formal Methods in System Design, v.13 n.1, p.87-119, May 1, 1998
	Massimo Franceschet , Angelo Montanari , Maarten De Rijke, Model Checking for Combined Logics with an Application to Mobile Systems, Automated Software Engineering, v.11 n.3, p.289-321, June 2004
	Guoping Jia , Guoliang Zheng, Fair transition system specification: an integrated approach, ACM SIGPLAN Notices, v.31 n.3, p.14-21, March 1996
	John Giacomoni , John K. Bennett , Antonio Carzaniga , Douglas C. Sicker , Manish Vachharajani , Alexander L. Wolf, Frame shared memory: line-rate networking on commodity hardware, Proceedings of the 3rd ACM/IEEE Symposium on Architecture for networking and communications systems, December 03-04, 2007, Orlando, Florida, USA
	Albert Benveniste , Benoît Caillaud , Luca P. Carloni , Paul Caspi , Alberto L. Sangiovanni-Vincentelli, Composing heterogeneous reactive systems, ACM Transactions on Embedded Computing Systems (TECS), v.7 n.4, p.1-36, July 2008
	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
	Junchang Wang , Haipeng Cheng , Bei Hua , Xinan Tang, Practice of parallelizing network applications on multi-core architectures, Proceedings of the 23rd international conference on Supercomputing, June 08-12, 2009, Yorktown Heights, NY, USA