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

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

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.