一句话：提出 System CSC：默认允许别名但在类型中追踪，按需控制别名以静态防止数据竞争。
数据竞争是并发编程中的长期难题，现有静态防竞争类型系统虽日益实用，却因严格禁止别名而难以兼容既有编程模式，阻碍主流采用。本文提出 Capture Separation Calculus（System CSC），用于建模 fork-join 并行，并遵循“按需控制”哲学：默认允许别名，但在类型系统中追踪它们；当存在数据竞争风险时，再通过类型规则控制别名，防止易导致竞争的模式。作者研究 System CSC 的形式性质：用标准 progress 与 preservation 定理证明类型健全性，并通过证明良类型程序的归约具有合流性，形式化验证其数据竞争自由性。评估以形式化证明为主，表明该设计在保持安全性的同时提升了对现有编程模式的兼容性。
Data races have long been a notorious problem in concurrent programming. They are hard to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress has been made in this area, and these type systems are increasingly usable and practical. However, their adoption in mainstream programming languages is still limited, which is largely attributed to their strict alias prevention principles that obstruct the usage of existing programming patterns. This is a deterrent to the migration of existing code bases. To tackle this problem, we propose Capture Separation Calculus (System CSC), a calculus that models fork-join parallelism and statically prevents data races while being compatible with established programming patterns. It follows a control-as-you-need philosophy: by default, aliases are allowed, but they are tracked in the type system. When data races are a concern, the tracked aliases are controlled to prevent data-race-prone patterns. We study the formal properties of System CSC. Type soundness is proven via the standard progress and preservation theorems. Additionally, we formally verify the data race freedom property of System CSC by proving that the reduction of a well-typed program is confluent.
@article{paperbot2554,
title = {Degrees of Separation: A Flexible Type System for Safe Concurrency},
author = {Yichen Xu and Aleksander Boruch-Gruszecki and Martin Odersky},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649853}
}