An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
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.
Thu 18 JanDisplayed time zone: London change
13:40 - 15:00
|How Hard is Weak-Memory Testing?
Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus UniversityPre-print
|An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Angus Hammond University of Cambridge, Zongyuan Liu Aarhus University, Thibaut Pérami University of Cambridge, Peter Sewell University of Cambridge, Lars Birkedal Aarhus University, Jean Pichon-Pharabod Aarhus UniversityPre-print
|Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
|Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University NijmegenPre-print