Fri 20 Jan 2023 15:10 - 15:35 at Avenue34 - Concurrency & Linearizability Chair(s): Tej Chajed

Concurrent data structures and synchronization mechanisms implemented by expert developers are indispensable for modular software development. In this paper, we address the fundamental problem of library abstraction under weak memory concurrency, and identify a general library correctness condition allowing clients of the library to reason about program behaviors using the specification code, which is often much simpler than the concrete implementation. We target (a fragment of) the RC11 memory model, and develop an equivalent operational presentation that exposes knowledge propagation between threads, and is sufficiently expressive to capture library behaviors as totally ordered operational execution traces. We further introduce novel access modes to the language that allow intricate specifications accounting for library internal synchronization that is not exposed to the client, as well as the library's demands on external synchronization by the client. We illustrate applications of our approach in several examples of different natures.

Fri 20 Jan

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

15:10 - 16:25
Concurrency & LinearizabilityPOPL at Avenue34
Chair(s): Tej Chajed VMware Research
15:10
25m
Talk
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
POPL
Abhishek Kr Singh Tel Aviv University, Ori Lahav Tel Aviv University
DOI
15:35
25m
Talk
The Path to Durable Linearizability
POPL
Emanuele D’Osualdo MPI-SWS, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
DOI
16:00
25m
Talk
A Compositional Theory of Linearizability
POPL
Arthur Oliveira Vale Yale University, Zhong Shao Yale University, Yixuan Chen Yale University
DOI