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 sharedmemory 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 "presilicon
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, manycore systems such that the protocols are verifiable using existing, automated, easytouse 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 Nnode 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 selfsimilarity 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 sharedmemory 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 directorybased 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 selfsimilarity
of fractals to enable the verification of any arbitrary Nnode 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: 
[ZhangLebeckSorin10]
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 471482, 2010.
Available online at: http://people.ee.duke.edu/~sorin/papers/micro10_fractal.pdf or from our FTP site in PDF or PostScript [Zhang13] Meng Zhang. "Scalably Verifiable Cache Coherence". PhD thesis, Duke University, 2013. Available online at: http://dukespace.lib.duke.edu/dspace/handle/10161/8203 or from our FTP site in PDF or PostScript [VoskuilenVijaykumar14a] Gwendolyn Voskuilen and T. N. Vijaykumar. "HighPerformance 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. 701714, ACM, March 2014. Available online at: http://dl.acm.org/citation.cfm?id=2541982 [VoskuilenVijaykumar14b] 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. 409420, IEEE., June 2014. Available online 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 277080291 USA Tel: 9196605439 Fax: 9196605293 Email: sorin@ee.duke.edu 
Further remarks:  This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/casestudies 