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.

Agenda

  • Introduction and Motivation (roughly 30 minutes)
  • MCM Background and Basics of our Approach (roughly 30 minutes)
  • Verifying microarchitectural implementations against ISA-specified MCMs: PipeCheck description and hands-on example. (30 minutes)
  • Expanding Treatment of Coherence and Memory Hierarchies: CCICheck hands-on example. (15 minutes)
  • Coffee break. (30 minutes)
  • Spanning the Hardware-Software Interface, part 1: COATCheck with hands-on example. (30 minutes)
  • Spanning the Hardware-Software Interface, part 2: TriCheck with hands-on example. (30 minutes)
  • Future possibilities and Wrap-up. (15 minutes)



pipecheck

Demos

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

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