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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
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)
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
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
Batson B, Lamport L (2002) High-level specifications: lessons from industry. In: Formal methods for components and objects
Bingham J (2008) Automatic non-interference lemmas for parameterized model checking. In: Formal methods in computer aided design
Chandy KM, Misra J (1988) Parallel program design: a doundation. Addison-Wesley, Reading
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
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
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
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
Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, New York
Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Computer aided verification
Clint M (1973) Program proving: coroutines. In: Acta informatica, pp 50–63
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
Edelkamp S, Lluch-Lafuente A, Leue S (2001) Directed explicit-state model checking with HSF-SPIN. In: SPIN workshop, pp 57–79
Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: Intl confererence on automated deduction, pp 236–254
German S (2004) Tutorial on verification of distributed cache memory protocols. In: Formal methods in computer aided design
German SM (2003) Formal design of cache memory protocols in IBM. In: Formal methods in system design
Gharachorloo K, Sharma M, Steely S, Doren SV (2000) Architecture and design of AlphaServer GS320. In: Architecture support for programming languages and operating systems
Gopalakrishnan G, Hunt W (2003) Formal methods in industrial practice: a sampling. In: Formal methods in system design
Ip CN, Dill DL (1996) Verifying systems with replicated components in Murphi. In: Computer aided verification, pp 147–158
Krstić S (2005) Parameterized system verification with guard strengthening and parameter abstraction. In: Automated verification of infinite-state systems
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
Lahiri SK, Bryant RE (2004) Constructing quantified invariants via predicate abstraction. In: Verification, model checking, and abstract interpretation (VMCAI)
Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Reading
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
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
Marty MR (2008) Cache coherence techniques for multicore processors. PhD thesis, University of Wisconsin-Madison
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
McMillan KL (1999) Circular compositional reasoning about liveness. In: International conference on correct hardware design and verification methods
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
McMillan KL, Schwalbe J (1991) Formal verification of the gigamax cache-consistency protocol. In: Int’l symposium on shared memory multiprocessing
McMillan KL (1992) Symbolic model checking. PhD thesis, Carnegie Mellon University
Moore KE, Bobba J, Moravan MJ, Hill MD, Wood DA (2006) Logtm: log-based transactional memory. In: High-performance computer architecture
Owicki S (1976) A consistent and complete deductive system for the verification of parallel programs. In: Symposium on theory of computing
Papamarcos M, Patel J (1984) A low overhead coherence solution for multiprocessors with private cache memories. In: Int’l symposium on computer architecture
Shen X, Arvind, Rudolph L (1999) CACHET: an adaptive cache coherence protocol for distributed shared-memory systems. In: Int’l conference on supercomputing
Talupur M, Tuttle M (2008) Going with the flow: parameterized verification using message flows. In: Formal methods in computer aided design
Yang L, Gao D, Mostoufi J, Joshi R, Loewenstein P (1995) System design methodology of UltraSPARC-I. In: Design automation conference
Author information
Authors and Affiliations
Corresponding author
Additional information
This work is supported in part by SRC TJ 1318.001, 1847.00, and NSF CCF-0811429.
Rights and permissions
About this article
Cite this article
Chen, X., Yang, Y., Gopalakrishnan, G. et al. Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. Form Methods Syst Des 36, 37–64 (2010). https://doi.org/10.1007/s10703-010-0092-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-010-0092-y