Duke University (Durham, NC, USA)
CADP (Construction and Analysis of Distributed Processes)
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.
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
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 the CADP Web 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 the CADP Web 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
Daniel J. Sorin
Electrical and Computer Engineering and Computer Science
Office: 209C Hudson Hall
Durham, NC 27708-0291
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|