Wed 19 Jan 2022 15:05 - 15:30 at Salon III - Concurrency and Parallelism Chair(s): Andrew C. Myers

Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is in contrast to the customary approach based on exhibiting the algorithm’s linearization points. In this paper we apply visibility relations to develop modular proofs for three elegant concurrent snapshot algorithms of Jayanti. The proofs are divided into components of increasing level of abstraction, using type-theoretic notions of signatures and functors (i.e., dependent $\Sigma$ and $\Pi$ types) as interfaces. The proofs are modular because the components at higher abstraction levels are shared, i.e., they apply to all three algorithms simultaneously. Importantly, the interface properties mathematically capture Jayanti’s original intuitions that have previously been given only informally.

Wed 19 Jan

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

15:05 - 16:20
Concurrency and ParallelismPOPL at Salon III
Chair(s): Andrew C. Myers Cornell University
15:05
25m
Research paper
Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote
POPL
Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute
DOI Media Attached
15:30
25m
Research paper
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen
DOI Media Attached
15:55
25m
Research paper
Static Prediction of Parallel Computation GraphsInPerson
POPL
Stefan K. Muller Illinois Institute of Technology
DOI Media Attached