LFCS Seminar: Friday, 17 February - Jules Jacobs

Speaker:   Jules Jacobs

Title:          Higher-Order Leak and Deadlock Free Locks

Abstract:

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, and prove in Coq that all well-typed programs are leak and deadlock free.