Sound and Complete Reachability Analysis under PSO

Abstract: Modern multiprocessor systems use weak (relaxed) memory models in order to execute memory sharing multi-threaded code in an efficient manner, but are much harder for programmers to reason about than systems using the sequential consistency memory model. The SB abstraction and its implementation in the Memorax tool allows sound and complete checking of control state reachability under the TSO memory model, used in modern x86 processors. In this paper, I present a formalisation of the PSO memory model using the semantics of the Sun SPARC documentation and an alternate semantic, called Partial Write Serialisation, I conjecture to be equivalent with my formalisation under the control state reachability problem. PWS is proved to be a well-structured system which allows sound and complete reachability analysis. An implementation of PWS is presented  as part of the Memorax tool and demonstrated  experimentally to be capable of analysing reachability and inferring minimal fence sets on many non-trivial and real world examples in reasonable time and memory usage.