Deadlock avoidance in parallel programs with futures: why parallel tasks should not wait for strangers
Deadlock avoidance in parallel programs with futures: why parallel tasks should not wait for strangers
复制标题
带有 future 的并行程序中的死锁避免：为什么并行任务不应该等待陌生人
DOI：
10.1145/3143359
复制
发表时间：
2017
影响因子：
--
通讯作者：
M. Grossman
中科院分区：
文献类型：
--
作者：
Tiago Cogumbreiro;R. Surendran;F. Martins;Vivek Sarkar;V. Vasconcelos;M. Grossman
在函数式程序中， futures（期货/未来对象，一种异步编程概念）是一种表达并行性的巧妙方法。然而，在像C++或Java这样的命令式编程中结合futures，由于通过可变共享内存的不受控制的数据流，可能会导致以数据竞争和死锁形式出现的严重错误。在本文中，我们为带有futures的并行程序引入了已知连接（KJ）属性，并将其与死锁自由（DF）和数据竞争自由（DRF）属性相关联。我们的论文提供了两个关键的理论结果：1）DRF蕴含KJ，2）KJ蕴含DF。这些结果表明，在仅操作非同步共享变量的带有futures的程序中，数据竞争自由足以保证死锁自由。据我们所知，这些是首次为带有futures的命令式并行程序建立死锁自由的充分条件，并描述可能引发死锁的数据竞争子集（那些违反KJ属性的数据竞争）的理论结果。根据结果2），我们开发了一种工具，当KJ成立时，即在对futures的引用之间没有数据竞争时，该工具能在线性时间和空间内避免死锁。当KJ不成立时，该工具报告数据竞争，并可选择回退到通过循环检测的标准死锁避免算法。我们的工具验证了约2300个学生作业解决方案的数据集，并发现了一个死锁程序。从我们的工具获得的性能结果非常令人鼓舞：在16核机器上最大减速为1.06倍，总是优于通过循环检测的死锁避免方法。两个主要结果的证明使用Coq证明助手进行了形式化。
Futures are an elegant approach to expressing parallelism in functional programs. However, combining futures with imperative programming (as in C++ or in Java) can lead to pernicious bugs in the form of data races and deadlocks, as a consequence of uncontrolled data flow through mutable shared memory. In this paper we introduce the Known Joins (KJ) property for parallel programs with futures, and relate it to the Deadlock Freedom (DF) and the Data-Race Freedom (DRF) properties. Our paper offers two key theoretical results: 1) DRF implies KJ, and 2) KJ implies DF. These results show that data-race freedom is sufficient to guarantee deadlock freedom in programs with futures that only manipulate unsynchronized shared variables. To the best of our knowledge, these are the first theoretical results to establish sufficient conditions for deadlock freedom in imperative parallel programs with futures, and to characterize the subset of data races that can trigger deadlocks (those that violate the KJ property). From result 2), we developed a tool that avoids deadlocks in linear time and space when KJ holds, i.e., when there are no data races among references to futures. When KJ fails, the tool reports the data race and optionally falls back to a standard deadlock avoidance algorithm by cycle detection. Our tool verified a dataset of ∼2,300 student’s homework solutions and found one deadlocked program. The performance results obtained from our tool are very encouraging: a maximum slowdown of 1.06× on a 16-core machine, always outperforming deadlock avoidance via cycle-detection. Proofs of the two main results were formalized using the Coq proof assistant.
参数化图的代数
影响因子：
2
作者：
Mokhov A
通讯作者：
Mokhov A