An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic

TY - JOUR

T1 - An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture

T2 - The AxSL Logic

AU - Hammond, Angus

AU - Liu, Zongyuan

AU - Pérami, Thibaut

AU - Sewell, Peter

AU - Birkedal, Lars

AU - Pichon-Pharabod, Jean

N1 - Publisher Copyright: © 2024 Owner/Author.

PY - 2024/1/5

Y1 - 2024/1/5

N2 - Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the 'current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.

AB - Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the 'current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.

KW - Arm

KW - Iris

KW - program logic

KW - relaxed memory models

KW - separation logic

UR - http://www.scopus.com/inward/record.url?scp=85182263167&partnerID=8YFLogxK

U2 - 10.1145/3632863

DO - 10.1145/3632863

M3 - Journal article

AN - SCOPUS:85182263167

SN - 2475-1421

VL - 8

SP - 604

EP - 637

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

M1 - 21

ER -