TY - GEN
T1 - Trace Semantics and Algebraic Laws for MCA ARMv8 Architecture Based on UTP
AU - Xiao, Lili
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - Hardware architectures like x86 and ARM provide relaxed memory models for efficiency reasons. The revised ARMv8 architecture is multi-copy atomic (MCA), which brings relaxed-memory effects through thread-local out-of-order, speculative execution and thread-local buffering. In this paper, we investigate the trace semantics for the MCA ARMv8 architecture, acting in the denotational semantics style based on Unifying Theories of Programming (UTP). In order to present all the valid execution results including reorderings of any program under ARMv8, a trace expressed as a sequence of snapshots is introduced, and it relies heavily on various dependencies. The snapshots record the change of variables of different types of actions. We also study the algebraic laws for MCA ARMv8, including a set of sequential and parallel expansion laws. The concept of head normal form is explored for each program, and every program is described in the form of guarded choice which can model the execution of a program with reorderings. Therefore, the linearizability for ARMv8 is supported.
AB - Hardware architectures like x86 and ARM provide relaxed memory models for efficiency reasons. The revised ARMv8 architecture is multi-copy atomic (MCA), which brings relaxed-memory effects through thread-local out-of-order, speculative execution and thread-local buffering. In this paper, we investigate the trace semantics for the MCA ARMv8 architecture, acting in the denotational semantics style based on Unifying Theories of Programming (UTP). In order to present all the valid execution results including reorderings of any program under ARMv8, a trace expressed as a sequence of snapshots is introduced, and it relies heavily on various dependencies. The snapshots record the change of variables of different types of actions. We also study the algebraic laws for MCA ARMv8, including a set of sequential and parallel expansion laws. The concept of head normal form is explored for each program, and every program is described in the form of guarded choice which can model the execution of a program with reorderings. Therefore, the linearizability for ARMv8 is supported.
KW - Algebraic laws
KW - MCA ARMv8 architecture
KW - Relaxed memory model
KW - Trace semantics
KW - Unifying Theories of Programming (UTP)
UR - https://www.scopus.com/pages/publications/85120520898
U2 - 10.1007/978-3-030-91265-9_5
DO - 10.1007/978-3-030-91265-9_5
M3 - 会议稿件
AN - SCOPUS:85120520898
SN - 9783030912642
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 81
EP - 101
BT - Dependable Software Engineering. Theories, Tools, and Applications - 7th International Symposium, SETTA 2021, Proceedings
A2 - Qin, Shengchao
A2 - Woodcock, Jim
A2 - Zhang, Wenhui
PB - Springer Science and Business Media Deutschland GmbH
T2 - 7th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2021
Y2 - 25 November 2021 through 27 November 2021
ER -