Abstract
The majority consensus algorithm of Thomas [Thom79] for concurrency control in multiple copy databases is proved correct, using system-wide invariants. The specification of the algorithm is extended to a more formal and more complete form. It is shown that the algorithm as given by Thomas does not guarantee internal consistency, but that a slightly modified form does. We also describe a modification in which votes need not be remembered.
Preview
Unable to display preview. Download preview PDF.
References
Ceri, S., and G. Pelagatti: Distributed Databases. Principles and systems. McGraw-Hill Book Company, London,1985.
Drost, N.J., and J. van Leeuwen: Assertional verification of a Majority Consensus Algorithm for Concrrency control in Multiple Copy Databases. Techn. Rep. RUU-CS-88-13, Dept. of Computer Science, University of Utrecht, Utrecht. 1988.
Drost, N.J., and A.A. Schoone: Assertional Verification of a Reset Algorithm. Techn. Rep. RUU-CS-88-5, Dept. of Computer Science, University of Utrecht, Utrecht. 1988.
Jonsson,B.: Modular Verification of Asynchronous Networks. Proc. 6th Annual ACM Symp. on Principles of Distributed Computing, Vancouver, pp. 152–166, 1987.
Knuth, D.E.: Verification of Link-Level Protocols. BIT 21:31–36. 1981.
Krogdahl, S.: Verification of a Class of Link-Level Protocols. BIT 18:436–448. 1978.
Lamport, L.: An Assertional Correctness Proof of a Distributed Algorithm. Science of Computer Programming 2:175–206. 1982.
Schoone, A.A.: Verification of Connection-Management Protocols. Techn. Rep. RUU-CS-87-14, Dept. of Computer Science, University of Utrecht, Utrecht. 1987.
Schoone, A.A. and J. van Leeuwen: Verification of Balanced Link-Level Protocols. Techn. Rep. RUU-CS-85-12, Dept. of Computer Science, University of Utrecht, Utrecht. 1985. (Revised version to appear in BIT).
Tel, G.: Assertional Verification of a Timer-based Protocol. Techn. Rep. RUU-CS-87-15, Dept. of Computer Science, University of Utrecht, Utrecht. 1987.
Thomas, R.H.: A Majority Consensus Approach to Concurrency Control for Multiple Copy Databases. ACM Trans. on Database Systems 4,2:180–209,1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drost, N.J., van Leeuwen, J. (1988). Assertional verification of a majority consensus algorithm for concurrency control in multiple copy databases. In: Vogt, F.H. (eds) CONCURRENCY 88. CONCURRENCY 1988. Lecture Notes in Computer Science, vol 335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50403-6_48
Download citation
DOI: https://doi.org/10.1007/3-540-50403-6_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50403-0
Online ISBN: 978-3-540-45999-6
eBook Packages: Springer Book Archive