Herding cats: Modelling, simulation, testing, and data-mining for weak memory

International audienceThere is a joke where a physicist and a mathematician are asked to herd cats. The physicist starts with an infinitely large pen which he reduces until it is of reasonable diameter yet contains all the cats. The mathematician builds a fence around himself and declares the outside to be the inside. Defining memory models is akin to herding cats: both the physicist's or mathematician's attitudes are tempting, but neither can go without the other. When executing shared-memory concurrent programs, modern multiprocessors (e.g. Intel x86, IBM Power or ARM) exhibit be-haviours (e.g. store buffering or load delaying) that contradict the programming model we have been taught at school, namely Lam-port's Sequential Consistency (SC) [4]. Indeed, for performance reasons, multiprocessors implement weak memory models. Ideally, we believe that these models would benefit from stating principles that underpin weak memory as a whole, not just one par-ticular architecture or language. Not only would it be aesthetically pleasing, but it would allow more informed decisions on the design of high-level memory models, ease the conception and proofs of compilation schemes, and allow the reusability of simulation and verification techniques from one model to another. We outline our work below – full details can be found in [1]. As foundation, we propose an axiomatic generic framework for mod-elling weak memory hardware. We have four axioms: (1) SC PER LOCATION expresses memory coherence; (2) NO THIN AIR defines the minimal causality constraints enforced by deployed hardware; (3) OBSERVATION reflects the ordering of writes induced by mem-ory fences, as observed by an external thread; (4) PROPAGATION states how one can use memory fences to restore SC on top of a weak memory model. We instantiate our framework for SC, TSO, C++ restricted to release-acquire atomics, Power, and ARM. For Power, we compare our model to a preceding operational model [5, 6] in which we found a flaw. To facilitate the comparison, we define in the Coq proof assistant an operational model that we show equivalent to our axiomatic model (see also www. We also propose a model for ARM, based on extensive testing of ARM hardware, and its presumed proximity to Power hard-ware (see also diy.inria.fr/cats/model-arm). Our testing on this ar-chitecture revealed a behaviour later acknowledged as a bug by ARM, and more recently we discovered 31 additional anoma-lies, documented in our experimental reports at diy.inria.fr/cats