Wed 18 Jan 2023 10:45 - 11:10 at Avenue34 - Types I Chair(s): Neel Krishnaswami

Reasoning about concurrent programs is challenging, especially if data is shared among threads.
Program correctness can be violated by the presence of data races—whose prevention has been a topic of concern
both in research and in practice.
The Rust programming language is a prime example, putting the slogan fearless concurrency in practice
by not only employing an ownership-based type system for memory management,
but also using its type system to enforce mutual exclusion on shared data.
Locking, unfortunately, not only comes at the price of \emph{deadlocks} but shared access to data may also cause memory \emph{leaks}.

This paper develops a theory of deadlock and leak freedom for \emph{higher-order locks} in a shared memory concurrent setting.
Higher-order locks allow sharing not only of basic values but also of other locks and channels, and are themselves first-class citizens.
The theory is based on the notion of a \emph{sharing topology}, administrating who is permitted to access shared data at what point in the program.
The paper first develops higher-order locks for \emph{acyclic} sharing topologies,
instantiated in a $\lambda$-calculus with higher-order locks and message-passing concurrency.
The paper then extends the calculus to support \emph{circular} dependencies with \emph{dynamic} lock orders,
which we illustrate with a dynamic version of Dijkstra's dining philosophers problem.
Well-typed programs in the resulting calculi are shown to be free of deadlocks and memory leaks,
with proofs mechanized in the Coq proof assistant.

Wed 18 Jan

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

10:45 - 12:00
Types IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
Higher-Order Leak and Deadlock Free LocksDistinguished Paper
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
Taro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP
Recursive Subtyping for All
Litao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong