Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
This program is tentative and subject to change.
Read-Copy-Update (RCU) is a critical synchronization mechanism for concurrent data structures,
enabling efficient deferred memory reclamation.
However, implementing and using RCU correctly is challenging due to its inherent concurrency complexities.
While previous work verified RCU,
they either relied on unrealistic assumptions of sequentially consistent (SC) memory model
or lacked three key features of general-purpose RCU libraries:
modular specification, switchable critical sections, and concurrent writer support.
We present the first formal verification of a general-purpose RCU in realistic \emph{relaxed memory consistency} (RMC),
addressing the challenges posed by these features.
To achieve modular specification that encompasses relaxed behaviors, we extend existing SC specifications to account for explicit synchronization.
To support switchable critical sections, which require read-after-write (RAW) synchronization, we introduce a reasoning principle for RAW-synchronizing SC fences.
Using this principle, we also present the first formal verification of Peterson's mutex in RMC.
To support concurrent writers performing partially ordered writes,
we avoid assuming a total order of links and instead formulate invariants based on per-node incoming link histories.
Our proofs are mechanized in the iRC11 relaxed memory separation logic, built upon Iris, in Rocq.
This program is tentative and subject to change.
Fri 20 JunDisplayed time zone: Seoul change
10:30 - 12:10 | |||
10:30 20mTalk | Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI Research Papers Jaehwang Jung Rebellions Inc, Sunho Park KAIST, Janggun Lee KAIST, Jeho Yeon KAIST, Jeehoon Kang KAIST DOI | ||
10:50 20mTalk | Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals PLDI Research Papers DOI | ||
11:10 20mTalk | Iso: Request-Private Garbage Collection PLDI Research Papers Tianle Qiu Australian National University, Stephen M. Blackburn Google; Australian National University DOI | ||
11:30 20mTalk | CRGC: Fault-Recovering Actor Garbage Collection in Pekko PLDI Research Papers Dan Plyukhin University of Southern Denmark, Gul Agha University of Illinois at Urbana-Champaign, Fabrizio Montesi University of Southern Denmark DOI | ||
11:50 20mTalk | RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures PLDI Research Papers DOI |