Fences in weak memory models (extended version)

Abstract : We present a class of relaxed memory models, defined in Coq, parame-terised 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 system-atically 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.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2012, 40 (2), pp.170 - 205. 〈10.1007/s10703-011-0135-z〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01100778
Contributeur : Luc Maranget <>
Soumis le : mercredi 7 janvier 2015 - 09:48:16
Dernière modification le : mardi 10 février 2015 - 15:06:33
Document(s) archivé(s) le : mercredi 8 avril 2015 - 11:25:22

Fichier

fences-fmsd12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell. Fences in weak memory models (extended version). Formal Methods in System Design, Springer Verlag, 2012, 40 (2), pp.170 - 205. 〈10.1007/s10703-011-0135-z〉. 〈hal-01100778〉

Partager

Métriques

Consultations de
la notice

138

Téléchargements du document

81