一句话：提出 Armus：基于 phaser 的事件图模型，为 X10 与 Java 实现可靠完备的动态屏障死锁检测与避免。
论文针对现代语言与库中通用屏障同步（如 X10 phaser：分相同步、动态成员、可选等待）的死锁问题，提出验证工具 Armus。其核心是一个新的事件图模型，刻画屏障并发约束，并区分任务-事件与事件-任务两类依赖；这种解耦使得对带动态成员的分布式屏障（X10 的难点特性）也能进行验证。该图表示可在任务级 Wait-for Graph（WFG）与事件级 State Graph（SG）之间动态切换，以提升可扩展性。作者在核心 phaser 语言上形式化证明了验证相对于死锁发生的可靠性与完备性，并证明图表示切换保持这两个性质，相关结论已在 Coq 证明助手中机器验证。作者为 X10 和 Java 实现了 Armus，并在三组基准上于本地与分布式场景测量运行时开销：检测方面分布式开销可忽略、本地低于 1.15×；避免方面开销更高，动态选择图表示优势明显，某基准中为 1.8×，而 SG 静态选择为 2.6×、WFG 静态选择为 5.9×。
We present Armus, a verification tool for dynamically detecting or avoiding barrier deadlocks. The core design of Armus is based on phasers, a generalisation of barriers that supports split-phase synchronisation, dynamic membership, and optional-waits. This allows Armus to handle the key barrier synchronisation patterns found in modern languages and libraries. We implement Armus for X10 and Java, giving the first sound and complete barrier deadlock verification tools in these settings. Armus introduces a novel event-based graph model of barrier concurrency constraints that distinguishes task-event and event-task dependencies. Decoupling these two kinds of dependencies facilitates the verification of distributed barriers with dynamic membership, a challenging feature of X10. Further, our base graph representation can be dynamically switched between a task-to-task model, Wait-for Graph (WFG), and an event-to-event model, State Graph (SG), to improve the scalability of the analysis. Formally, we show that the verification is sound and complete with respect to the occurrence of deadlock in our core phaser language, and that switching graph representations preserves the soundness and completeness properties. These results are machine checked with the Coq proof assistant. Practically, we evaluate the runtime overhead of our implementations using three benchmark suites in local and distributed scenarios. Regarding deadlock detection, distributed scenarios show negligible overheads and local scenarios show overheads below 1.15×. Deadlock avoidance is more demanding, and highlights the potential gains from dynamic graph selection. In one benchmark scenario, the runtime overheads vary from 1.8× for dynamic selection, 2.6× for SG-static selection, and 5.9× for WFG-static selection.
@article{paperbot309,
title = {Dynamic Deadlock Verification for General Barrier Synchronisation},
author = {Tiago Cogumbreiro and Raymond Hu and Francisco Martins and Nobuko Yoshida},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {1},
year = {2018},
doi = {10.1145/3229060}
}