Degrees of Separation: A Flexible Type System for Data Race Prevention
Data race is a notorious problem in parallel programming. There has been great research interest in type systems that statically prevent data races. Despite the progress in the safety and usability of these systems, lots of existing approaches enforce strict anti-aliasing principles to prevent data races. The adoption of them is often intrusive, in the sense that it invalidates common programming patterns and requires paradigm shifts. We propose Capture Separation Calculus (System CSC), a calculus based on Capture Calculus (System CC<:box), that achieves static data race freedom while being non-intrusive. It allows aliasing in general to permit common programming patterns, but tracks aliasing and controls them when that is necessary to prevent data races. We study the formal properties of System CSC by establishing its type safety and data race freedom. Notably, we establish the data race freedom property by proving the confluence of its reduction semantics. To validate the usability of the calculus, we implement it as an extension to the Scala 3 compiler, and use it to type-check the examples.
(paper.pdf) | 847KiB |
Tue 24 OctDisplayed time zone: Lisbon change
11:00 - 12:30 | |||
11:00 30mTalk | Borrow checking Hylo IWACO File Attached | ||
11:30 30mTalk | Degrees of Separation: A Flexible Type System for Data Race Prevention IWACO File Attached | ||
12:00 30mTalk | Latte: Lightweight Aliasing Tracking for Java IWACO Conrad Zimmerman Brown University, Catarina Gamboa Carnegie Mellon University and LASIGE, University of Lisbon, Alcides Fonseca LASIGE, University of Lisbon, Jonathan Aldrich Carnegie Mellon University Pre-print |