Degrees of Separation: A Flexible Type System for Data Race Prevention

TL;DR

This paper introduces System CSC, a flexible type system for data race prevention in parallel programming that allows aliasing and is less intrusive than existing approaches, ensuring safety through formal proofs and practical implementation.

Contribution

It presents a novel type calculus that balances data race prevention with programming flexibility, validated by formal proofs and a Scala 3 compiler extension.

Findings

System CSC guarantees data race freedom through confluence of reduction semantics.

The calculus is formally proven to be type safe and data race free.

Implementation in Scala 3 demonstrates practical usability.

Abstract

Data races are 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 in the paper.