PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Fri 20 Jun 2025 10:30 - 10:50 at Cosmos, Violet & Tulip - Memory Management

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 Jun

Displayed time zone: Seoul change

10:30 - 12:10
10:30
20m
Talk
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
20m
Talk
Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
PLDI Research Papers
DOI
11:10
20m
Talk
Iso: Request-Private Garbage Collection
PLDI Research Papers
Tianle Qiu Australian National University, Stephen M. Blackburn Google; Australian National University
DOI
11:30
20m
Talk
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
20m
Talk
RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures
PLDI Research Papers
Md Amit Hasan Arovi Pennsylvania State University, Ruslan Nikolaev Pennsylvania State University
DOI