Program Transformations in Weak Memory Models

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.