PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications

摘要

Memory consistency models (MCMs) specify rules which constrain the values that can be returned by load instructions in parallel programs. To ensure that parallel programs run correctly, verification of hardware MCM implementations would ideally be complete; i.e. verified as being correct across all possible executions of all possible programs. However, no existing automated approach is capable of such complete verification. To help fill this verification gap, we present PipeProof, a methodology and tool for complete MCM verification of an axiomatic microarchitectural (hardware-level) ordering specification against an axiomatic ISA-level MCM specification. PipeProof can automatically prove a microarchitecture correct in all cases, or return an indication (often a counterexample) that the microarchitecture could not be verified. To accomplish unbounded verification, PipeProof introduces the novel Transitive Chain Abstraction to represent microarchitectural executions of an arbitrary number of instructions using only a small, finite number of instructions. With the help of this abstraction, PipeProof proves microarchitectural correctness using an automatic abstraction refinement approach. PipeProof's implementation also includes algorithmic optimizations which improve runtime by greatly reducing the number of cases considered. As a proof-of-concept study, we present results for modelling and proving correct simple microarchitectures implementing the SC and TSO MCMs. PipeProof verifies both case studies in under an hour, showing that it is indeed possible to automate microarchitectural MCM correctness proofs.