28/10/2008, 16:30 — 17:30 — Tagus-1.1
Gustavo Petri, INRIA, Sophia-Antipolis
Relaxed Memory Models: an Operational Approach
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.
