A flexible type system for fearless concurrency
A flexible type system for fearless concurrency
复制标题
灵活的类型系统，可实现无所畏惧的并发
DOI：
10.1145/3519939.3523443
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Myers, Andrew C.
中科院分区：
文献类型：
--
作者：
Milano, Mae;Turcotti, Joshua;Myers, Andrew C.
本文提出了一种新的并发程序类型系统，允许线程交换复杂对象图 而不冒破坏性数据竞赛的风险。虽然这一目标是 由于过去工作的丰富历史，现有的解决方案要么依赖于严格执行的堆不变量， 自然的编程模式，或者甚至对于简单的编程任务也需要普遍的注释。因此，过去 系统不能在没有不自然的重写或大量注释负担的情况下直观地表达简单的代码。我们的工作 通过一个新颖的类型系统避免了这些陷阱，该类型系统提供了关于堆中分离的合理推理， 保持足够的灵活性以支持广泛的期望堆操作。这个新的最佳点是 通过类似于先验的强制堆支配不变量， 工作，但通过允许复杂的异常， 添加很少的注释负担。我们的结果包括：（1）代码 这些例子显示了在现有技术中难以或不可能表达的常见数据结构操作， 工作是自然的和直接的，（2）形式证明 正确性证明了良好类型的程序在运行时不会遇到破坏性的数据竞争，以及（3） 在Gallina和OCaml中实现的高效类型检查器。
This paper proposes a new type system for concurrent programs, allowing threads to exchange complex object graphs without risking destructive data races. While this goal is shared by a rich history of past work, existing solutions either rely on strictly enforced heap invariants that prohibit natural programming patterns or demand pervasive annotations even for simple programming tasks. As a result, past systems cannot express intuitively simple code without unnatural rewrites or substantial annotation burdens. Our work avoids these pitfalls through a novel type system that provides sound reasoning about separation in the heap while remaining flexible enough to support a wide range of desirable heap manipulations. This new sweet spot is attained by enforcing a heap domination invariant similarly to prior work, but tempering it by allowing complex exceptions that add little annotation burden. Our results include: (1) code examples showing that common data structure manipulations which are difficult or impossible to express in prior work are natural and direct in our system, (2) a formal proof of correctness demonstrating that well-typed programs cannot encounter destructive data races at run time, and (3) an efficient type checker implemented in Gallina and OCaml.
登录
查看更多内容
DOI：
--
发表时间：
2016
期刊：
European Conference on Object-Oriented Programming
影响因子：
--
作者：
Elias Castegren;Tobias Wrigstad
通讯作者：
Tobias Wrigstad
赛车安全宇宙
DOI：
--
发表时间：
2007
期刊：
影响因子：
--
作者：
D. Cunningham;S. Eisenbach;S. Drossopoulou
通讯作者：
S. Drossopoulou
DOI：
--
发表时间：
2015
期刊：
--
影响因子：
--
作者：
Eric C. Reed
通讯作者：
Eric C. Reed
能力演算中的类型化内存管理
DOI：
--
发表时间：
1999
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Karl Crary;D. Walker;G. Morrisett
通讯作者：
G. Morrisett
会话类型的基础知识
影响因子：
1
作者：
V. Vasconcelos
通讯作者：
V. Vasconcelos