Abstract
The specification and verification of distributed systems calls for techniques tuned to the particular area of application. In this paper we introduce a specification and verification technique which exploits the order (causality) in which different events of distributed systems must occur. The technique is illustrated by applying it to a distributed shared memory system (DSM-system). We model a DSM-system by means of Petri net protocols for a DSM-system and prove that the executions of the protocols respect the specified ordering of events.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. K. Bennet, J.B. Carter, and W. Zwaenepoel. Munin: Distributed shared memory based on type-specific memory coherence. In 2nd ACM SIGPLAN Symposium on Principles and Practise of Parallel Programming. ACM, March 1990.
P.A. Bernstein and N. Goodman. Concurrency control in distributed database systems. ACM Computing Surveys, 13 (2): 185–221, June 1981.
Lothar Borrmann and Martin Herdieckershoff. A coherency model for virtually shared memory. In International Conference on Parallel Processing, August 1990.
Dominik Gomm and Ekkart Kindler. Causality based specification and correctness proof of a virtually shared memory scheme. SFB-Bericht 342/6/91 B, Technische Universität München, August 1991.
Dominik Gomm and Ekkart Kindler. A weakly coherent virtually shared memory scheme: Formal specification and analysis. SFB-Bericht 342/5/91 B, Technische Universität München, August 1991.
Herrmann Hellwagner. A survey of virtually shared memory schemes. SFB-Bericht 342/33/90 A, Technische Universität München, December 1990.
Kai Li and Paul Hudak. Memory coherence in shared virtual memory systems. ACM Transactions on Computer Systems, 7 (4): 321–359, November 1989.
Andreas Listl and Markus Pawlowski. Parallel cache management of RDBMS. SFB-Bericht 342/18/92 A, Technische Universität München, August 1992.
Wolfgang Reisig. Petri Nets, EATCS Monographs on Theoretical Computer Science, volume 4. Springer-Verlag, 1985.
Wolfgang Reisig. Petri nets and algebraic specifications. Theoretical Computer Science, 80: 1–34, May 1991.
A.J. Smith. Cache memories. ACM Computing Surveys, 14 (3): 473–530, September 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Gomm, D., Kindler, E. (1993). Causality Based Proof of a Distributed Shared Memory System. In: Bode, A., Dal Cin, M. (eds) Parallel Computer Architectures. Lecture Notes in Computer Science, vol 732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-21577-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-662-21577-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57307-4
Online ISBN: 978-3-662-21577-7
eBook Packages: Springer Book Archive