Skip to main content

PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications

Author(s): Manerkar, Yatin A; Lustig, Daniel; Martonosi, Margaret; Gupta, Aarti

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1vv69
Full metadata record
DC FieldValueLanguage
dc.contributor.authorManerkar, Yatin A-
dc.contributor.authorLustig, Daniel-
dc.contributor.authorMartonosi, Margaret-
dc.contributor.authorGupta, Aarti-
dc.date.accessioned2021-10-08T19:45:27Z-
dc.date.available2021-10-08T19:45:27Z-
dc.date.issued2018en_US
dc.identifier.citationManerkar, Yatin A., Daniel Lustig, Margaret Martonosi, and Aarti Gupta. "PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications." 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO) (2018): pp. 788-801. doi:10.1109/MICRO.2018.00069en_US
dc.identifier.urihttps://www.cs.princeton.edu/~aartig/papers/micro18-pipeproof.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1vv69-
dc.description.abstractMemory 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.en_US
dc.format.extent788 - 801en_US
dc.language.isoen_USen_US
dc.relation.ispartof51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO)en_US
dc.rightsAuthor's manuscripten_US
dc.titlePipeProof: Automated Memory Consistency Proofs for Microarchitectural Specificationsen_US
dc.typeConference Articleen_US
dc.identifier.doi10.1109/MICRO.2018.00069-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
PipeproofConsistencyProofsMicroarchitecturalSpecs.pdf752.52 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.