Database of Case Studies Achieved Using CADP

Scalably Verifiable Cache Coherence

Organisation: Duke University (Durham, NC, USA)

Method: n/a

Tools used: CADP (Construction and Analysis of Distributed Processes)
MurPhi

Domain: Hardware Design.

Period: 2010

Size: n/a

Description: A buggy cache coherence protocol might lead to a catastrophic failure of the shared-memory system that employs this protocol. To achieve high performance, current cache coherence protocols allow multiple outstanding requests and concurrent operations. This concurrency implies numerous transient states and nondeterministic behaviour due to race conditions. To ensure the reliability of the protocol, design verification (also known as "design validation" or "pre-silicon validation") must be done as part of implementing cache coherence protocols for real systems.

This work proposes, from the perspective of architects, a new methodology for designing cache coherence protocols, called Fractal Coherence. The objective is to design cache coherence protocols for large, many-core systems such that the protocols are verifiable using existing, automated, easy-to-use formal tools. The smallest complete system, called the minimum system, is small enough to be easily verified coherent using existing formal verification tools without incurring the state explosion problem. Larger systems can be verified fractal in behaviour by showing that any scale of the system behaves exactly the same w.r.t. coherence. The whole system can then be proved coherent using induction, and thus the verification of a Fractal Coherence protocol can be scaled to any arbitrary N-node system. To make the induction proof work, two verification steps are needed. First, the minimum system must be verified cache coherent (using model checking), and secondly, the whole system must be verified fractal in behaviour (using equivalence checking), such that self-similarity can be leveraged to arbitrary levels.

The Fractal Coherence methodology is illustrated by the design of a concrete example of a cache coherence protocol, called TreeFractal. The primary difference between TreeFractal and traditional protocols is that TreeFractal introduces an interface component to maintain the fractal behaviour at each scale. TreeFractal connects the interfaces, the cores, the caches and the memories to construct a shared-memory system. The cache coherence of the minimum system for TreeFractal (which contains two tag processes and three controller processes) was verified using MurPhi, and the fractal behaviour was verified using the BISIMULATOR equivalence checker of CADP. The TreeFractal protocol was also compared, by means of extensive simulation, with classical snooping and directory-based cache coherency protocols, and shown to exhibit comparable performance.

Conclusions: The Fractal Coherence methodology puts forward a class of scalably verifiable coherence protocols, which leverages the self-similarity of fractals to enable the verification of any arbitrary N-node system. The verification of Fractal Coherence protocols is simplified to two straightforward, automated steps and does not incur the state explosion problem. This methodology encourages hardware architects to consider verification effort as a design constraint and incorporate it in early design stages.

Publications: [Zhang-Lebeck-Sorin-10] Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. "Fractal Coherence: Scalably Verifiable Cache Coherence". Proceedings of the 43th Annual IEEE/ACM International Symposium on Microarchitecture MICRO'10, IEEE Computer Society, pages 471-482, 2010.
Available on-line at: http://people.ee.duke.edu/~sorin/papers/micro10_fractal.pdf
or from our FTP site in PDF or PostScript

[Zhang-13] Meng Zhang. "Scalably Verifiable Cache Coherence". PhD thesis, Duke University, 2013.
Available on-line at: http://dukespace.lib.duke.edu/dspace/handle/10161/8203
or from our FTP site in PDF or PostScript

[Voskuilen-Vijaykumar-14-a] Gwendolyn Voskuilen and T. N. Vijaykumar. "High-Performance Fractal Coherence". Proceedings of the 19th International Conference on Architectural Support for Programming Languages and Operating Systems ASPLOS'14 (Salt Lake City, Utah, USA), pp. 701-714, ACM, March 2014.
Available on-line at: http://dl.acm.org/citation.cfm?id=2541982

[Voskuilen-Vijaykumar-14-b] Gwendolyn Voskuilen and T. N. Vijaykumar. "Fractal++: Closing the Performance Gap between Fractal and Conventional Coherence". Proceedings of the 41st ACM/IEEE International Symposium on Computer Architecture ISCA'2014 (Minneapolis, Minnesota, USA), pp. 409-420, IEEE., June 2014.
Available on-line at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6853211

Contact:
Daniel J. Sorin
Electrical and Computer Engineering and Computer Science
Duke University
Office: 209C Hudson Hall
Box 90291
Durham, NC 27708-0291
USA
Tel: 919-660-5439
Fax: 919-660-5293
Email: sorin@ee.duke.edu



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page