Away From Linear Models of Concurrent Programs

Traditional approaches to imperative programming language semantics rely on first defining how each individual statement modifies the memory state, and then composing these definitions into a whole program via the interpretation of the sequential composition operator: the humble semicolon. The creation of the multiprocessor and advent of parallelism began to challenge this model. No longer was a program a single, linear sequence of statements, but it had statements which might occur in one order or another, or even simultaneously. To add to the complexity, compilers and hardware began to optimise their input programs, reordering and removing statements to improve runtime performance. The resulting stack of transformations and complications caused runtime executions to drift progressively further away from the program that a programmer believed they were writing. Several approaches to this have appeared: process calculi which forbid processes from sharing memory and instead force them to communicate directly, maintaining sequential consistency, in which an execution must at least appear to be respecting the ordered sequence of statements model, and permitting weak memory ordering, in which an execution must maintain orders involving explicitly synchronised accesses but is free to reorder everything else. While weak memory is preferred by engineers building high-performance code, due to the relatively high cost of both passing messages and maintaining sequential consistency, the problem of creating a sound weak memory semantics for a real-world programming language with shared memory concurrency has yet to be fully solved. Here we present a weakly ordered semantics for shared memory concurrency, given as an extension to a previously published model. We show that the existing model can be integrated into reasoning techniques which rely on an operational semantics, and that program transformations which cannot introduce new behaviours can be expressed as a relation over the objects of this semantics. We then add a layer of abstraction to the model which allows us to represent dynamic memory allocation in a weak memory context for the first time.