Fences in weak memory models (extended version)

Jade Alglave*, Luc Maranget, Susmit Sarkar, Peter Sewell

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

19 Citations (Scopus)

Abstract

We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and by 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. These tests can be used to explore the behaviour of processor implementations and the behaviour of models, and hence to compare the two against each other. We detail the results of experiments on Power and a model we base on them.

Original languageEnglish
Pages (from-to)170-205
Number of pages36
JournalFormal methods in system design
Volume40
Issue number2
DOIs
Publication statusPublished - Apr 2012

Keywords

  • Generic framework
  • Formal proofs
  • Testing tool
  • PowerPC
  • Weak memory models
  • Fences

Fingerprint

Dive into the research topics of 'Fences in weak memory models (extended version)'. Together they form a unique fingerprint.

Cite this