CCICheck: Using νhb graphs to verify the coherence-consistency interface

Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Rose Martonosi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

30 Scopus citations

Abstract

In parallel systems, memory consistency models and cache coherence protocols establish the rules specifying which values will be visible to each instruction of parallel programs. Despite their central importance, verifying their correctness has remained a major challenge, due both to informal or incomplete specifications and to difficulties in scaling verification to cover their operations comprehensively. While coherence and consistency are often specified and verified independently at an architectural level, many systems implement performance enhancements that tightly interweave coherence and consistency at a microarchitectural level in ways that make verification of consistency difficult. This paper introduces CCICheck, a tool and technique supporting static verification of the coherence-consistency interface (CCI). CCICheck enumerates and checks families of microarchitectural happens-before (νhb) graphs that describe how a particular coherence protocol combines with a particular processor's pipelines and memory hierarchy to enforce the requirements of a given consistency model. To support tractable CCI verification, CCICheck introduces the ViCL (Value in Cache Lifetime), an abstraction which allows the νhb graphs to cleanly represent CCI events relevant to consistency verification, including demand fetching, cache line invalidation, coherence protocol windows of vulnerability, and partially incoherent cache hierarchies. We implement CCICheck as an automated tool and demonstrate its use on a number of case studies. We also show its tractability across a wide range of litmus tests.

Original languageEnglish (US)
Title of host publicationProceedings - 48th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2015
PublisherIEEE Computer Society
Pages26-37
Number of pages12
ISBN (Electronic)9781450340342
DOIs
StatePublished - Dec 5 2015
Event48th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2015 - Waikiki, United States
Duration: Dec 5 2015Dec 9 2015

Publication series

NameProceedings of the Annual International Symposium on Microarchitecture, MICRO
Volume05-09-December-2015
ISSN (Print)1072-4451

Other

Other48th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2015
Country/TerritoryUnited States
CityWaikiki
Period12/5/1512/9/15

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Fingerprint

Dive into the research topics of 'CCICheck: Using νhb graphs to verify the coherence-consistency interface'. Together they form a unique fingerprint.

Cite this