Model checking a cache coherence protocol for a Java DSM implementation
Journal of Logic and Algebraic Programming , Volume 71 - Issue 1 p. 1- 43
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 $\mu$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.
|Journal of Logic and Algebraic Programming|
|Organisation||Software Analysis and Transformation|
Pang, J, Fokkink, W.J, Hofman, R, & Veldema, R. (2007). Model checking a cache coherence protocol for a Java DSM implementation. Journal of Logic and Algebraic Programming, 71(1), 1–43.