MemSynth

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.

Publications

• James Bornholt and Emina Torlak. Synthesizing Memory Models from Framework Sketches and Litmus Tests. In Proc. of the 38th PLDI, Jun 2017. [pdf] [slides]

Software

MemSynth is hosted on GitHub at https://github.com/uwplse/memsynth.

MemSynth’s reasoning engine is built on Ocelot, an embedding of relational logic (like Alloy) in the Rosette solver-aided programming language.

The artifact for the PLDI 2017 paper is available here.