Why Memory Consistency Models Matter...

And tools for analyzing and verifying them.

Yatin Manerkar, Caroline Trippel, Prof. Margaret Martonosi
Princeton University

Goals

This tutorial will start by making a case for why Memory Consistency Models matter now more than ever! We will then give participants a concrete set of tools and techniques for broader MCM research, based on the approaches in our Check toolsuite. For each portion of the tutorial, participants will get the chance to experiment with hands-on examples using the tools and modeling techniques. We hope to get you thinking about future work possibilities in this area. In the process, we also hope to foster the broadening of a research community active in and conversant about MCM issues.
Please download VirtualBox before the tutorial!

Agenda

  • Introduction and Motivation (roughly 20 minutes)
  • MCM Background and Basics of our Approach (roughly 30 minutes)
  • Verifying microarchitectural implementations against ISA-specified MCMs: PipeCheck description and hands-on example of specifying microarchitectures. (40 minutes)
  • Coffee break and hands-on practice. (30 minutes)
  • PipeCheck hands-on example continues: Verifying examples. (30 minutes)
  • Spanning the Hardware-Software Interface: TriCheck with hands-on example. (45 minutes)
  • Future possibilities and Wrap-up. (15 minutes)



pipecheck

Demos

Tutorial Files

This is a virtual machine that contains all necessary tutorial files. It can be run with VirtualBox. Please download VirtualBox before the tutorial!
WARNING: This VM is currently preliminary; changes to it may be made before the tutorial.
Download VM

http://check.cs.princeton.edu/

http://mrmgroup.cs.princeton.edu/