A diy “Seven” tutorial

Version 7.47+1

August 21, 2017

diy7 is a tool suite for testing shared memory models. We provide several tools, litmus7 (Part I) and klitmus7 (Sec. 5) for running tests, diy7 generators (Part II) for producing tests from concise specifications, and herd7 (Part III) for simulating memory models. In Part IV we describe a few concrete experiments, illustrating frequent usage patterns of diy7 generators and of litmus7.

The software is written in Objective Caml, and released as sources. The web site of diy7 is http://diy.inria.fr/, authors can be contacted at diy-devel@inria.fr. This software is released under the terms of the CeCILL-B Free Software License Agreement.

This document in Postscript and Pdf.

The authors of the diy7 tool suite are Jade Alglave and Luc Maranget, with contributions by Jacques-Pascal Deplaix (litmus7 for C) and Keryan Didier (herd7 semantics for ARMv8 and simple ARMv8 models).

Past contributors are Susmit Sarkar (litmus), Tyler Sorensen (herd), John Wickerson (herd). The tool litmus is inspired from an unreleased prototype by Thomas Braibant and Francesco Zappa Nardelli.

This document was translated from LATEX by HEVEA.