一句话：将解缠从 fork/join 推广到 future 并行，并证明其在状态、交互下的保持及无死锁性。
现有解缠（disentanglement）研究仅针对 fork/join 并行模型，无法直接适用于更强大的 future 并行，因为 future 使并行计算成为一等值，可被传递和存储，并与可变状态交互，产生复杂依赖甚至死锁。本文研究解缠能否推广到 future。作者考虑一个带有 future、输入/输出和可变引用（状态）的函数式语言，首先为 future 形式化解缠，并证明纯函数式程序是解缠的；随后从三个方向推广：带状态程序若数据竞争自由则解缠；竞争自由是充分但非必要条件，某些使用原子读-改-写和非确定性组合子的程序也可解缠；最后证明用 future 编写的解缠任务并行程序无死锁。这些结果表明解缠可推广到 future 并行，其收益不限于 fork/join。
Recent work has proposed a memory property for parallel programs, called disentanglement, and showed that it is pervasive in a variety of programs, written in different languages, ranging from C/C++ to Parallel ML, and showed that it can be exploited to improve the performance of parallel functional programs. All existing work on disentanglement, however, considers the “fork/join” model for parallelism and does not apply to “futures”, the more powerful approach to parallelism. This is not surprising: fork/join parallel programs exhibit a reasonably strict dependency structure (e.g., series-parallel DAGs), which disentanglement exploits. In contrast, with futures, parallel computations become first-class values of the language, and thus can be created, and passed between functions calls or stored in memory, just like other ordinary values, resulting in complex dependency structures, especially in the presence of mutable state. For example, parallel programs with futures can have deadlocks, which is impossible with fork-join parallelism. In this paper, we are interested in the theoretical question of whether disentanglement may be extended beyond fork/join parallelism, and specifically to futures. We consider a functional language with futures, Input/Output (I/O), and mutable state (references) and show that a broad range of programs written in this language are disentangled. We start by formalizing disentanglement for futures and proving that purely functional programs written in this language are disentangled. We then generalize this result in three directions. First, we consider state (effects) and prove that stateful programs are disentangled if they are race free. Second, we show that race freedom is sufficient but not a necessary condition and non-deterministic programs, e.g. those that use atomic read-modify-operations and some non-deterministic combinators, may also be disentangled. Third, we prove that disentangled task-parallel programs written with futures are free of deadlocks, which arise due to interactions between state and the rich dependencies that can be expressed with futures. Taken together, these results show that disentanglement generalizes to parallel programs with futures and, thus, the benefits of disentanglement may go well beyond fork-join parallelism.
@article{paperbot2633,
title = {Disentanglement with Futures, State, and Interaction},
author = {Jatin Arora and Stefan K. Muller and Umut A. Acar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632895}
}