loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
International Parallel and Distributed Processing Symposium (IPDPS'03)
Model Checking a Cache Coherence Protocol for a Java DSM Implementation
Nice, France
April 22-April 26
ISBN: 0-7695-1926-1
ASCII Text
x 
 
Jun Pang, Wan Fokkink, Rutger Hofman, Ronald Veldema, "Model Checking a Cache Coherence Protocol for a Java DSM Implementation," Parallel and Distributed Processing Symposium, International, pp. 238b, International Parallel and Distributed Processing Symposium (IPDPS'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/IPDPS.2003.1213433,
author = {Jun Pang and Wan Fokkink and Rutger Hofman and Ronald Veldema},
title = {Model Checking a Cache Coherence Protocol for a Java DSM Implementation},
journal ={Parallel and Distributed Processing Symposium, International},
volume = {0},
year = {2003},
issn = {1530-2075},
pages = {238b},
doi = {http://doi.ieeecomputersociety.org/10.1109/IPDPS.2003.1213433},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Parallel and Distributed Processing Symposium, International
TI - Model Checking a Cache Coherence Protocol for a Java DSM Implementation
SN - 1530-2075
SP
EP
A1 - Jun Pang,
A1 - Wan Fokkink,
A1 - Rutger Hofman,
A1 - Ronald Veldema,
PY - 2003
KW - µCRL
KW - model checking
KW - cache coherence protocols
KW - distributed shared memory
KW - Java
VL - 0
JA - Parallel and Distributed Processing Symposium, International
ER -
 
Jun Pang, CWI
Wan Fokkink, CWI and Vrije Universiteit
Rutger Hofman, Vrije Universiteit
Ronald Veldema, Vrije Universiteit
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.
Index Terms:
µCRL, model checking, cache coherence protocols, distributed shared memory, Java
Citation:
Jun Pang, Wan Fokkink, Rutger Hofman, Ronald Veldema, "Model Checking a Cache Coherence Protocol for a Java DSM Implementation," ipdps, pp.238b, International Parallel and Distributed Processing Symposium (IPDPS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.