ACL2 Seminar
February 3, 2014
Jade Alglave, University College London

Tutorial on weak memory
-----------------------

We propose a generic framework for weak memory, in which one can
represent Sequential Consistency (SC), Intel x86 (i.e. Sparc Total Store
Order, TSO), IBM Power, and a fragment of C++.

We offer a companion simulation tool, called herd, which allows the user
to specify the model of his choice in a concise way. Given a
specification of a model, the tool becomes a simulator for that model. 
 
In this talk, I will give a tutorial on how to use herd, which is in
fact a tutorial on weak memory.