Deadlock-Free Separation Logic
Event details
| Date | 06.02.2024 |
| Hour | 12:00 › 13:00 |
| Speaker | Jules Jacobs, Cornell University |
| Location | |
| Category | Conferences - Seminars |
| Event Language | English |
Subtitle: Linearity yields progress for dependent higher-order message passing
Joint work with Jonas Kastberg Hinrichsen and Robbert Krebbers
Abstract: We introduce a new concurrent separation logic for message passing programs with mutable state. The key feature of this logic is that it not only guarantees safety, but also deadlock freedom, and does so “for free” by being linear, without requiring any additional proof effort specific to deadlock freedom. The soundness of the logic is proved via a step-indexed model in Coq. As a demonstration, we show that all programs that can be proven to be deadlock free using linear session types, can also be proven deadlock free with our logic.
Speaker bio: Jules Jacobs is a postdoctoral researcher at Cornell University, working with Nate Foster and Alexandra Silva. He did his PhD at Radboud University, under the supervision of Robbert Krebbers and Stephanie Balzer, where he worked primarily on type systems and separation logics for concurrent programming languages.
Joint work with Jonas Kastberg Hinrichsen and Robbert Krebbers
Abstract: We introduce a new concurrent separation logic for message passing programs with mutable state. The key feature of this logic is that it not only guarantees safety, but also deadlock freedom, and does so “for free” by being linear, without requiring any additional proof effort specific to deadlock freedom. The soundness of the logic is proved via a step-indexed model in Coq. As a demonstration, we show that all programs that can be proven to be deadlock free using linear session types, can also be proven deadlock free with our logic.
Speaker bio: Jules Jacobs is a postdoctoral researcher at Cornell University, working with Nate Foster and Alexandra Silva. He did his PhD at Radboud University, under the supervision of Robbert Krebbers and Stephanie Balzer, where he worked primarily on type systems and separation logics for concurrent programming languages.
Practical information
- Informed public
- Free
Organizer
- Prof. Nate Foster
Visiting Professor, EPFL, DCSL Lab
Professor, Cornell University, Computer Science
Contact
- Nate Foster, [email protected]