TY - GEN
T1 - CCICheck
T2 - 48th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2015
AU - Manerkar, Yatin A.
AU - Lustig, Daniel
AU - Pellauer, Michael
AU - Martonosi, Margaret Rose
N1 - Publisher Copyright:
© 2015 ACM.
PY - 2015/12/5
Y1 - 2015/12/5
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84959860022&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84959860022&partnerID=8YFLogxK
U2 - 10.1145/2830772.2830782
DO - 10.1145/2830772.2830782
M3 - Conference contribution
AN - SCOPUS:84959860022
T3 - Proceedings of the Annual International Symposium on Microarchitecture, MICRO
SP - 26
EP - 37
BT - Proceedings - 48th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2015
PB - IEEE Computer Society
Y2 - 5 December 2015 through 9 December 2015
ER -