Demystifying Memory Models Across The Computing Stack

Yatin Manerkar, Caroline Trippel, Prof. Margaret Martonosi
Princeton University
Date and Time: Morning of Saturday, June 22nd, 2019
Register Now!

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.

Please download VirtualBox before the tutorial!



pipecheck

Agenda and Slides

Demos

Tutorial Files

We provide a virtual machine that contains all necessary tutorial files. It can be run with VirtualBox.
Download VM

https://check.cs.princeton.edu/

https://mrmgroup.cs.princeton.edu/