Modelling and Verifying Programs Under the Total Store Order Memory Model in an Algebraic Semantics Style

Modelling and verification of multi-threaded programs are difficult since one must consider all the ways that instructions in different threads can be interleaved. Modern hardware architectures and mainstream programming languages employ relaxed memory models for efficiency purposes, and the additional interleavings from them make the modelling and verification more complex. Total Store Order (TSO) is a widely used relaxed memory model in SPARC implementations and x86 architecture. In this paper, we are committed to proposing a lightweight method for formally modelling and verifying programs under the TSO memory model. Above all, we apply Unifying Theories of Programming (UTP) to investigate a set of algebraic laws, which can dynamically generate configuration sequences of programs under TSO. At the meantime, the information of each configuration is recorded. During this process, we define three properties (including Write-Read Reordering, Read-after-Write Elimination and Barrier) related to the unique features of TSO, and check whether the properties are satisfied. The algebraic laws are implemented in the rewriting engine Maude, and the verification is also conducted in Maude. The verification results show that the properties are all in line with our expectations.