Skip to main content
SpringerLink
Log in

Model Checking Data Consistency for Cache Coherence Protocols

  • Theory
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order μ-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Baukus K, Lakhnech Y, Stahl K. Parameterized verification of a cache coherence protocol: Safety and liveness. In 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 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 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 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 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 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 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 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 CADE’00, Pittsburgh, PA, USA, LNCS 1831, 2000, pp. 236–254.

  10. Das S, Dill D, Park S. Experience with predicate abstraction. In 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 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 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 VMCAI’04, Venice, Italy, LNCS 2937, Springer-Verlag, 2004, pp. 267–281.

  14. Lin H. Model checking value-passing processes. In 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 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 FMCAD’04, Austin, Texas, USA, 2004.

Download references

Author information

Authors and Affiliations

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

    Hong Pan, Hui-Min Lin & Yi Lv

Authors
  1. Hong Pan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hui-Min Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yi Lv
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hong Pan.

Additional information

Regular Paper: Supported by the Intel Strategic CAD Labs, the National Natural Science Foundation of China (Grant No. 60421001), and the Chinese Academy of Sciences.

Hong Pan received her B.E. degree in computer science from the University of Science and Technology of China in 2002. She is now a Ph.D. candidate in the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (CAS). Her research interests include model checking, protocol verification, and concurrent systems.

Hui-Min Lin received his Ph.D. degree in computer science from the Institute of Software, CAS in 1986. He is now a research professor in the State Key Laboratory of Computer Science, Institute of Software, CAS. His research interests include concurrency theory, value-passing process algebras, mobile computing, model checking and modal logics, and formal methods.

Yi Lv received his Ph.D. degree in computer architecture from the Institute of Computing Technology, CAS, in 2004. He is now a post-doctor in the State Key Laboratory of Computer Science, Institute of Software, CAS. His current research interests include model checking and formal verification.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Pan, H., Lin, HM. & Lv, Y. Model Checking Data Consistency for Cache Coherence Protocols. J Comput Sci Technol 21, 765–775 (2006). https://doi.org/10.1007/s11390-006-0765-6

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-006-0765-6

Keywords

Search

Navigation