Using message passing for distributed programming: proof rules and disciplines

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using message passing for distributed programming: proof rules and disciplines

Full text

Pdf (1.66 MB)

Source

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

Pages: 402 - 431

Year of Publication: 1984

ISSN:0164-0925

Authors

Richard D. Schlichting	University of Arizona
Fred B. Schneider	Cornell University, Ithaca, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 26, Citation Count: 7

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/579.583 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	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 [doi>10.1145/357103.357110]
	2	BARRINC~:R, H., AND MEARNS, I. Axioms and proof rules for Ada tasks. IEE Proc. 129, Part E, 2 (Mar. 1982), 38-48.
	3	Per Brinch Hansen, Distributed processes: a concurrent programming concept, Communications of the ACM, v.21 n.11, p.934-941, Nov. 1978 [doi>10.1145/359642.359651]
	4	CLINT, M. Program proving: Coroutines. Acta lnl:. 2, i (1973), 50-63.
	5	Patrick Cousot , Radhia Cousot, Semantic Analysis of Communicating Sequential Processes (Shortened Version), Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.119-133, July 14-18, 1980
	6	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	7	Nissim Francez, Extended naming conventions for communicating processes, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-45, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582158]
	8	Rob Gerth, A sound and complete Hoare axiomatization of the Ada-rendezvous, Ninth colloquium on Automata, languages, and programming., p.252-264, January 2000, Aarhus, Denmark
	9	GERTH, R., AND DE ROEVER, W.P. A proof system for concurrent Ada programs. Tech. Rep. RUU-CS-83-2, Vakgroep Informatica, Rijksuniversiteit Utrecht, The Netherlands, Jan. 1983.
	10	Rob Gerth , Willem P. de Roever , Marly Roncken, Procedures and concurrency: A study in proof, Proceedings of the 5th Colloquium on International Symposium on Programming, p.132-163, April 06-08, 1982
	11	Donald I. Good , Richard M. Cohen , James Keeton-Williams, Principles of proving concurrent programs in Gypsy, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.42-52, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567757]
	12	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]
	13	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	14	HOARE, C.A.R. A calculus of total correctness for communicating processes. $ci. Comput. Prog. 1, (1981), 49-72.
	15	J. D. Ichbiah, Preliminary Ada reference manual, ACM SIGPLAN Notices, v.14 n.6a, p.1-145, June 1979 [doi>10.1145/956650.956651]
	16	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 [doi>10.1145/2993.357247]
	17	LEVIN, G., AND GRIES, D. Proof techniques for communicating sequential processes. Acta. In{. 15 (1981), 281-302.
	18	MISRA, J., AND CHANDY, K.M. Proofs of networks of processes. IEEE Trans. Softw. Eng. SE- 7, 4 (July 1981), 417-426.
	19	J. Misra , K. M. Chandy , Todd Smith, Proving safety and liveness of communicating processes with examples, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.201-208, August 18-20, 1982, Ottawa, Canada [doi>10.1145/800220.806698]
	20	MITCHELL, J.G., MAYBURY, W., AND SWEET, R. Mesa language manual (Version 5.0). Tech. Rep. CSL-79-3, Xerox Palo Alto Research Center, Palo Alto, Calif., 1979.
	21	OWlCKI, S., AND GRIES, D. An axiomatic proof technique for parallel programs I. Acta In{. 6 (1976), 319-340.
	22	SOUNDARARAJAN, N. Axiomatic semantics of communicating sequential processes. Tech. Rep., Dept. of Computer and Information Science, Ohio State Univ., Columbus, 1981.
	23	A. S. Tanenbaum, Computer networks, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988

CITED BY 7

	Wil Janssen, Refining knowledge oriented actions to layered implementations, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.91-100, May 23-26, 1996, Philadelphia, Pennsylvania, United States
	Richard D. Schlichting , Fred B. Schneider, Understanding and using asynchronous message passing (Preliminary Version), Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.141-147, August 18-20, 1982, Ottawa, Canada
	T. Camp , P. Kearns , M. Ahuja, Proof Rules for Flush Channels, IEEE Transactions on Software Engineering, v.19 n.4, p.366-378, April 1993
	Bernadette Charron-Bost , Friedemann Mattern , Gerard Tel, Synchronous, asynchronous, and causally ordered communication, Distributed Computing, v.9 n.4, p.173-191, February 1996
	Sigurd Meldal, A complete axiomatic semantics of spawning, Distributed Computing, v.5 n.3, p.159-174, December 1991
	Keith Shafer , Mohan Ahuja, Implementation of hierarchical F-channels for high-performance distributed computing, Distributed Computing, v.8 n.4, p.211-218, June 1995
	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