一句话：提出 AxSL 分离逻辑，支持 Arm-A 宽松内存下的模块化验证，并在 Iris 中机械化证明其相对 Arm-A 公理模型的可靠性。
Arm-A、RISC-V、Power 等宽松并发内存模型允许乱序执行，破坏程序顺序与 reads-from 关系带来的顺序直觉，使程序没有“当前”状态，从而难以设计语法导向、模块化的 Hoare 式推理。本文提出 AxSL：面向 Arm-A 宽松内存模型的分离逻辑，允许在宽松读/写能够产生线程间顺序时转移任意资源，以支持高性能系统代码中低开销同步的细粒度推理。作者在 Iris 分离逻辑框架中机械化 AxSL，给出关键例子，并证明其相对于 Arm-A 公理化内存模型的可靠性。该方案对公理模型和指令集语义大多通用，为其他类似内存模型及生产级并发模型与完整 ISA 的组合提供了组合推理路径。
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.
@article{paperbot2582,
title = {An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic},
author = {Angus Hammond and Zongyuan Liu and Thibaut Pérami and Peter Sewell and Lars Birkedal and Jean Pichon-Pharabod},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632863}
}