Concurrent programming has historically had to deal with problems related to already established single-threaded optimizations. The complexity involved in concurrent program analysis increases significantly from single-threaded program analysis, even without taking single-threaded optimizations into account, and increases significantly even more so when single-threaded optimizations are involved. Relaxed memory models enable reasoning about concurrent programs in a framework that captures behaviors due to such program optimizations. A key property of relaxed memory models is that programs without data races behave as if no optimizations have to be taken into account, that is, all behaviors of data-race-free programs should be sequentially consistent. This property is known as data-race-free sequential consistency, or DRF-SC.
In this thesis, we develop an operational semantics for a relaxed memory model inspired by the Go programming language, with shared memory, delayed read semantics, and synchronization based on message passing. We will prove the DRF-SC property formally for the relaxed memory model, along with inspecting behaviors and optimizations enabled by the semantics through litmus tests. The approach is directly based on an already developed operational semantics in Daniel Fava, Martin Steffen, and Volker Stolz, Operational Semantics of a Weak Memory Model with Channel Synchronization, in the Journal of Logical and Algebraic Methods in Programming (vol 103, 2019).
| supervisors | Martin Steffen |