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

Artifacts evaluated. Artifacts available.

Synthesizing Memory Models from Framework Sketches and Litmus Tests.

James Bornholt and Emina Torlak
PLDI 2017

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.