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.

,
North-Holland
Journal of Logic and Algebraic Programming
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.