Check: Research Tools and Papers

Princeton University

New!

Overview

From 2013 to the present, our work on specifying, verifying and translating memory consistency models has led to a number of publications, tool releases, and industry adoption.
Perhaps most importantly for a verification project, our verification tools have found numerous major design errors at this point. These include:
  • Fundamental deficiencies in the draft specification of a widely-discussed instruction set architecture (more info),
  • An error in the consistency implementation for a widely used simulator (more info),
  • A corner case in a proposed lazy coherence method (more info)(updated spec),
  • Errors in compiler mappings for translating high-level synchronization primitives onto particular instruction sets with weak memory model. And, an error in the formal proof previously thought to ensure the correctness of those mappings (more info).
Beyond these concrete bug discoveries, our tools have also been used to reproduce other known bugs and deepen understanding of them.

pipecheck



pipecheck

Tool Releases

  • PipeCheck: For verifying that the memory ordering provided by a particular microarchitectural implementation match that of the architectural memory model specification. (github)

  • CCICheck: For verifying coherence and consistency implementations in a unified manner. (github)

  • Web Interface: For building intuition about memory ordering and microarchitectural modeling and verification. (web interface to tool)

  • COATCheck: For verifying memory ordering issues in the face of virtual memory issues (virtual to physical page mappings) and other Hardware-OS Interface issues. (github)

  • ArMOR: For automatically specifying and translating between memory consistency models. (github)

  • TriCheck: Full-Stack MCM verification from high-level languages (e.g. C11) to microarchitectures. (github)

Press

April, 2017: Press regarding TriCheck and deficiences in the RISC-V ISA MCM Specification:
February, 2017: STARNet Center for Future Architectures Research (CFAR) Coverage of COATCheck Top Picks Selection
March, 2016: STARNet Center for Future Architectures Research (CFAR) Coverage of our work

Publications

Our work has been supported in part by the National Science Foundation*(under grants CCF-1117147, CCF-1253700, and others). (Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. In addition, we acknowledge past or ongoing support from CFAR, DARPA and others. The provided papers are subject to copyright by ACM, IEEE, or other entities.
  • Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee, "Transistency Models: Memory Ordering at the Hardware-OS Interfaces". IEEE Micro, 37 (3) (Top Picks of the 2016 Computer Architecture Conferences), May-June 2017

  • Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. "TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA", 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2017. (pdf)

  • Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. "Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings". CoRR, abs/1611.01507, 2016. (pdf)

  • Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee, "COATCheck: Verifying Memory Ordering at the Hardware-OS Interface", the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2016. (pdf)

  • Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. "CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface", the 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), December 2015. Nominated for Best Paper. (pdf) (slides) (poster)

  • Daniel Lustig, "Specifying, Verifying, and Translating Between Memory Consistency Models", Ph.D. Dissertation, November 2015. Honorable Mention, Bede Liu EE Department Dissertation Award (pdf)

  • Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi, "ArMOR: Defending Against Consistency Model Mismatches in Heterogeneous Architectures", the 42nd International Symposium on Computer Architecture (ISCA), June 2015. (pdf) (extended pdf and gallery) (slides)

  • Daniel Lustig, Michael Pellauer, and Margaret Martonosi, "Verifying Correct Microarchitectural Enforcement of Memory Consistency Models." IEEE Micro, 35 (3) (Top Picks of the 2014 Computer Architecture Conferences), May-June 2015 (pdf)

  • Daniel Lustig, Michael Pellauer, and Margaret Martonosi. PipeCheck: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models. 47th Annual IEEE/ACM International Symposium on Microarchitecture. December, 2014. Nominated for Best Paper Award. (pdf)

People

Tutorial

    We will be giving a tutorial about our tool suite on Sunday June 25, 2017 at ISCA in Toronto. The tutorial webpage includes agenda information and will be updated with slides and demo materials.

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