Abstract
A correctness proof of a variant of Segall's Propagation of Information with Feedback protocol is outlined. The proof, which is carried out within the I/O automata model of Lynch and Tuttle, is standard except for the use of a prophecy variable. The aim of this paper is to show that, unlike what has been suggested in the literature, assertional methods based on invariant reasoning support an intuitive way to think about and understand this algorithm.
The author was supported by Esprit BRA 7166 concur 2. This paper is dedicated to P.C. Baayen who, like the root node in Segall's algorithm, initiated a cascade of mathematical activity.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.
K.M. Chandy and J. Misra. Parallel Program Design. A Foundation. Addison-Wesley, 1988.
C.-T. Chou. Mechanical verification of distributed algorithms in higher-order logic. In T.F. Melham and J. Camilleri, editors, Proceedings 7 th International Workshop on Higher-Order Logic and its Applications, volume 859 of Lecture Notes in Computer Science, pages 158–176. Springer-Verlag, 1994. A revised version will appear in The Computer Journal, 1995.
C.-T. Chou. Practical use of the notions of events and causality in reasoning about distributed algorithms. CS Report #940035, UCLA, October 1994. Available via anonymous ftp at the URL ftp://ftp.cs.ucla.edu/pub/chou/nil.ps.
J.F. Groote and A. Ponse. Proof theory for μCRL: A language for processes with data. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors. Proceedings of the International Workshop on Semantics of Specification Languages, Workshops in Computer Science, pages 231–250. Springer-Verlag, 1993.
L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, editors, Proceedings International Workshop TYPES'93, Nijmegen, The Netherlands, May 1993, volume 806 of Lecture Notes in Computer Science, pages 127–165. Springer-Verlag, 1994. Full version available as Report CS-R9420, CWI, Amsterdam, March 1994.
B. Jonsson. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259–303, March 1994.
S.S. Lam and A.U. Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, 10(4):325–342, July 1984.
L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, 1983.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, March 1994.
P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory, Vienna, June 1968.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6 th Annual ACM Symposium on Principles of Distributed Computing, pages 137–151, August 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.
N.A. Lynch and M.R. Tuttle. An introduction to input/output automata. CWI Quarterly, 2(3):219–246, September 1989.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — part I: Untimed systems. Technical Memo MIT/LCS/TM-486.b (new version of TM-486), Laboratory for Computer Science, Massachusetts Institute of Technolog, Cambridge, MA, August 1994. To appear in Information and Computation.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.
T. Nipkow and K. Slind. I/O automata in Isabelle/HOL. In Proceedings International Workshop TYPES'94, Lecture Notes in Computer Science. Springer-Verlag, 1995. To appear.
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319–340, 1976.
A. Segall. Distributed network protocols. IEEE Transactions on Information Theory, IT-29(2):23–35, January 1983.
J. Søgaard-Andersen, S. Garland, J. Guttag, N.A. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In C. Courcoubetis, editor, Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece, volume 697 of Lecture Notes in Computer Science, pages 305–319. Springer-Verlag, 1993.
F.W. Vaandrager. Verification of a distributed summation algorithm. Report CS-R9505, CWI, Amsterdam, January 1995. A preliminary version appeared in K.R. Apt, A. Schrijver, N.M. Temme, editors, From Universal Morphisms to Megabytes — a Baayen Space Odyssey, pages 593–608, CWI, Amsterdam, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vaandrager, F. (1995). Verification of a distributed summation algorithm. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_14
Download citation
DOI: https://doi.org/10.1007/3-540-60218-6_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60218-7
Online ISBN: 978-3-540-44738-2
eBook Packages: Springer Book Archive