Abstract
In this paper, we propose a technique for parallel composition of protocols. The technique allows an interleaved execution of the component protocols at a site. We give a sound and complete proof system for composing the partial correctness proofs of the component protocols to obtain a proof of the composite protocol. We first develop the technique for the case in which the component protocols are linear sequences of events. We then apply this technique in a hierarchical fashion to combine more complex protocols. We illustrate the use of this technique by designing a new protocol for breadth-first numbering.
This work was supported by NSF under grants CCR8701671 and CCR8901966.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Awerbuch, B. Complexity of network synchronization. JACM, 32(4), Oct. 1985.
Bouge, L. and Francez, N. A compositional approach to superimposition. In Proceedings of the ACM Symposium on Principles of Programming Languages, 1988.
Chandy, K. M. and Lamport, L. Distributed snapshots: Determining global states in distributed systems. ACM Transaction on Computing Systems, 3(1), July 1985.
Chandy, M. and Misra, J. Distributed computation on graphs: Shortest path algorithms. Communications of the ACM, 25(11), Nov. 1982.
Chandy, M. and Misra, J. Parallel program design. Addison-Weslay, 1988.
Chou, C.T. and Gafni, E. Understanding and verifying distributed algorithms using stratified decomposition. In Proceedings of the ACM Symposium on Principles of Distributed Computing, 1988.
Erland, T. and Francez, N. Decomposition of distributed programs into communication closed layers. Science of Computer Programming, 2, Dec. 1982.
Fix, L., Francez, N., and Grumberg, O. Semantics-driven decompositions of the verification of distributed programs. In Proceedings of the IFIP Working Group 2.2/2.3 Working Conference on Programming Concepts and Methods, 1990.
Gafni, E. Perspectives on distributed network protocols: A case study of building blocks. In Proceedings of MILCOM, 1986.
Gallager, R.G., Humblet, P.A., and Spira, P.M. A distributed algorithmfor minimal spanning tree. ACM Transaction on Programming Languages and Systems, 30(12), Dec. 1983.
Levin, G. and Gries, D. Proof techniques for communicating sequential processes. Acta Informatica, 15, 1981.
Owicki, S. and Gries, D. An axiomatic proof technique for parallel programs. Acta Informatica, 6, 1976.
Segall, A. Distributed network protocols. IEEE Transactions on Information Theory, 29, 1983.
Singh, G. Transformation and composition of distributed protocols. In Ph.D thesis, Department of Computer Science, SUNY, Stony Brook, 1991.
Stomp, F. and Roever, W. de. Designing distributed algorithms by means of formal sequentially phased reasoning. In Proceedings of the 3rd Int'l Workshop on Distributed Algorithms, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Singh, G., Bernstein, A.J. (1992). A framework for parallel composition of protocols. In: Etiemble, D., Syre, JC. (eds) PARLE '92 Parallel Architectures and Languages Europe. PARLE 1992. Lecture Notes in Computer Science, vol 605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55599-4_133
Download citation
DOI: https://doi.org/10.1007/3-540-55599-4_133
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55599-5
Online ISBN: 978-3-540-47250-6
eBook Packages: Springer Book Archive