Microsoft Research,

Most current multiprocessor architectures and shared memory parallel program-ming languages are not sequentially consistent for parallel programs. Their pos-sible behaviors are characterized by weak or relaxed memory models. A memory model describes the way in which parallel programs can interact by reading and writing the shared memory. Thus, a relaxed memory model exhibits more be-haviors than sequential consistency (a “strong ” memory model). The fact that most architectures have relaxed memory models has been known for decades, and yet few programmers understand which are the exact behaviors a parallel program can have in such architectures. We argue in this thesis that the prob-lem stems from the difficulty in understanding the specification of these relaxed memory models. Firstly because few architectures or programming languages provide a formal definition of their memory model. And secondly because the majority of the existing formal definitions are axiomatic, which hinders their un-derstandability and makes them unsuitable for language-based techniques suc