Abstract
The specification and verification of shared-memory multiprocessor cache coherence protocols is a paradigmatic example of parallel technologies where formal methods can be applied. In this paper we present the specification and verification of a cache protocol and a set of formalisms which are based on ‘process theory’. System correctness is not established by simple techniques such as testing and simulation, but ‘ensured’ in terms of the underlying formalism. In order to manipulate the specification and verify the properties we have used an automated tool —namely the ‘Edinburgh Concurrency Workbench’ (CWB).
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
Rance Cleaveland, Joachim Parrow, and Bernhard Steffen. The Concurrency Workbench. Technical Report ECS-LFCS-89-83, LFCS, Department of Computer Science, University of Edinburgh, 1989.
G. Delzanno. Automatic verification of parameterized cache coherence protocols. In Proceedings ofCAV’2000, vol. 1885 of LNCS, pages 53–68. Springer-Verlag, 2000.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. Technical Report CMU-CS-96-178, September 1996.
Matthew Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, 1988.
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
K.L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, School of Computer Science, CMU, May 1992.
Dexter Kozen. Results on the Propositional μ-Calculus. Theoretical Computer Science, 27(3):333–354, December 1983.
Ladkin, Lamport, Olivier, and Roegel. Lazy caching in TLA. Distributed Computing, 12, 1999.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
A.K. Nanda and L.N. Bhuyan. A formal specification and verification technique for cache coherence protocols. In Proceedings of the 1992 International Conference on Parallel Processing, pages 122–126, 1992.
Fong Pong and Michel Dubois. Verification techniques for cache coherence protocols. A CM Computing Surveys, 29(1):82–126, March 1997.
Per Stenström. A Survey of Cache Coherence Schemes for Multiprocessors. IEEE Computer, 23(6):12–24, June 1990.
C. Stirling. Modal and temporal logics for processes. Technical Report ECS-LFCS-92-221, LFCS, Dep. of Computer Science, University of Edinburgh, June 1992.
Colin Stirling. An introduction to modal and temporal logic for ccs. In Proc. 1989 UK/Japan Workshop on Concurrency, LNCS 491, pages 2–20. Springer 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barrio-Solórzano, M., Encarnación Beato, M., Cuesta, C.E., de la Fuente, P. (2001). Formal Verification of Coherence for a Shared Memory Multiprocessor Model. In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 2001. Lecture Notes in Computer Science, vol 2127. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44743-1_2
Download citation
DOI: https://doi.org/10.1007/3-540-44743-1_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42522-9
Online ISBN: 978-3-540-44743-6
eBook Packages: Springer Book Archive