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

We introduce the notion of a \emph{connectivity graph}—an abstract representation of the topology of concurrently interacting entities, which allows us to encapsulate generic principles of reasoning about deadlock freedom. Connectivity graphs are \emph{parametric} in their vertices (which represent entities like threads and channels) and their edges (which represent references between entities) with labels (which represent interaction protocols). To prove deadlock and memory leak freedom in the style of progress and preservation, we distill generic \emph{separation logic rules} for local graph transformations that preserve acyclicity of the connectivity graph, and a \emph{waiting induction} principle for acyclic connectivity graphs, to reason about global progress locally. We mechanize our results in Coq, and instantiate our method with a higher-order binary session-typed language to obtain the first mechanized proof of deadlock and leak freedom.

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