Processing math: 100%
We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 21 Issue 5
September  2006
Turn off MathJax
Article Contents
Abstract
References
Hong Pan, Hui-Min Lin, Yi Lv. Model Checking Data Consistency for Cache Coherence Protocols[J]. Journal of Computer Science and Technology, 2006, 21(5): 765-775.
Citation: Hong Pan, Hui-Min Lin, Yi Lv. Model Checking Data Consistency for Cache Coherence Protocols[J]. Journal of Computer Science and Technology, 2006, 21(5): 765-775.
shu

Model Checking Data Consistency for Cache Coherence Protocols

  • Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, P.R. China

More Information
  • Received Date: June 04, 2006
  • Revised Date: August 14, 2006
  • Published Date: September 14, 2006
    Abstract
  • A method for automatic verification of cache coherence protocols ispresented, in which cache coherence protocols are modeled asconcurrent value-passing processes, and control and data consistencyrequirement are described as formulas in first-order μ-calculus.A model checker is employed to check if the protocol underinvestigation satisfies the required properties. Using this method adata consistency error has been revealed in a well-known cachecoherence protocol. The error has been corrected, and the revisedprotocol has been shown free from data consistency error for anydata domain size, by appealing to data independence technique.
    • FullText(HTML)
    • References (17)
  • [1]
    Baukus K, Lakhnech Y, Stahl K. Parameterized verification of a cache coherence protocol: Safety and liveness. In -\it Proc. VMCAI'02}, Venice, Italy, LNCS 2294, Springer-Verlag, 2002, pp.317--330.
    [2]
    Chou C T, Mannava P K, Park S. A simple method for parameterized verification of cache coherence protocols. In -\it FMCAD'04}, Austin, Texas, USA, LNCS 3312, Springer-Verlag, 2004, pp.382--398.
    [3]
    Pnueli A, Ruah S, Zuck L. Automatic deductive verification with invisible invariants. In -\it TACAS'01}, Genova, Italy, LNCS 2031, Springer-Verlag, 2001, pp.82--97.
    [4]
    Lahiri S K, Bryant R. Indexed predicate discovery for unbounded system verification. In -\it CAV'04}, Boston, Massachusetts, USA, LNCS 3114, Springer-Verlag, 2004, pp.135--147.
    [5]
    Emerson E A, Lahon V. Exact and efficient verification of parameterized cache coherence protocols. In -\it CHARME'03}, L'Aquila, Italy, 2003, pp.247--262.
    [6]
    McMillan K. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In -\it CHARME'01}, Livingston, Scotland, LNCS 2144, Springer-Verlag, 2001, pp.179--195.
    [7]
    McMillan K. Verification of infinite state systems by compositional model checking. In -\it CHARME'99}, Bad Herrenalb, Germany, LNCS 1703, Springer-Verlag, 1999, pp.219--233.
    [8]
    McMillan K, Qadeer S, Saxe J B. Induction in compositional model checking. In -\it CAV'00}, Chicago, IL, USA, LNCS 1855, 2000, pp.312--327.
    [9]
    Emerson E A, Lahon V. Reducing model checking for the many to the few. In -\it CADE'00}, Pittsburgh, PA, USA, LNCS 1831, 2000, pp.236--254.
    [10]
    Das S, Dill D, Park S. Experience with predicate abstraction. In -\it CAV'99}, Trento, Italy, LNCS 1633, Springer-Verlag, 1999, pp.160--171.
    [11]
    Graf S, Saidi H. Construction of abstract state graphs with PVS. In -\it CAV'97}, Haifa, Israel, LNCS 1254, Springer-Verlag, 1997, pp.72--83.
    [12]
    Bryant R E, Lahiri S K, Seshia S A. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In -\it CAV'02}, Copenhagen, Denmark, LNCS 2404, Springer-Verlag, 2002, pp.78--92.
    [13]
    Lahiri S K, Bryant R. Constructing quantified invariants via predicate abstraction. In -\it VMCAI'04}, Venice, Italy, LNCS 2937, Springer-Verlag, 2004, pp.267--281.
    [14]
    Lin H. Model checking value-passing processes. In -\it APSEC'2001}, Macau, December 4--7, IEEE Computer Society, 2001 pp.3--10.
    [15]
    Lin H. ``On-the-fly" instantiation of value-passing processes. In -\it FORTE/PSTV'98}, Paris, France, Kluwer Academic Publishers, 1998, pp.215--230.
    [16]
    Milner R. Communication and Concurrency. Prentice-Hall, 1989.
    [17]
    German S, Janssen G. Tutorial on verification of distributed cache memory protocols. In -\it FMCAD'04}, Austin, Texas, USA, 2004.
    • Relative Articles
  • Supplements (0)

Catalog

    Get Citation
    XML
    Article views (23) PDF downloads (1630) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return