Model checking a cache coherence protocol of a Java DSM implementation

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

doi:10.1016/j.jlap.2006.08.007

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 Journal › Article › Academic › peer-review

Abstract

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 language	English
Pages (from-to)	1-43
Journal	Journal of Logic and Algebraic Programming
Volume	71
Issue number	1
DOIs	https://doi.org/10.1016/j.jlap.2006.08.007
Publication status	Published - 2007

Bibliographical note

DBLP:journals/jlp/PangFHV07

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1016/j.jlap.2006.08.007

Persistent URL (handle)

Persistent link

Cite this

@article{49e0e2b2b2dd4c8196ed338355a43318,

title = "Model checking a cache coherence protocol of a Java DSM implementation",

abstract = "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. {\textcopyright} 2006 Elsevier Inc. All rights reserved.",

author = "J. Pang and W.J. Fokkink and R. Hofman and R.S. Veldema",

note = "DBLP:journals/jlp/PangFHV07 ",

year = "2007",

doi = "10.1016/j.jlap.2006.08.007",

language = "English",

volume = "71",

pages = "1--43",

journal = "Journal of Logic and Algebraic Programming",

issn = "1567-8326",

publisher = "Elsevier Inc.",

number = "1",

}

TY - JOUR

T1 - Model checking a cache coherence protocol of a Java DSM implementation

AU - Pang, J.

AU - Fokkink, W.J.

AU - Hofman, R.

AU - Veldema, R.S.

N1 - DBLP:journals/jlp/PangFHV07

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1016/j.jlap.2006.08.007

DO - 10.1016/j.jlap.2006.08.007

M3 - Article

SN - 1567-8326

VL - 71

SP - 1

EP - 43

JO - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

IS - 1

ER -

Model checking a cache coherence protocol of a Java DSM implementation

Abstract

Bibliographical note

UN SDGs

Access to Document

Persistent URL (handle)

Fingerprint

Cite this