Goals

Concurrency and parallelism have proliferated throughout the hardware/software stack in today's computing landscape, with various threads/cores/accelerators communicating with each other via shared memory. Memory consistency models (MCMs) specify ordering rules which constrain the values that can be read by load operations in such shared-memory programs. MCMs are defined for both high-level languages (HLLs) like Java and C++, as well as hardware instruction sets (ISAs) like x86, ARM, and RISC-V. They have ramifications throughout the computing stack, and their correct implementations are critical to parallel system correctness.

Despite their importance, MCMs are often misunderstood and shunned by the majority of the systems community. This has led to incorrect hardware, flawed ISA specifications, and broken compiler mappings from HLL synchronization primitives to assembly language instructions.

In this tutorial, we will demystify MCMs using the Check suite, a concrete set of tools and techniques for MCM verification that span the entire hardware/software stack. Tutorial participants will get the chance to experiment with hands-on examples using our tools and modelling techniques. The overarching goal of our work is to give systems researchers the ability to automatically and thoroughly verify the MCM properties of their systems by themselves, without needing to enlist the help of formal methods experts. In the process, we hope to foster the broadening of a research community active in and conversant about MCM issues.

This tutorial builds on our prior tutorial on MCM verification from ISCA 2017, and includes new material on automated inductive MCM correctness proofs for hardware and MCM verification of Verilog RTL.