Relaxed memory models: an operational approach

Gérard Boudol 1, 2 Gustavo Petri 1, 2
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
2 INDES - Secure Diffuse Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code.
Type de document :
Communication dans un congrès
POPL'09, Jan 2009, Savannah, GA,, United States. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00420352
Contributeur : Gustavo Petri <>
Soumis le : lundi 28 septembre 2009 - 16:54:12
Dernière modification le : jeudi 18 janvier 2018 - 01:25:32
Document(s) archivé(s) le : mercredi 16 juin 2010 - 00:11:27

Fichier

gg-popl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00420352, version 1

Citation

Gérard Boudol, Gustavo Petri. Relaxed memory models: an operational approach. POPL'09, Jan 2009, Savannah, GA,, United States. 2009. 〈inria-00420352〉

Partager

Métriques

Consultations de la notice

170

Téléchargements de fichiers

237