Fences in Weak Memory Models

Jade Alglave

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). 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.

We prove results on the required behaviour and placement of synchronisation primitives to restore a given model, such as Sequential Consistency (SC), from a weaker one. We implemented these results in our offence tool, which places either lock-based or lock-free synchronisation in a x86 or Power program to ensure what we call its stability, i.e. it behaves as if running on SC.