Model Checking a Cache Coherence Protocol for a Java DSM Implementation
Pang J, Fokkink W, Hofmann R, Veldema R (2003)
Publication Language: English
Publication Type: Conference contribution, Original article
Publication year: 2003
Publisher: IEEE
Pages Range: CDROM
Conference Proceedings Title: Proceedings of 17th International Parallel and Distributed Processing Symposium (IPDPS)
Event location: Nizza
ISBN: 0-7695-1926-1
URI: http://www2.informatik.uni-erlangen.de/publication/download/proto_proof.pdf
DOI: 10.1109/IPDPS.2003.1213433
Abstract
Jackal is a fine-grained distributed shared memory implementation of the Java programming language. It aims to implement Java's memory model and allows multithreaded Java programs to run unmodified on a distributed memory system. It employs a multiple-writer cache coherence protocol. In this paper, we report on our analysis of this protocol. We present its formal specification in μCRL, and discuss the abstractions that were made to avoid state explosion. Requirements were formulated and model checked with respect to several configurations. Our analysis revealed two errors in the implementation.
Authors with CRIS profile
Involved external institutions
Netherlands (NL)How to cite
APA:
Pang, J., Fokkink, W., Hofmann, R., & Veldema, R. (2003). Model Checking a Cache Coherence Protocol for a Java DSM Implementation. In Proceedings of 17th International Parallel and Distributed Processing Symposium (IPDPS) (pp. CDROM). Nizza, FR: IEEE.
MLA:
Pang, Jun, et al. "Model Checking a Cache Coherence Protocol for a Java DSM Implementation." Proceedings of the 8th International Workshop on Formal Methodes for Parallel Programming: Theory and Applications (FMPPTA), Nizza IEEE, 2003. CDROM.
BibTeX: Download