IC Colloquium: Separation is all you need - Foundations for Modular Verification of Realistic Concurrent Programs
By: Ralf Jung - MIT
IC Faculty candidate
Abstract
Concurrent programming is essential for achieving good performance on modern processors, but it is notoriously hard to get right. In this talk, I present Iris, a new foundation for verification of concurrent programs that was developed only a few years ago but has already been built upon in over 50 follow-on publications and has been adopted as core technology by several verification projects in industry.
Iris builds on O'Hearn's seminal work on concurrent separation logic. The key idea is to exploit the fact that threads which access disjoint parts of the machine state can be verified independently of each other. However, separation logic has no clear answer for what to do with shared state, leading to the development of a plethora of extensions to separation logic which close this gap. In my work on Iris, I have shown that ``separation is all you need'': by allowing application-specific notions of ``separation'', even shared-state concurrent programs can be seen as upholding a separation discipline.
As one example for applying Iris to a challenging real-world problem, I will present RustBelt, a proof of type safety for the up-and-coming systems programming language Rust.
Bio
Ralf Jung is a post-doctoral researcher in the PDOS group at MIT CSAIL working on formal verification of concurrent and distributed software, operational semantics, and type systems. He completed his PhD in 2020 at MPI-SWS and Saarland University under the supervision of Derek Dreyer. His thesis has received numerous international awards: an Honorable Mention for the ACM Doctoral Dissertation Award, an ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award, and the ETAPS Doctoral Dissertation Award.
More information
IC Faculty candidate
Abstract
Concurrent programming is essential for achieving good performance on modern processors, but it is notoriously hard to get right. In this talk, I present Iris, a new foundation for verification of concurrent programs that was developed only a few years ago but has already been built upon in over 50 follow-on publications and has been adopted as core technology by several verification projects in industry.
Iris builds on O'Hearn's seminal work on concurrent separation logic. The key idea is to exploit the fact that threads which access disjoint parts of the machine state can be verified independently of each other. However, separation logic has no clear answer for what to do with shared state, leading to the development of a plethora of extensions to separation logic which close this gap. In my work on Iris, I have shown that ``separation is all you need'': by allowing application-specific notions of ``separation'', even shared-state concurrent programs can be seen as upholding a separation discipline.
As one example for applying Iris to a challenging real-world problem, I will present RustBelt, a proof of type safety for the up-and-coming systems programming language Rust.
Bio
Ralf Jung is a post-doctoral researcher in the PDOS group at MIT CSAIL working on formal verification of concurrent and distributed software, operational semantics, and type systems. He completed his PhD in 2020 at MPI-SWS and Saarland University under the supervision of Derek Dreyer. His thesis has received numerous international awards: an Honorable Mention for the ACM Doctoral Dissertation Award, an ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award, and the ETAPS Doctoral Dissertation Award.
More information
Practical information
- General public
- Free
Contact
- Host: Martin Odersky