Modeling and Verifying PSO Memory Model Using CSP

Modern processors deploy a variety of weak memory models for efficiency reasons. Total Store Order (TSO) is a widely used weak memory model which omits store-load constraint by allowing each core to employ a write buffer. Partial Store Order (PSO) is similar to TSO, but in consideration of higher performance, it does not guarantee that writes to different locations propagate to the shared memory following the program order. For understanding the reordering appearing in PSO precisely, we analyze this memory model by utilizing formal methods. In this paper, we apply Communicating Sequential Processes (CSP) to model PSO. By feeding the constructed model into the model checker Process Analysis Toolkit (PAT), we verify four properties. The requirements of TSO are more stringent than PSO, and then PSO must preserve write-read reordering and read-after-write elimination defined by TSO. The programs containing store-store fences between every two writes have the same outcomes under TSO and PSO, which is called outcomes consistency. Last but not the least, PSO should satisfy write-write reordering which indicates that two writes by the same thread may be reordered if they target different locations.