Advertisement

Formal Methods in System Design

, Volume 36, Issue 1, pp 37–64 | Cite as

Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols

  • Xiaofang Chen
  • Yu Yang
  • Ganesh Gopalakrishnan
  • Ching-Tsun Chou
Article

Abstract

Multicore architectures are considered inevitable, given that sequential processing hardware has hit various limits. Unfortunately, the memory system of multicore processors is a huge bottleneck. To combat this problem, one needs to design aggressively optimized cache coherence protocols. This introduces the design correctness problem for advanced cache coherence protocols which will be hierarchically organized for scalable designs. Experiences show that monolithic formal verification will not scale to hierarchical designs. Hence, one needs to handle the complexity of several coherence protocols running concurrently, i.e. hierarchical protocols, using compositional techniques.

To solve the problem, we develop a family of compositional approaches all based on assume-guarantee reasoning to reducing the verification complexity. We show that for the three hierarchical protocols with certain realistic features that we developed for multiple chip-multiprocessors, more than a 20-fold improvement in terms of the number of states visited can be achieved. Also, to avoid false alarms wasting designer time, we have developed an error trace justification method to eliminate false alarms using heuristics that also capitalize on our assume-guarantee approaches. Our techniques need no special tool support. They can be carried out using the widely used Murphi model checker along with support tools for abstraction and error trace justification that we have built.

Keywords

