SHF: Small: QED - A New Approach to Scalable Verification of Hardware Memory Consistency

SHF：小型：QED - 硬件内存一致性可扩展验证的新方法

• 批准号: 2332891
• 负责人: T Vijaykumar
• 金额: $ 59.34万
• 依托单位: Purdue University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-03-01 至 2027-02-28
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2332891&HistoricalAwards=false
• 关键词: SHF; Small; QED; New; Approach

A key correctness requirement of modern, general-purpose, high-performance, shared-memory multiprocessor systems is that they must comply with the rules of memory consistency that control the perceived order of memory operations. However, implementing memory consistency correctly is notoriously non-intuitive and complex. Memory consistency is a significant source of hardware design bugs. As such, the ability to formally verify the correctness of implementations before manufacture and distribution is desirable. Unfortunately, comprehensive verification to rule out these subtle bugs is difficult. Consequently, real-world products often exhibit buggy behavior in the field. In spite of its importance, the intractability of formal verification at meaningful scales has thus far resulted in either (1) less-than-complete approaches based on collections of tests, which are by no means comprehensive, or (2) comprehensive verification of simple cores that are not representative of modern out-of-order processors. To address this problem, this project develops a formal verification framework -- QED -- to verify that an RTL (register-transfer-level) implementation of a modern, out-of-order processor with a cache hierarchy is compliant with a given memory consistency model (MCM). The project’s novelties are (1) a divide-and-conquer approach to isolate and focus on memory consistency violations separately from other verification tasks (such as pipeline verification) that are well-studied, (2) novel ways to provably reduce the number of instructions to be considered, (3) an automatic way to scalably consider all possible reorderings by ignoring reorderings that are provably unobservable, and (4) reducing the RTL verification burden to that of checking specific, narrow predicates (binary questions) on the RTL implementation. The project’s impacts are (1) tackling the grand-challenge MCM verification problem that is of high importance to the computer hardware industry, and (2) training graduate researchers in the field of MCM verification.The key insights and observations behind the project’s innovations are as follows. QED reduces the memory ordering problem from having to consider arbitrary instruction sequence ordering (which is intractably large) to having to consider only pairwise instruction ordering (which is in the hundreds-thousands range) to achieve the same ordering guarantees. QED is able to further reduce the number of instruction reorderings to consider by leveraging the notion of ‘unobservable’ reorderings -- instruction reorderings that produce the same values as the original order, which can thus be ignored safely in the verification effort. The team of investigators will develop formal un-reordering rules that will enable automatic verification of arbitrary implementations. Combining the above innovations, it is possible to consider all possible interleavings of pairs of memory accesses (and arbitrary external events) and develop a decision-tree-based verification framework that is scalable to any number of cores and any number of instructions. The nodes of the decision tree are effectively predicates about the implementation, which can also be automatically checked by QED's proposed automatic RTL predicate checkers. In combination, the techniques enable QED to feasibly verify the consistency behavior of modern, out-of-order processors with cache hierarchies.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

现代、通用、高性能、共享内存多处理器系统的一个关键正确性要求是它们必须遵守控制内存操作感知顺序的内存一致性规则。然而，众所周知，正确实现内存一致性是不可行的。内存一致性是设计错误的一个重要来源，因此，在制造和分发之前能够正式验证实现的正确性是很困难的。 -世界各地的产品经常展出尽管该领域的错误行为很重要，但迄今为止，在有意义的规模上进行形式验证的棘手性导致了（1）基于测试集合的不完整方法，这些方法绝不是全面的，或者（ 2）对不代表现代乱序处理器的简单内核进行全面验证为了解决这个问题，该项目开发了一个正式的验证框架——QED——来验证RTL（寄存器传输级）实现。一个现代的、具有缓存层次结构的乱序处理器符合给定的内存一致性模型 (MCM) 该项目的新颖之处在于 (1) 采用分而治之的方法，将内存一致性违规与其他验证任务分开并重点关注（ （2）可证明减少要考虑的指令数量的新颖方法，（3）一种通过忽略可证明的重新排序来可扩展地考虑所有可能的重新排序的自动方法(4) 将 RTL 验证负担减少到检查 RTL 实施的具体、狭窄谓词（二元问题）。该项目的影响是 (1) 解决了对 MCM 非常重要的重大挑战 MCM 验证问题。计算机硬件行业，减少和（2）培训 MCM 验证领域的研究生研究人员。该项目创新背后的关键见解和观察如下：QED 必须考虑任意指令序列排序（其中。难以处理的大）到只需考虑成对指令排序（在数十万范围内）即可实现相同的排序保证 QED 能够通过利用“不可观察”的概念进一步减少要考虑的指令重新排序的数量。重新排序——产生与原始顺序相同的值的指令重新排序，因此在验证工作中可以安全地忽略这些值，研究人员团队将开发正式的取消重新排序规则，以实现任意的自动验证。结合上述创新，可以考虑内存访问对（以及任意外部事件）的所有可能交错，并开发可扩展到任意数量的内核和任意数量的指令的基于决策树的验证框架。决策树的节点是关于实现的有效谓词，也可以由 QED 的自动提出的 RTL 谓词检查器自动检查。结合起来，这些技术使 QED 能够切实验证现代的一致性行为。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。