A diy “Seven” tutorial

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 Antoine Hacquerd (X86_64 architecture), Boqun Feng (contribution to the jingle tool), Kate 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.

• Contents

• Running tests with litmus7
• Generating tests
• Simulating memory models with herd7
• Some examples
• References

This document was translated from L^AT_EX by H^EV^EA.