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

This program is tentative and subject to change.

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

We present DRFCaml, an extension of OCaml’s type system that guarantees data race freedom for multi-threaded OCaml programs while retaining backward compatibility with existing sequential OCaml code. We build on recent work of Lorenzen et al., who extend OCaml with \emph{modes} that keep track of locality, uniqueness, and affinity. We introduce two new mode axes, \emph{contention} and \emph{portability}, which record whether data has been shared or can be shared between multiple threads. Although this basic type-and-mode system has limited expressive power by itself, it does let us express APIs for \emph{capsules}, regions of memory whose access is controlled by a unique ghost key, and \emph{reader-writer locks}, which allow a thread to safely acquire partial or full ownership of a key. We show that this allows complex data structures (which may involve aliasing and mutable state) to be safely shared between threads. We formalize the complete system and establish its soundness by building a semantic model of it in the Iris program logic on top of the Coq proof assistant.

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