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 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
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

Back to the CADP case studies page