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.

翻译：数据竞争是并行编程中一个众所周知的问题。针对静态预防数据竞争的类型系统，已有大量研究兴趣。尽管这些系统在安全性和可用性方面取得了进展，但许多现有方法为了预防数据竞争而强制执行严格的反别名原则。它们的引入往往具有侵入性，即会失效常见编程模式并要求范式转变。我们提出了捕获分离演算（System CSC），这是一种基于捕获演算（System CC<:box）的演算，能够在非侵入性的前提下实现静态数据竞争自由。它允许一般情况下的别名以兼容常见编程模式，但会追踪别名并在必要时加以控制以预防数据竞争。我们通过建立System CSC的类型安全性和数据竞争自由性质来研究其形式化属性。值得注意的是，我们通过证明其约简语义的合流性建立了数据竞争自由属性。为验证该演算的可用性，我们将其作为Scala 3编译器的扩展实现，并用于类型检查论文中的示例。