Weak Memory Models: From Axioms to Execution Steps


In a multiprocessor system, hardware performance optimizations can lead
to different threads observing different memory states at the same time.
The extent of this effect is described by a "memory consistency model".

This master thesis project focuses on the three models Sequential
Consistency (SC), Total Store Order (TSO) and Partial Store Order (PSO)
and the question whether the operational versions of these models by
Mantel, Perner, and Sauer (CSF, 2014) cover all executions that are
allowed in the respective axiomatic versions by Alglave (FMSD, 2012).

We propose an "anarchic" semantics to generate executions of a program,
independent of the memory-model. These executions can then be checked
for validity using the axiomatic model.  Furthermore, we present a
formal completeness claim for the operational model with respect to the
axiomatic model and this anarchic semantics.  We also argue that for TSO
and PSO, modifying the operational model by relaxing the program order
between writes and computations is necessary.

A formal proof relating each axiomatically valid execution in the
anarchic semantics to an execution in the respective operational model
is under development, using the Isabelle/HOL proof assistant.