An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
summary
Claims a new separation logic AxSL for the Arm‑A user‑mode axiomatic model that lets relaxed reads/writes transfer resources when they induce ordering, implemented by inventing an OPAC semantics that guesses a whole-program memory‑event graph up front and then checks executions against it, mechanised in Iris with new assertions like register-point and tie-to and an adequacy proof by stratified traversal; artifacts are available and the logic is proven sound, though coherence support and some usability abstractions are still missing.
AI-written summary · about
chapters (10)
- 0:00Axiomatic reasoning on relaxed Arm-A
- 1:04Load buffering in weak memory
- 2:29Compositional reasoning failure
- 3:54Arm memory model challenges
- 5:17OPA semantics for operational reasoning
- 7:03XEL program logic on OPA
- 8:30Message passing proof with XEL
- 12:02Soundness proof and adequacy
- 12:44Limitations and future work
- 13:28Q&A
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
26mArmed cats: formal concurrency modelling at Arm
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
01h 11mProgramming language memory models: Problems, solutions, and directions
16mPersistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-
17mPutting Weak Memory in Order via a Promising Intermediate Representation
21mCSL and relaxed memory