Events

26 November 2008

Mercredi 26 novembre 2008, 11h, Batiment I, 1er étage

Relaxed memory models: an operational approach
Gérard Boudol
INRIA

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. This provides a frame in which the implementor, including the hardware designer, can deploy various optimizations, especially regarding memory operations, and a contract for the programmer, guaranteeing that well-synchronized, that is, data-race free code has a standard semantics. Memory models have been defined axiomatically, setting constraints on the order in which memory operations are allowed to occur with respect to each other. In this work we propose a new approach to formalizing a memory model. Namely, we propose this model to be part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a memory model where the write operations to the store are buffered. This allows 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.