SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Tue 24 Oct 2023 11:30 - 12:00 at Room XIII - IWACO Session 1 Chair(s): Aleksander Boruch-Gruszecki

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 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
IWACO Session 1IWACO at Room XIII
Chair(s): Aleksander Boruch-Gruszecki EPFL
11:00
30m
Talk
Borrow checking Hylo
IWACO
Dimi Racordon Northeastern University, USA, Dave Abrahams Adobe
File Attached
11:30
30m
Talk
Degrees of Separation: A Flexible Type System for Data Race Prevention
IWACO
File Attached
12:00
30m
Talk
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