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.
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