ISCA Tutorial: Demystifying Memory Models Across the Computing Stack
Phoenix, Arizona, USA
June 22, 2019
Early registration deadline: May 24th, 2019
Do you find memory consistency models inscrutable? Does your parallel
program mysteriously crash or give counterintuitive results? Do you lie
awake at night wondering if your processor is buggy? Then this tutorial
is for you!
Memory consistency models (MCMs) specify ordering rules which
constrain the values that can be read by loads in parallel programs.
Correct MCM implementations are critical to parallel system correctness,
and each layer of the hardware/software stack is responsible for
enforcing some of the orderings required. However, MCMs are notoriously
complicated to specify and verify, and often require examination of many
counterintuitive corner cases.
This tutorial will teach hardware and software researchers how to
navigate the world of MCMs through the Check suite, a collection of
automated tools for formal MCM verification developed by our group at
Princeton over the last five years. With tools for every layer of the
stack from high-level languages to Verilog RTL, we have something for
virtually all FCRC attendees. Topics we will cover include:
-automated all-program inductive proofs of hardware MCM correctness
-how to balance high-level language MCM requirements against hardware optimizations
-MCM verification of real Verilog RTL!
Along the way, we’ll point out some of the real-world bugs we’ve
discovered in the course of our work, including IBM compiler flaws,
issues with the RISC-V ISA, and even a problem with the C++ memory
model.
So whether you want to verify that your processor correctly
implements its MCM, or you’re wondering what fences to include in your
shiny new ISA, or you just want to learn more about memory consistency,
please do attend our tutorial on the morning of Saturday, June 22nd at
FCRC 2019 in Phoenix, AZ. We hope to see you there!
FCRC Registration:
https://www.cvent.com/events/fcrc-2019/registration-78e7bfed5fc9437291908ea8f0950311.aspx?fqp=true
ISCA Tutorial List:
https://iscaconf.org/isca2019/workshops.html
ORGANIZERS:
Yatin Manerkar, Caroline Trippel, Prof. Margaret Martonosi (Princeton University)