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.
James Bornholt and Emina Torlak. Synthesizing Memory Models from Framework Sketches and Litmus Tests. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Jun 2017. [pdf] [slides]
MemSynth is hosted on Github at https://github.com/uwplse/memsynth.
The artifact for the PLDI 2017 paper is available here.