POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Thu 23 Jan 2025 16:00 - 16:20 at Peek-A-Boo - Concurrency

State-of-the-art model checkers employing dynamic partial order reduction (DPOR) can verify concurrent programs under a wide range of memory models such as sequential consistency (SC), total store order (TSO), release-acquire (RA), and the repaired C11 memory model (RC11) in an optimal and memory-efficient fashion. Unfortunately, these DPOR techniques cannot be applied in an optimal fashion to programs with mixed-sized accesses (MSA), where atomic instructions access different (sets of) bytes belonging to the same word. Such patterns naturally arise in real life code with C/C++ union types, and are even used in a concurrent setting. In this paper, we introduce Mixer, an optimal DPOR algorithm for MSA programs that allows (multi-byte) reads to be revisited by multiple writes together. We have implemented Mixer in the GenMC model checker, enabling (for the first time) the automatic verification of C/C++ code with mixed-size accesses. Our results also extend to the more general case of transactional programs provided that the set of read accesses performed by a transaction can be dynamically overapproximated at the beginning of the transaction.

This program is tentative and subject to change.

Thu 23 Jan

Displayed time zone: Mountain Time (US & Canada) change

15:00 - 16:20
ConcurrencyPOPL at Peek-A-Boo
15:00
20m
Talk
Data Race Freedom à la Mode
POPL
Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Benjamin Peters MPI-SWS, Laila Elbeheiry MPI-SWS, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street, François Pottier Inria, Derek Dreyer MPI-SWS
15:20
20m
Talk
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
POPL
15:40
20m
Talk
Relaxed Memory Concurrency Re-executed
POPL
Evgenii Moiseenko JetBrains Research, Matteo Meluzzi TU Delft, the Netherlands, Innokentii Meleshchenko JetBrains Research, Neapolis University Pafos, Cyprus, Ivan Kabashnyi JetBrains Research, Constructor University Bremen, Germany, Anton Podkopaev JetBrains Research, Constructor University, Soham Chakraborty TU Delft
16:00
20m
Talk
Model Checking C/C++ with Mixed-Size Accesses
POPL