Sciweavers

JLP
2007

Model checking a cache coherence protocol of a Java DSM implementation

13 years 3 months ago
Model checking a cache coherence protocol of a Java DSM implementation
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 disabstractions 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. Key words: formal specification, model checking, cache coherence protocols, Java memory model, µCRL is the full version of an extended abstract that appeared in the Proceedings of the 8th Workshop on Formal Methods for Parallel Programming: Theory and Applications, IEEE Computer Society Press, 2003. The research is partly supported by the Dutch Technology Foundation STW under the project CES500...
Jun Pang, Wan Fokkink, Rutger F. H. Hofman, Ronald
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JLP
Authors Jun Pang, Wan Fokkink, Rutger F. H. Hofman, Ronald Veldema
Comments (0)