Fences in Weak Memory Models

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Original languageEnglish
Title of host publicationCOMPUTER AIDED VERIFICATION, PROCEEDINGS
EditorsT Touili, B Cook, P Jackson
Place of PublicationBERLIN
PublisherSpringer-Verlag
Pages258-272
Number of pages15
ISBN (Print)978-3-642-14294-9
Publication statusPublished - 2010
Event22nd International Conference on Computer Aided Verification - Edinburgh
Duration: 15 Jul 201019 Jul 2010

Publication series

NameLecture Notes in Computer Science
PublisherSPRINGER-VERLAG BERLIN
Volume6174
ISSN (Print)0302-9743

Conference

Conference22nd International Conference on Computer Aided Verification
CityEdinburgh
Period15/07/1019/07/10

Fingerprint

Dive into the research topics of 'Fences in Weak Memory Models'. Together they form a unique fingerprint.

Cite this