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 条
  • [21] Research on Cache Coherence Protocol Verification Method Based on Model Checking
    Zhao, Yiqiang
    Shi, Boning
    Zhang, Qizhi
    Yuan, Yidong
    He, Jiaji
    [J]. ELECTRONICS, 2023, 12 (16)
  • [22] A JPSL Based Model Checking Approach for Java']Java Programs
    Shu, XinFeng
    Li, YanLin
    Gao, WeiRan
    [J]. STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2022, 2023, 13854 : 30 - 49
  • [23] Model Checking of Concurrent Algorithms: From Java']Java to C
    Artho, Cyrille
    Hagiya, Masami
    Leungwattanakit, Watcharin
    Tanabe, Yoshinori
    Yamamoto, Mitsuharu
    [J]. DISTRIBUTED, PARALLEL AND BIOLOGICALLY INSPIRED SYSTEMS, 2010, 329 : 90 - +
  • [24] Towards Model Checking of Computer Games with Java']Java PathFinder
    Shafiei, Nastaran
    van Breugel, Franck
    [J]. 2013 3RD INTERNATIONAL WORKSHOP ON GAMES AND SOFTWARE ENGINEERING: ENGINEERING COMPUTER GAMES TO ENABLE POSITIVE, PROGRESSIVE CHANGE (GAS), 2013, : 15 - 21
  • [25] A local approach for temporal model checking of Java']Java bytecode
    Santone, A
    Vaglini, G
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2005, 70 (02) : 258 - 281
  • [26] Software model checking for Internet Protocols with Java']Java Pathfinder
    Martinez, Jesss
    Jimenez, Cristobal
    [J]. MSVVEIS 2008: MODELLING, SIMULATION, VERIFICATION AND VALIDATION OF ENTERPRISE INFORMATION SYSTEMS, 2008, : 91 - 100
  • [27] Model checking real time Java using Java PathFinder
    Lindstrom, Gary
    Mehlitz, Peter C.
    Visser, Willem
    [J]. Lect. Notes Comput. Sci., (444-456):
  • [28] Java']Java implementation of an authentication protocol with application on mobile phones
    Groza, Bogdan
    Pop, Dragos
    Silea, Ioan
    [J]. 2008 IEEE INTERNATIONAL CONFERENCE ON AUTOMATION, QUALITY AND TESTING, ROBOTICS (AQTR 2008), THETA 16TH EDITION, VOL I, PROCEEDINGS, 2008, : 190 - +
  • [29] Implementation of the T=1 protocol based on Java']Java Card
    Ju, HI
    Han, JW
    [J]. 8TH WORLD MULTI-CONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL IV, PROCEEDINGS: INFORMATION SYSTEMS, TECHNOLOGIES AND APPLICATIONS: I, 2004, : 475 - 479
  • [30] Extended static checking for Java']Java
    Nelson, G
    [J]. MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, 2004, 3125 : 1 - 1
12345