Model checking a cache coherence protocol of a Java DSM implementation

J. Pang, W.J. Fokkink, R. Hofman, R.S. Veldema

Research output: Contribution to JournalArticleAcademicpeer-review


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. © 2006 Elsevier Inc. All rights reserved.
Original languageEnglish
Pages (from-to)1-43
JournalJournal of Logic and Algebraic Programming
Issue number1
Publication statusPublished - 2007

Bibliographical note



Dive into the research topics of 'Model checking a cache coherence protocol of a Java DSM implementation'. Together they form a unique fingerprint.

Cite this