Automated Full-Stack Memory Model Verification with the Check suite

Add to your list(s) Download to your calendar using vCal

• Yatin Manerkar, Princeton University
• Thursday 19 July 2018, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

Memory models constrain the values that can be read by loads in shared-memory parallel systems. They are defined for high-level languages (like C11 and Java) and instruction set architectures (ISAs) like x86-TSO, ARM , RISC-V, and Power. If any layer of the hardware-software stack does not maintain the guarantees required by the memory model at that layer’s interface, then parallel programs may not run correctly on the system. This necessitates full-stack memory model verification from high-level languages all the way down to processor RTL (register transfer language).

In this talk, I will describe techniques for full-stack memory model verification using tools from the Check suite developed by myself and others. In particular, I will focus on the CCI Check, TriCheck, and RTL Check tools.

At the core of the Check suite is its ability to model hardware implementations as a set of microarchitectural ordering axioms (invariants) in the domain-specific µspec language. This allows for efficient microarchitectural verification using happens-before graphs. The axioms can describe a variety of microarchitectural orderings, including those related to coherence protocols. While coherence and consistency are usually verified independently, their implementations are often closely coupled, which increases the possibility of bugs. To help mitigate these issues, CCI Check allows designers to verify that their coherence protocol and pipeline work correctly together to implement the consistency model of the processor.

The TriCheck tool allows designers of an ISA to reason about the ability of their intended hardware implementations to efficiently support high-level language requirements. TriCheck was utilised to detect deficiencies in the initial draft RISC -V ISA memory model that prevented it from supporting the C11 high-level language. TriCheck also discovered two counterexamples to compiler mappings from C11 to ARMv7 and Power that were previously thought to be proven correct.

The microarchitectural models of the Check suite are only valid if their axioms are actually maintained by the underlying implementation, which is written in RTL like Verilog. RTL Check, the newest addition to the Check suite, enables automated translation of the microarchitectural axioms to SystemVerilog Assertions (SVA) for a given litmus test. The generated assertions can then be automatically checked by a commercial RTL verifier like JasperGold to ensure that the RTL maintains the microarchitectural axioms for that litmus test. The translation from µspec to SVA is complicated by semantic mismatches between the axiomatic nature of µspec and the temporal worldview of SVA , and RTL Check uses novel techniques to bridge this gap.

The combination of CCI Check, TriCheck, and RTL Check with the rest of the Check suite provide system designers and implementers with the ability to conduct automated full-stack memory model verification of their systems for suites of litmus tests, greatly reducing the possibility of memory model bugs in their systems.

Bio:

Yatin Manerkar is a fourth-year PhD candidate in the Department of Computer Science at Princeton University, advised by Prof. Margaret Martonosi. Yatin’s research interests lie in the use of formal methods to verify parallel systems, specifically focusing on verification of memory model implementations at multiple levels of the hardware-software stack. He holds a BASc in Computer Engineering from the University of Waterloo and an M.S. from the University of Michigan, and has also worked full-time at Qualcomm Research. Yatin’s work has led to the discovery of bugs in a lazy coherence protocol, a “proven-correct” C11 atomic compiler mapping, a commercial compiler, and an open-source processor. He has also contributed to the development of the RISC -V ISA ’s memory model by finding deficiencies in its draft specification, and is currently a member of the RISC -V Memory Model Task Group. Yatin is a recipient of Princeton’s Wallace Memorial Fellowship.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.