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) (pdf) (quick start guide)
- MCM Background and Basics of our Approach (roughly 30 minutes) (pdf)
- Verifying microarchitectural implementations against ISA-specified MCMs: PipeCheck description and hands-on example of specifying microarchitectures. (40 minutes) (pdf)
- Coffee break and hands-on practice. (30 minutes)
- PipeCheck hands-on example continues: Verifying examples. (30 minutes) (pdf)
- Spanning the Hardware-Software Interface: TriCheck with hands-on example. (45 minutes) (pdf)
- Future possibilities and Wrap-up. (15 minutes) (pdf)(reading list for more info)
