Skip to content

An advanced automated reasoning tool for memory consistency model specifications.

License

Notifications You must be signed in to change notification settings

uwplse/memsynth

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

5 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

MemSynth

Build Status

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.

About

An advanced automated reasoning tool for memory consistency model specifications.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages