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）可能会重新启动（4），并且（4检查有关RTL实现的特定狭窄谓词（二进制问题）。该项目的影响是（1）解决QED的大挑战MCM验证问题，从必须考虑任意说明序列排序（这是很大的）到只需要考虑仅考虑成对的指令排序（数千个范围）到获得相同的排序保证的，就必须考虑任意说明序列排序（这是很大的）。 QED能够通过利用“不可观察”重新排序的通知来进一步减少要考虑的指令重新排序的数量 - 在验证工作中可以安全地忽略的指令重新排序，从而产生与原始顺序相同的值。调查人员团队将制定正式的未订购规则，以自动验证任意实施。结合上述创新，可以考虑所有可能的内存访问（和任意外部事件）的所有可能交织，并开发基于决策的验证验证框架，该框架可扩展到任何数量的内核和任何数量的指令。有效地预测了有关实现的决策树节点，也可以自动检查QED的自动RTL谓词检查器。结合起来，这些技术使QED可以可行地验证现代，阶外处理器与缓存层次结构的一致性行为。该奖项反映了NSF的法定任务，并被认为是通过基金会的智力优点和更广泛的影响来通过评估来获得的支持。