Tutorial on Demystifying Memory Models Across the Computing Stack
May 24, 2019
Tutorial on Demystifying Memory Models Across the Computing Stack
in conjunction with ISCA 2019
Phoenix, Arizona, USA
June 22, 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)