Program Transformations in Weak Memory Models
View/ Open
Date
2009Author
Sevcik, Jaroslav
Metadata
Abstract
We analyse the validity of common optimisations on multi-threaded programs in
two memory models—the DRF guarantee and the Java Memory Model. Unlike
in the single-threaded world, even simple program transformations, such as common
subexpression elimination, can introduce new behaviours in shared-memory
multi-threading with an interleaved semantics. To validate such optimisations,
most current programming languages define weaker semantics, called memory
models, that aim to allow such transformations while providing reasonable guarantees.
In this thesis, we consider common program transformations and analyse
their safety in the two most widely used language memory models: (i) the DRF
guarantee, which promises sequentially consistent behaviours for data race free
programs, and (ii) the Java Memory Model, which is the semantics of multithreaded
Java. The DRF guarantee is the semantics of Ada and it has been
proposed as the semantics of the upcoming revision of C++. Our key results
are: (i) we prove that a large class of elimination and reordering transformations
satisfies the DRF guarantee; (ii) we find that the Java language is more
restrictive—despite the claims in the specification, the Java Memory Model does
not allow some important program transformations, such as common subexpression
elimination.
To establish the safety results, we develop a trace semantic framework and
describe important program optimisations as relations on sets of traces. We
prove that all our elimination and reordering transformations satisfy the DRF
guarantee, i.e., the semantic transformations cannot introduce new behaviours
for data race free programs. Moreover, we prove that all the transformations
preserve data race freedom. This ensures safety of transformations composed
from eliminations and reorderings. In addition to the DRF guarantee, we prove
that for arbitrary programs, our transformations prevent values appearing “outof-
thin-air”—if a program does not contain constant c and does not perform any
operation that could create c, then no transformation of the program can output
c. We give an application of the semantic framework to a concrete language and
prove safety of several simple syntactic transformations.
We employ similar semantic techniques to prove validity of several classes of
transformations, such as the elimination of an overwritten write or reordering
of independent memory accesses, in the Java Memory Model. To establish the
iii
negative results for the Java Memory Model, we provide counterexamples showing
that several common optimisations can introduce new behaviours and thus are
not safe.