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.

翻译：数据竞争是并行编程中一个臭名昭著的问题。针对静态预防数据竞争的类型系统研究已取得重要进展。尽管这些系统在安全性和可用性方面有所突破，但现有许多方法仍通过强制执行严格的反别名原则来预防数据竞争。这些方法的采用往往具有侵入性，即会破坏常见编程模式并需要范式转换。我们提出捕获分离演算（System CSC），这是一种基于捕获演算（System CC<:box）的演算系统，在保持非侵入性的同时实现了静态数据竞争自由。该系统允许一般情况下的别名化以兼容常见编程模式，但会在必要时追踪并控制别名化行为以防止数据竞争。通过建立类型安全性和数据竞争自由属性，我们研究了System CSC的形式化性质。值得注意的是，我们通过证明其归约语义的合流性确立了数据竞争自由属性。为验证该演算的可用性，我们将其实现为Scala 3编译器的扩展，并用于类型检查相关示例。