Fences and Synchronisation Idioms in Weak Memory Models

We present an axiomatic framework, implemented in the Coq proof assistant, to define weak memory models in terms of several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as SC from a weaker one. Finally, we provide formal requirements for abstract locks that guarantee SC semantics to data race free programs, and show that a particular implementation of locks matches these requirements