Armed cats: formal concurrency modelling at Arm
summary
Arm formalizes its CPU memory model in the cat language and runs litmus suites with herd+diy; the work yields two provably equivalent reformulations of the model, adds a precise mixed‑size‑access extension, and validates that extension by vast hardware experiments (including confirming the same rule applies to x86). The paper shows a concrete bug pattern in Linux dentry/lockref refcounts where mixed‑size accesses permit a bad outcome; adding the mixed‑size ordering inherited from global communication forbids that outcome and matches observed hardware behavior.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 2:25Arm architecture
- 3:37Formal memory model
- 4:57External visibility
- 6:08No cycles
- 8:14Contributions
- 10:28Pathways
- 11:41Example
- 14:15Extension principle
- 14:39Formal model
- 15:33Directory entry cache
- 15:57Local structure
- 16:34Litmus test
- 18:15Litmus test execution
- 20:40Questions
related talks
01h 11mProgramming language memory models: Problems, solutions, and directions
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
01h 02mThe Two Memory Models
19mAn Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
16mCompound Memory Models
30mA Tale of Shared Memory Concurrency in Programming Languages
28mCAAT: Consistency as a Theory
21mModel Checking C/C++ with Mixed-Size Accesses