PoP Seminar Talk

Types for Verifying Concurrent Programs

Stephanie Balzer, Assistant Research Professor in the Principles of Programming Group of the Computer Science Department
Tuesday, 26 September, 2023; 3:00pm
GHC 8102
Host: N/A

Abstract

Today’s application landscape is typically concurrent, making concurrent programming a necessity. Writing correct concurrent code is — as we all know — notoriously difficult. My research is concerned with the development of rigorous reasoning techniques, such as type systems, proof methods, and verification logics, to enable the construction of provably correct and safe concurrent software.

In this talk, I focus on my work on developing type systems for concurrent programming based on linear logic. I first introduce a type system for message-passing concurrency where types prescribe communication protocols and type checking ensures that well-typed programs adhere to these protocols [1-3]. The resulting type system is implemented as an EDSL in Rust [4-5], taking advantage of Rust’ ownership type system. Then I introduce a Rust-like type system for shared memory concurrency with higher-order locks [1], allowing locks to be passed as values and stored in other locks. Type-checking ensures that well-typed programs are free of memory leaks and deadlocks. These correctness guarantees have been verified in the Coq proof assistant [6-8]. I conclude my talk with an overview of ongoing work and future research directions.

References:

[1] https://dl.acm.org/doi/10.1145/3110281 [2] https://drops.dagstuhl.de/opus/volltexte/2018/9568/ [3] https://link.springer.com/chapter/10.1007/978-3-030-17184-1_22 [4] https://drops.dagstuhl.de/opus/volltexte/2022/16250/ [5] https://github.com/ferrite-rs/ferrite [6] https://dl.acm.org/doi/10.1145/3571229 [7] https://dl.acm.org/doi/10.1145/3498662 [8] https://dl.acm.org/doi/10.1145/3547638

Bio

Stephanie Balzer is an Assistant Research Professor in the Principles of Programming group in the Computer Science Department of Carnegie Mellon University. She obtained her PhD from ETH Zurich. The goal of her research is to enable the construction of failure-free software, software that is correct by construction and secure to run