Fences in weak memory models

Jade Alglave; Luc Maranget; Susmit Sarkar; Peter Sewell

doi:10.1007/978-3-642-14295-6_25

Fences in weak memory models

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

^*Corresponding author for this work

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English
Title of host publication	Computer aided verification
Subtitle of host publication	22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings
Editors	Tayssir Touili, Byron Cook, Paul Jackson
Place of Publication	Heidelberg
Publisher	Springer-Verlag
Pages	258-272
Number of pages	15
ISBN (Electronic)	9783642142956
ISBN (Print)	9783642142949
DOIs	https://doi.org/10.1007/978-3-642-14295-6_25
Publication status	Published - 30 Jun 2010
Event	22nd International Conference on Computer Aided Verification - Edinburgh Duration: 15 Jul 2010 → 19 Jul 2010

Publication series

Name	Lecture notes in computer science
Volume	6174
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Computer Aided Verification
City	Edinburgh
Period	15/07/10 → 19/07/10

Access to Document

10.1007/978-3-642-14295-6_25

Cite this

Alglave, J., Maranget, L., Sarkar, S., & Sewell, P. (2010). Fences in weak memory models. In T. Touili, B. Cook, & P. Jackson (Eds.), Computer aided verification: 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings (pp. 258-272). (Lecture notes in computer science; Vol. 6174). Springer-Verlag. https://doi.org/10.1007/978-3-642-14295-6_25

@inproceedings{e9ea02b408d44238aef1b94c181dc450,

title = "Fences in weak memory models",

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.",

author = "Jade Alglave and Luc Maranget and Susmit Sarkar and Peter Sewell",

note = "Funding: The authors acknowledge support from EPSRC grants EP/F036345 and EP/H005633 and ANR grant ANR-06-SETI-010-02.; 22nd International Conference on Computer Aided Verification ; Conference date: 15-07-2010 Through 19-07-2010",

year = "2010",

month = jun,

day = "30",

doi = "10.1007/978-3-642-14295-6_25",

language = "English",

isbn = "9783642142949",

series = "Lecture notes in computer science",

publisher = "Springer-Verlag",

pages = "258--272",

editor = "Tayssir Touili and Byron Cook and Paul Jackson",

booktitle = "Computer aided verification",

address = "Germany",

}

Alglave, J, Maranget, L, Sarkar, S & Sewell, P 2010, Fences in weak memory models. in T Touili, B Cook & P Jackson (eds), Computer aided verification: 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings. Lecture notes in computer science, vol. 6174, Springer-Verlag, Heidelberg, pp. 258-272, 22nd International Conference on Computer Aided Verification, Edinburgh, 15/07/10. https://doi.org/10.1007/978-3-642-14295-6_25

Fences in weak memory models. / Alglave, Jade; Maranget, Luc; Sarkar, Susmit et al.
Computer aided verification: 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings. ed. / Tayssir Touili; Byron Cook; Paul Jackson. Heidelberg: Springer-Verlag, 2010. p. 258-272 (Lecture notes in computer science; Vol. 6174).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Fences in weak memory models

AU - Alglave, Jade

AU - Maranget, Luc

AU - Sarkar, Susmit

AU - Sewell, Peter

N1 - Funding: The authors acknowledge support from EPSRC grants EP/F036345 and EP/H005633 and ANR grant ANR-06-SETI-010-02.

PY - 2010/6/30

Y1 - 2010/6/30

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

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

UR - https://doi.org/10.1007/978-3-642-14295-6

U2 - 10.1007/978-3-642-14295-6_25

DO - 10.1007/978-3-642-14295-6_25

M3 - Conference contribution

SN - 9783642142949

T3 - Lecture notes in computer science

SP - 258

EP - 272

BT - Computer aided verification

A2 - Touili, Tayssir

A2 - Cook, Byron

A2 - Jackson, Paul

PB - Springer-Verlag

CY - Heidelberg

T2 - 22nd International Conference on Computer Aided Verification

Y2 - 15 July 2010 through 19 July 2010

ER -

Fences in weak memory models

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this