Fences and Synchronisation Idioms in Weak Memory Models

Abstract : We present an axiomatic framework, implemented in the Coq proof assistant, to define weak memory models in terms of several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as SC from a weaker one. Finally, we provide formal requirements for abstract locks that guarantee SC semantics to data race free programs, and show that a particular implementation of locks matches these requirements.
Type de document :
Rapport
[Research Report] RR-7152, INRIA. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00440863
Contributeur : Alglave Jade <>
Soumis le : samedi 12 décembre 2009 - 17:53:01
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : jeudi 17 juin 2010 - 23:37:37

Fichier

rr-7152.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00440863, version 1

Collections

Citation

Jade Alglave, Luc Maranget. Fences and Synchronisation Idioms in Weak Memory Models. [Research Report] RR-7152, INRIA. 2009. 〈inria-00440863〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

102