Reasoning about weak memory models

We present a class of relaxed memory models, defined in Coq,
parameterised by the chosen permitted local reorderings of reads and
writes, and the visibility of inter- and intra-processor communications
through memory (e.g. store atomicity relaxation).  We prove results on
the required behaviour and placement of memory fences to restore a given
model (such as Sequential Consistency) from a weaker one.  Based on this
class of models we develop a tool, diy, that systematically and
automatically generates and runs litmus tests to determine properties of
processor implementations.  We detail the results of our experiments on
Power and the model we base on them. This work identified a rare
implementation error in Power 5 memory barriers (for which IBM is
providing a workaround); our results also suggest that Power 6 does not
suffer from this problem.