RC11z (Allocation-Aware RC11)
A variant of RC11 — the operational RC11-RAR fragment with relaxed and release-acquire accesses — extended with an explicit model of pointers and memory allocation, developed to verify safe memory reclamation (Read-Copy-Update, RCU) under weak memory. Allocation and deallocation are modelled as ordinary write events in the same memory state; a read that takes its value from an allocation or deallocation event therefore surfaces as a read-from-uninitialised or use-after-free error, making the ABA / reclamation hazards of lock-free code visible to the model. Combined with an ownership discipline and an Owicki-Gries logic, and mechanised in Isabelle/HOL. Locally dubbed RC11z, the 'z' standing for the zeroing allocation/deallocation events.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- yes x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- no Load/Store
- Other local transformations
- no Speculative load intro.
- yes Roach motel
- yes Strengthening
- yes Trace preserving
- no Common subexpr. elim.
- Global transformations
- yes Register promotion
- yes Thread inlining
- Reasoning guarantees
- yes External DRF
- yes Coherence
- no No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Equivalent to
- Repaired C11 (RC11) — RC11z extends the operational RC11-RAR semantics so that allocation and deallocation are explicit write events; a read taking its value from such an event surfaces as a read-from-uninitialised or use-after-free error. On the concurrency behaviours of well-allocated programs it coincides with RC11 — the added allocation layer exists to verify safe memory reclamation (RCU).
References
- Mikhail Semenyuk, Mark Batty, Brijesh Dongol. Verifying Read-Copy Update Under RC11. SEFM 2023 (LNCS 14323), 2023. doi:10.1007/978-3-031-47115-5_17
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer. Repairing Sequential Consistency in C/C++11. PLDI 2017, 2017. doi:10.1145/3062341.3062352