MemSynth
Synthesis-Aided Memory Model Development
MemSynth is an advanced automated reasoning tool for memory consistency models. It synthesizes axiomatic memory model specifications from a framework sketch and example litmus tests, and refines those specifications by generating new litmus tests exposing unresolved ambiguities. MemSynth also offers standard memory model verification and equivalence queries and outperforms existing tools.
We used MemSynth to synthesize memory model specifications for the x86 and PowerPC architectures in just a few seconds. In both cases, MemSynth found several ambiguities (including in the Intel documentation) and generated new litmus tests to resolve them. We also used MemSynth to synthesize a repair for an existing memory model tool that we could not fix by hand.
MemSynth’s reasoning engine is built on Ocelot, an embedding of relational logic (like Alloy) in the Rosette solver-aided programming language.
MemSynth is developed at the University of Washington by James Bornholt and Emina Torlak.
Read the paper
Synthesizing Memory Models from Framework Sketches and Litmus Tests.
- Paper (PDF, 280 kB)
- Artifact instructions (HTML)
Watch the video
Get the code
MemSynth is available on GitHub.
Browse the results
This page hosts the full synthesis results — specifications and litmus tests — for the experiments in the paper. We synthesized correct specifications for both the PowerPC and x86 memory models, and discovered several ambiguities in each.