分离度：一个灵活的类型系统用于数据竞争预防
摘要：静态防止数据竞争的类型系统中存在许多强制执行严格反别名原则以防止数据竞争的方法，这常常是具有侵入性的，因为它使常见的编程模式无效并需要范式转变。我们提出了一个基于捕获计算的捕获分离演算（System CSC），它在不具有侵入性的同时实现了静态数据竞争自由。它允许一般别名以允许常见的编程模式，但在必要时跟踪别名并对其进行控制以防止数据竞争。我们通过建立其类型安全性和数据竞争自由性来研究System CSC的形式属性。值得注意的是，通过证明其减少语义的合流性，我们建立了数据竞争自由性属性。为了验证演算的可用性，我们将其作为Scala 3编译器的扩展实现，并使用它来对示例进行类型检查。
作者：Yichen Xu and Martin Odersky
论文ID：2308.07474
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-16