Trace Semantics and Algebraic Laws for Total Store Order Memory Model

Modern multiprocessors deploy a variety of weak memory models (WMMs). Total Store Order (TSO) is a widely-used weak memory model in SPARC implementations and x86 architecture. It omits the store-load constraint by allowing each core to employ a write buffer. In this paper, we apply Unifying Theories of Programming (abbreviated as UTP) in investigating the trace semantics for TSO, acting in the denotational semantics style. A trace is expressed as a sequence of snapshots, which records the changes in registers, write buffers and the shared memory. All the valid execution results containing reorderings can be described after kicking out those that do not satisfy program order and modification order. This paper also presents a set of algebraic laws for TSO. We study the concept of head normal form, and every program can be expressed in the head normal form of the guarded choice which is able to model the execution of a program with reorderings. Then the linearizability of the TSO model is supported. Furthermore, we consider the linking between trace semantics and algebraic semantics. The linking is achieved through deriving trace semantics from algebraic semantics, and the derivation strategy under the TSO model is provided.