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

[github-actions]

This paper was randomly selected as your next reading.

An Axiomatic Basis for Computer Programming on the Relaxed ArmA Architecture: The AxSL Logic

Very relaxed concurrency memory models, like those of the ArmA, RISCV, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the readsfrom relation always both induce order in the execution. Instead, outoforder 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 syntaxdirected, 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 ArmA, that captures the finegrained reasoning underpinning the lowoverhead synchronisation mechanisms used by highperformance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce interthread 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 ArmA. Our approach

Hammond, Angus, et al. “An Axiomatic Basis for Computer Programming on the Relaxed ArmA Architecture: The AxSL Logic. Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 60437. Crossref, https://doi.org/10.1145/3632863.

Merge this PR to apply selection.