TY - CHAP
T1 - Modelling and Verifying Programs Under the Total Store Order Memory Model in an Algebraic Semantics Style
AU - Xiao, Lili
AU - Zhu, Huibiao
AU - Bowen, Jonathan P.
AU - Chen, Sini
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
KW - Algebraic Laws
KW - Relaxed Memory Models
KW - Total Store Order (TSO)
KW - Unifying Theories of Programming (UTP)
KW - Verification
UR - https://www.scopus.com/pages/publications/85205093413
U2 - 10.1007/978-3-031-66673-5_11
DO - 10.1007/978-3-031-66673-5_11
M3 - 章节
AN - SCOPUS:85205093413
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 206
EP - 225
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PB - Springer Science and Business Media Deutschland GmbH
ER -