MemSynth

MemSynth is a system for automatic synthesis of axiomatic memory model specifications from litmus tests.

Read more about MemSynth in our PLDI 2017 paper.

Getting started

MemSynth requires Racket, Rosette, and Ocelot.

Assuming you have Racket installed, run:

raco pkg install --auto ocelot

to install Ocelot and Rosette.

To check that everything is working, run MemSynth's tests:

make test

Reproducing our experiments

Our artifact evaluation guide contains a thorough walkthrough to reproducing all the results from our paper.

Exploring the MemSynth API

One of our case studies uses MemSynth to automatically repair an existing memory model framework. This example also serves as a readable walkthrough of verification and synthesis using the MemSynth API.

Memory model synthesis

MemSynth (in the memsynth directory) provides synthesis and verification algorithms for memory models. These algorithms take as input a memory model framework sketch. Two examples of framework sketches are included in the frameworks directory: one based on work by Alglave et al. and the other by Mador-Haim et al..

We use the Alglave framework to synthesize a specification of the PowerPC memory model; that demonstration is in ppc0.rkt. It uses 768 litmus tests from Alglave's work, which are defined in our litmus test DSL in ppc-all.rkt.

Interacting with other tools

MemSynth supports the Herd format for litmus tests. We provide a compiler from that format (supporting only PowerPC tests, without control flow) to MemSynth's litmus test DSL.