TY - GEN
T1 - Trace and Algebraic Semantics for Partial Store Order Memory Model
AU - Luo, Junfu
AU - Xiao, Lili
AU - Zhu, Huibiao
AU - Su, Ziqing
N1 - Publisher Copyright:
© 2024 IEEE.
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
KW - Algebraic Semantics
KW - PSO
KW - Trace Semantics
KW - UTP (Unifying Theories of Programming)
KW - Weak Memory Model
UR - https://www.scopus.com/pages/publications/85204099193
U2 - 10.1109/COMPSAC61105.2024.00348
DO - 10.1109/COMPSAC61105.2024.00348
M3 - 会议稿件
AN - SCOPUS:85204099193
T3 - Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024
SP - 2171
EP - 2176
BT - Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024
A2 - Shahriar, Hossain
A2 - Ohsaki, Hiroyuki
A2 - Sharmin, Moushumi
A2 - Towey, Dave
A2 - Majumder, AKM Jahangir Alam
A2 - Hori, Yoshiaki
A2 - Yang, Ji-Jiang
A2 - Takemoto, Michiharu
A2 - Sakib, Nazmus
A2 - Banno, Ryohei
A2 - Ahamed, Sheikh Iqbal
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 48th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2024
Y2 - 2 July 2024 through 4 July 2024
ER -