Trace and Algebraic Semantics for Partial Store Order Memory Model

Contemporary multiprocessor systems often use weak memory models (WMMs), including Partial Store Order (PSO) in some SPARC implementations. PSO relaxes the store-store constraint by allowing individual cores to use a write buffer for different memory locations. This paper employs the Unifying Theories of Programming (UTP) framework to investigate PSO's trace semantics, acting in the denotational semantics style. In this context, a trace is represented as a sequence of snapshots that track changes in registers, write buffers, and shared memory. Our approach generates the complete set of valid execution outcomes, including potential reorderings, while adhering to proper principles. This paper also introduces a set of algebraic laws tailored for PSO utilizing the concept of 'head normal form{\prime}. With the introduction of guarded choice, every program can be represented by head normal form. This representation models program execution in the presence of reorderings within the PSO model. Additionally, we also explores the relationship between trace semantics and algebraic semantics, establishing a connection by deriving trace semantics from algebraic semantics.