PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications
PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications
复制标题
PipeProof：微架构规范的自动内存一致性证明
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Aarti Gupta
中科院分区：
文献类型：
--
作者：
Yatin A. Manerkar;Daniel Lustig;M. Martonosi;Aarti Gupta
内存一致性模型（MCMS）指定规则，该规则限制了并行程序中的加载指令可以返回的值。为了确保并行程序正确运行，理想情况下，硬件MCM实现的验证将完成；即，在所有可能的程序的所有可能执行中，都被验证为正确的。但是，没有现有的自动化方法能够进行这种完整的验证。为了帮助填补此验证空白，我们提供了PipeProof，这是一种用于完整MCM验证的方法和工具，可针对公理ISA级MCM规范进行公理微构造（硬件级）订购规范。在所有情况下，PipeProof都可以自动证明是正确的，或者返回指示（通常是反例）无法验证微体系结构。为了完成无限的验证，PipeProof引入了新型的及时链抽象，以表示仅使用少量有限的指令数量的任意指令的微体系执行。在这种抽象的帮助下，PipeProof使用自动抽象的细化方法证明了微体系式的正确性。 PipeProof的实现还包括算法优化，可通过大大减少所考虑的案例数来改善运行时。作为概念验证的研究，我们提出了实施SC和TSO MCM的正确模拟和证明正确的简单微体系结构的结果。 PipeProove在一个小时内验证了这两个案例研究，表明确实可以自动化微体系模式MCM正确性。
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.
DOI：
10.1145/3009837.3009838
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Wickerson J
通讯作者：
Wickerson J