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

点击翻译按钮获取中文摘要

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.