NDLI: Revisiting the Complexity of Hardware Cache Coherence and Some Implications

Content Provider	ACM Digital Library
Author	Adve, Sarita V. Chou, Ching-Tsun Komuravelli, Rakesh
Copyright Year	2014
Abstract	Cache coherence is an integral part of shared-memory systems but is also widely considered to be one of the most complex parts of such systems. Much prior work has addressed this complexity and the verification techniques to prove the correctness of hardware coherence. Given the new multicore era with increasing number of cores, there is a renewed debate about whether the complexity of hardware coherence has been tamed or whether it should be abandoned in favor of software coherence. This article revisits the complexity of hardware cache coherence by verifying a publicly available, state-of-the-art implementation of the widely used MESI protocol, using the Murϕ model checking tool. To our surprise, we found six bugs in this protocol, most of which were hard to analyze and took several days to fix. To compare the complexity, we also verified the recently proposed DeNovo protocol, which exploits disciplined software programming models. We found three relatively easy to fix bugs in this less mature protocol. After fixing these bugs, our verification experiments showed that, compared to DeNovo, MESI had 15X more reachable states leading to a 20X increase in verification (model checking) time. Although we were eventually successful in verifying the protocols, the tool required making several simplifying assumptions (e.g., two cores, one address). Our results have several implications: (1) they indicate that hardware coherence protocols remain complex; (2) they reinforce the need for protocol designers to embrace formal verification tools to demonstrate correctness of new protocols and extensions; (3) they reinforce the need for formal verification tools that are both scalable and usable by non-expert; and (4) they show that a system based on hardware-software co-design can offer a simpler approach for cache coherence, thus reducing the overall verification effort and allowing verification of more detailed models and protocol extensions that are otherwise limited by computing resources.
Starting Page	1
Ending Page	22
Page Count	22
File Format	PDF
ISSN	15443566
e-ISSN	15443973
DOI	10.1145/2663345
Volume Number	11
Issue Number	4
Journal	ACM Transactions on Architecture and Code Optimization (TACO)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-12-08
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Cache coherence Model checking Multicore Protocol verification Shared memory Software-hardware co-design
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

The Effects of Granularity and Adaptivity on Private/Shared Classification for Coherence

Model checking parameterized asynchronous shared-memory systems

Design and formal verification of a hierarchical cache coherence protocol for NoC based multiprocessors

Parallel Stimulus Generation Based on Model Checking for Coherence Protocol Verification

Maintaining I/O Data Coherence in Embedded Multicore Systems

Scalable shared memory LTL model checking

Symmetry-Agnostic Coordinated Management of the Memory Hierarchy in Multicore Systems

A Hardware Memory Race Recorder for Deterministic Replay

Cache coherence tradeoffs in shared-memory MPSoCs

Revisiting the Complexity of Hardware Cache Coherence and Some Implications

Similar Documents

The Effects of Granularity and Adaptivity on Private/Shared Classification for Coherence

Model checking parameterized asynchronous shared-memory systems

Design and formal verification of a hierarchical cache coherence protocol for NoC based multiprocessors

Parallel Stimulus Generation Based on Model Checking for Coherence Protocol Verification

Maintaining I/O Data Coherence in Embedded Multicore Systems

Scalable shared memory LTL model checking

Symmetry-Agnostic Coordinated Management of the Memory Hierarchy in Multicore Systems

A Hardware Memory Race Recorder for Deterministic Replay

Cache coherence tradeoffs in shared-memory MPSoCs

Revisiting the Complexity of Hardware Cache Coherence and Some Implications