Model Checking a Cache Coherence Protocol for 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 discuss ractions 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.

• Type: Conference
• Year: 2003
• Where: IPPS
• Authors: Jun Pang, Wan Fokkink, Rutger F. H. Hofman, Ronald Veldema
• Keywords: Distributed And Parallel Computing, Distributed Memory System, Distributed Shared Memory, IPPS 2003, Java’s Memory Model