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

Explore a 19-minute conference talk from POPL 2024 that introduces AxSL, a separation logic for the relaxed memory model of Arm-A architecture. Delve into the challenges of designing syntax-directed, modular reasoning methods for very relaxed concurrency memory models used in Arm-A, RISC-V, and IBM Power hardware architectures. Learn how AxSL captures fine-grained reasoning for low-overhead synchronisation mechanisms in high-performance systems code, allowing resource transfer using relaxed reads and writes. Discover the mechanization of AxSL in the Iris separation logic framework, its application to key examples, and its soundness proof with respect to the axiomatic memory model of Arm-A. Gain insights into a potential approach for compositional reasoning applicable to similar models and the combination of production concurrency models with full-scale instruction set architectures.