Fences in Weak Memory Models

Abstract : We present here an axiomatic framework, implemented in the Coq proof assistant, for defining weak memory models in terms of several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory. In this context, we provide formal definition of weak memory models induced by architectures, illustrated by definitions of SC and Sparc TSO. Moreover, we define a comparison over architectures, an architecture A1 being weaker than another one A2 when A1 allows more behaviours than A2. In addition, we provide a characterisation of behaviours allowed by A1 which are also valid on A2. By that means, we provide a simple characterisation of SC and TSO behaviours on any weaker architecture. We also provide an abstract notion of what should be the action and placement of fences to restore a given model from a weaker one. Our framework led us to a model of a significant fragment of PowerPC with fences. In the absence of any public formal model of PowerPC, we base our study on intensive testing. We illustrate our approach by providing several tests that highlight the parameters of our model.
Type de document :
Rapport
[Research Report] RR-7010, INRIA. 2009
Liste complète des métadonnées

https://hal.inria.fr/inria-00408568
Contributeur : Alglave Jade <>
Soumis le : lundi 3 août 2009 - 12:40:06
Dernière modification le : samedi 17 septembre 2016 - 01:32:57
Document(s) archivé(s) le : mardi 15 juin 2010 - 19:12:29

Fichiers

RR-7010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00408568, version 1

Collections

Citation

Alglave Jade, Luc Maranget. Fences in Weak Memory Models. [Research Report] RR-7010, INRIA. 2009. 〈inria-00408568〉

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

91