Memory models define an interface between programs written insome language and their implementation, determining which be-haviour the memory (and thus a program) is allowed to have ina given model. A minimal guarantee memory models should pro-vide to the programmer is that well-synchronized, that is, data-racefree code has a standard semantics. Traditionally, memory mod-els are defined axiomatically, setting constraints on the order inwhich memory operations are allowed to occur, and the program-ming language semantics is implicit as determining some of theseconstraints. In this work we propose a new approach to formalizinga memory model in which the model itself is part of a weak op-erational semantics for a (possibly concurrent) programming lan-guage. We formalize in this way a model that allows write opera-tions to the store to be buffered. This enables us to derive the or-dering constraints from the weak semantics of programs, and toprove, at the programming language level, that the weak semanticsimplements the usual interleaving semantics for data-race free pro-grams, hence in particular that it implements the usual semanticsfor sequential code.
展开▼
