UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Fences in weak memory models

Alglave, J; Maranget, L; Sarkar, S; Sewell, P; (2010) Fences in weak memory models. In: (pp. pp. 258-272).

Full text not available from this repository.


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. © 2010 Springer-Verlag.

Type: Proceedings paper
Title: Fences in weak memory models
ISBN: 364214294X
DOI: 10.1007/978-3-642-14295-6_25
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1366415
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item