PoP Seminar Talk
Higher-Order Leak and Deadlock Free Locks
PhD Student at Radboud University
Wednesday, 14 June, 2023; 3:00pm
Host: Stephanie Balzer
Well-typed Rust programs are guaranteed to be memory safe and data-race free. Originally, Rust was also believed to be memory leak free, but there are well-typed programs that leak memory when using Rust’s shared memory concurrency APIs. This talk is about a step toward getting stronger guarantees by type checking: we present a linear type system for locks that guarantees leak and deadlock freedom. These locks are flexible in two ways: (1) they are first-class values that can be stored in data structures and passed around to other threads, (2) there is no restriction on the order of lock acquisition. Analogous to session types, the linear type system instead restricts the “sharing topology” to be acyclic. As an extension, we add lock orders to allow some well-behaved circular dependencies, at the cost of some restrictions on lock acquisition order. We prove in Coq that all well-typed programs are leak and deadlock free.
Jules Jacobs is a PhD student in the Software Science group at Radboud University in the Netherlands, under the supervision of Robbert Krebbers and Stephanie Balzer. He completed his undergraduate degree in mathematics and physics at Leiden University. His research focuses on the development of type systems and logics that prevent deadlocks and memory leaks in software systems.