Pipe Check: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models

摘要

We present Pipe Check, a methodology and automated tool for verifying that a particular micro architecture correctly implements the consistency model required by its architectural specification. Pipe Check adapts the notion of a "happens before" graph from architecture-level analysis techniques to the micro architecture space. Each node in the "micro architecturally happens before" (μhb) graph represents not only a memory instruction, but also a particular location (e.g., Pipeline stage) within the micro architecture. Architectural specifications such as "preserved program order" are then treated as propositions to be verified, rather than simply as assumptions. Pipe Check allows an architect to easily and rigorously test whether a micro architecture is stronger than, equal in strength to, or weaker than its architecturally-specified consistency model. We also specify and analyze the behavior of common micro architectural optimizations such as speculative load reordering which technically violate formal architecture-level definitions. We evaluate Pipe Check using a library of established litmus tests on a set of open-source pipelines. Using Pipe Check, we were able to validate the largest pipeline, the Open SPARC T2, in just minutes. We also identified a bug in the O3 pipeline of the gem5 simulator.