Model checking a cache coherence protocol of a Java']Java DSM implementation

被引：12
|
作者：
Pang, Jun
Fokkink, Wan
Hofman, Rutger
Veldema, Ronald
机构：
[1] Carl von Ossietzky Univ Oldenburg, Dept Informat, D-26111 Oldenburg, Germany
[2] Vrije Univ Amsterdam, Afdeling Informat, NL-1081 HV Amsterdam, Netherlands
[3] Ctr Wiskunde & Informat, Software Engn Dept, NL-1098 SJ Amsterdam, Netherlands
[4] Univ Erlangen Nurnberg, Inst Informat, D-91058 Erlangen, Germany
来源：
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING | 2007年 / 71卷 / 01期
关键词：
formal specification; model checking; cache coherence protocols; !text type='Java']Java[!/text] memory model; mu CRL;
D O I：
10.1016/j.jlap.2006.08.007
中图分类号：
学科分类号：
摘要：
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. (C) 2006 Elsevier Inc. All rights reserved.
引用
收藏
页码：1 / 43
页数：43
相关论文
共 50 条
  • [1] Java']Java model checking
    Park, DYW
    Stern, U
    Skakkebæk, JU
    Dill, DL
    [J]. FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2000, : 253 - 256
  • [2] JaMP: an implementation of OpenMP for a Java']Java DSM
    Klemm, Michael
    Bezold, Matthias
    Veldema, Ronald
    Philippsen, Michael
    [J]. CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2007, 19 (18): : 2333 - 2352
  • [3] Communication protocol implementation in Java']Java
    Csopaki, G
    Horváth, GA
    Kovács, G
    [J]. INTERACTIVE DISTRIBUTED MULTIMEDIA SYSTEMS AND TELECOMMUNICATION SERVICES, PROCEEDINGS, 2000, 1905 : 254 - 265
  • [4] Model checking of software components: Combining Java']Java PathFinder and behavior protocol model checker
    Parizek, Pavel
    Plasil, Frantisek
    Kofron, Jan
    [J]. 30TH ANNUAL IEEE/NASA SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS, 2006, : 133 - +
  • [5] Model checking the Java']Java metalocking algorithm
    Basu, Samik
    Smolka, Scott A.
    [J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (03) : C1 - C35
  • [6] Model checking programs with Java']Java PathFinder
    Visser, W
    Mehlitz, P
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 27 - 27
  • [7] Applying model checking in Java']Java verification
    Havelund, K
    Skakkebæk, JU
    [J]. THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING, 1999, 1680 : 216 - 231
  • [8] An Approach to Checking Consistency between UML Class Model and Its Java']Java Implementation
    Chavez, Hector M.
    Shen, Wuwei
    France, Robert B.
    Mechling, Benjamin A.
    Li, Guangyuan
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2016, 42 (04) : 322 - 344
  • [9] Heuristic model checking for Java']Java programs
    Groce, A
    Visser, W
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 242 - 245
  • [10] Model checking real time Java']Java using Java']Java PathFinder
    Lindstrom, G
    Mehlitz, PC
    Visser, W
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 444 - 456
12345