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能够可行地验证具有高速缓存层次结构的现代无序处理器的一致性行为。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.