Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14295-6_25 | CAV |
Keywords | Field | DocType |
litmus test,memory model,memory barrier,weak memory model,memory fence,required behaviour,store atomicity relaxation,intra-processor communication,sequential consistency,rare implementation error,local reorderings | Extended memory,Computer science,Distributed memory,Algorithm,Theoretical computer science,Memory model,Memory management,Memory map,Overlay,Distributed shared memory,Flat memory model | Conference |
Volume | ISSN | ISBN |
6174 | 0302-9743 | 3-642-14294-X |
Citations | PageRank | References |
36 | 1.93 | 15 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jade Alglave | 1 | 608 | 26.53 |
| Luc Maranget | 2 | 808 | 49.83 |
| Susmit Sarkar | 3 | 744 | 30.76 |
| Peter Sewell | 4 | 1446 | 68.16 |