Explicit state model checking Hierarchical cache coherence protocols Abstraction/refinement Assume-guarantee reasoning 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
  2. 2.
  3. 3.
    Abts D, Lilja D, Scott S (2000) Toward complexity-effective verification: a case study of the cray SV2 cache coherence protocol. In: Int’l symp computer architecture workshop complexity-effective design (2000) Google Scholar
  4. 4.
    Barroso LA, Gharachorloo K, McNamara R, Nowatzyk A, Qadeer S, Sano B, Smith S, Stets R, Verghese B (2000) Piranha: a scalable architecture based on single-chip multiprocessing. In: Int’l symposium on computer architecture Google Scholar
  5. 5.
    Baskett F, Jermoluk TA, Solomon D (1988) The 4d-mp graphics superworkstation: computing + graphics = 40 mips + 40 mflops and 100,000 lighted polygons per second. In: Digest of papers, thirty-third IEEE computer society int’l conference, pp 468–471 Google Scholar
  6. 6.
    Batson B, Lamport L (2002) High-level specifications: lessons from industry. In: Formal methods for components and objects Google Scholar
  7. 7.
    Bingham J (2008) Automatic non-interference lemmas for parameterized model checking. In: Formal methods in computer aided design Google Scholar
  8. 8.
    Chandy KM, Misra J (1988) Parallel program design: a doundation. Addison-Wesley, Reading Google Scholar
  9. 9.
    Chen X, Yang Y, Delisi M, Gopalakrishnan G, Chou C-T (2007) Hierarchical cache coherence protocol verification one level at a time through assume guarantee. In: IEEE intl high level design validation and test workshop Google Scholar
  10. 10.
    Cheng L, Muralimanohar N, Ramani K, Balasubramonian R, Carter JB (2006) Interconnect-aware coherence protocols for chip multiprocessors. In: Int’l symp on computer architecture Google Scholar
  11. 11.
    Chou CT, German SM, Gopalakrishnan G (2004) Tutorial on specification and verification of shared memory protocols and consistency models. In: Formal methods in computer-aided design Google Scholar
  12. 12.
    Chou C-T, Mannava PK, Park S (2004) A simple method for parameterized verification of cache coherence protocols. In: Formal methods in computer aided design Google Scholar
  13. 13.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, New York Google Scholar
  14. 14.
    Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Computer aided verification Google Scholar
  15. 15.
    Clint M (1973) Program proving: coroutines. In: Acta informatica, pp 50–63 Google Scholar
  16. 16.
    Dill DL, Drexler AJ, Hu AJ, Yang CH (1992) Protocol verification as a hardware design aid. In: IEEE intl conference on computer design: VLSI in computers and processors Google Scholar
  17. 17.
    Edelkamp S, Lluch-Lafuente A, Leue S (2001) Directed explicit-state model checking with HSF-SPIN. In: SPIN workshop, pp 57–79 Google Scholar
  18. 18.
    Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: Intl confererence on automated deduction, pp 236–254 Google Scholar
  19. 19.
    German S (2004) Tutorial on verification of distributed cache memory protocols. In: Formal methods in computer aided design Google Scholar
  20. 20.
    German SM (2003) Formal design of cache memory protocols in IBM. In: Formal methods in system design Google Scholar
  21. 21.
    Gharachorloo K, Sharma M, Steely S, Doren SV (2000) Architecture and design of AlphaServer GS320. In: Architecture support for programming languages and operating systems Google Scholar
  22. 22.
    Gopalakrishnan G, Hunt W (2003) Formal methods in industrial practice: a sampling. In: Formal methods in system design Google Scholar
  23. 23.
    Ip CN, Dill DL (1996) Verifying systems with replicated components in Murphi. In: Computer aided verification, pp 147–158 Google Scholar
  24. 24.
    Krstić S (2005) Parameterized system verification with guard strengthening and parameter abstraction. In: Automated verification of infinite-state systems Google Scholar
  25. 25.
    Kuskin J, Ofelt D, Heinrich M, Heinlein J, Simoni R, Gharachorloo K, Chapin J, Nakahira D, Baxter J, Horowitz M, Gupta A, Rosenblum M, Hennessy J (1994) The Stanford FLASH multiprocessor. In: Proceedings of the 21st intl symposium on computer architecture, pp 302–313 Google Scholar
  26. 26.
    Lahiri SK, Bryant RE (2004) Constructing quantified invariants via predicate abstraction. In: Verification, model checking, and abstract interpretation (VMCAI) Google Scholar
  27. 27.
    Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Reading Google Scholar
  28. 28.
    Lenoski D, Laudon J, Gharachorloo K, Gupta A, Hennessy J (1990) The directory-based cache coherence protocol for the DASH multiprocessor. In: Int’l symposium on computer architecture (ISCA), pp 148–159 Google Scholar
  29. 29.
    Li Y (2007) Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols. In: ACM symposium on applied computing, pp 1534–1535 Google Scholar
  30. 30.
    Marty MR (2008) Cache coherence techniques for multicore processors. PhD thesis, University of Wisconsin-Madison Google Scholar
  31. 31.
    Marty MR, Bingham JD, Hill MD, Hu AJ, Martin MMK, Wood DA (2005) Improving multiple-CMP systems using token coherence. In: Intl symposium on high performance computer architecture Google Scholar
  32. 32.
    McMillan KL (1999) Circular compositional reasoning about liveness. In: International conference on correct hardware design and verification methods Google Scholar
  33. 33.
    McMillan KL (2001) Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Correct hardware design and verification methods, pp 179–195 Google Scholar
  34. 34.
    McMillan KL, Schwalbe J (1991) Formal verification of the gigamax cache-consistency protocol. In: Int’l symposium on shared memory multiprocessing Google Scholar
  35. 35.
    McMillan KL (1992) Symbolic model checking. PhD thesis, Carnegie Mellon University Google Scholar
  36. 36.
    Moore KE, Bobba J, Moravan MJ, Hill MD, Wood DA (2006) Logtm: log-based transactional memory. In: High-performance computer architecture Google Scholar
  37. 37.
    Owicki S (1976) A consistent and complete deductive system for the verification of parallel programs. In: Symposium on theory of computing Google Scholar
  38. 38.
    Papamarcos M, Patel J (1984) A low overhead coherence solution for multiprocessors with private cache memories. In: Int’l symposium on computer architecture Google Scholar
  39. 39.
    Shen X, Arvind, Rudolph L (1999) CACHET: an adaptive cache coherence protocol for distributed shared-memory systems. In: Int’l conference on supercomputing Google Scholar
  40. 40.
    Talupur M, Tuttle M (2008) Going with the flow: parameterized verification using message flows. In: Formal methods in computer aided design Google Scholar
  41. 41.
    Yang L, Gao D, Mostoufi J, Joshi R, Loewenstein P (1995) System design methodology of UltraSPARC-I. In: Design automation conference Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  • Xiaofang Chen
    • 1
  • Yu Yang
    • 1
  • Ganesh Gopalakrishnan
    • 1
  • Ching-Tsun Chou
    • 2
  1. 1.School of ComputingUniversity of UtahSalt Lake CityUSA
  2. 2.Intel CorporationSanta ClaraUSA

Personalised recommendations