Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Cogumbreiro:2019:10.1145/3229060,
author = {Cogumbreiro, T and Hu, R and Martins, F and Yoshida, N},
doi = {10.1145/3229060},
journal = {ACM Transactions on Programming Languages and Systems},
pages = {1--38},
title = {Dynamic deadlock verification for general barrier synchronisation},
url = {http://dx.doi.org/10.1145/3229060},
volume = {41},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - We present Armus, a verification tool for dynamically detecting or avoiding barrier deadlocks. The core designof 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. Our base graph representation can also 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 theruntime 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 below1. 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 dynamicselection, 2.6× for SG-static selection, and 5.9× for WFG-static selection.
AU  - Cogumbreiro,T
AU  - Hu,R
AU  - Martins,F
AU  - Yoshida,N
DO  - 10.1145/3229060
EP  - 38
PY  - 2019///
SN  - 0164-0925
SP  - 1
TI  - Dynamic deadlock verification for general barrier synchronisation
T2  - ACM Transactions on Programming Languages and Systems
UR  - http://dx.doi.org/10.1145/3229060
UR  - http://hdl.handle.net/10044/1/60269
VL  - 41
ER  -
Download