Imperial College London
Mr Lloyd Kamara

MrLloydKamara

Faculty of Engineering, Department of Computing

Computing Support Manager
 
 
 
//

Contact

 

+44 (0)20 7594 8400l.kamara Website

 
 
//

Location

 

305Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@techreport{Cogumbreiro:2014:10.25561/95041,
author = {Cogumbreiro, T and Hu, R and Martins, F and Yoshida, N},
booktitle = {Departmental Technical Report: 14/12},
doi = {10.25561/95041},
publisher = {Department of Computing, Imperial College London},
title = {Dynamic deadlock verification for general barrier synchronisation},
url = {http://dx.doi.org/10.25561/95041},
year = {2014}
}
Download

RIS format (EndNote, RefMan)

TY  - RPRT
AB  - We present Armus, a dynamic verification tool for deadlock detectionand avoidance specialised in barrier synchronisation. Barriersare used to coordinate the execution of groups of tasks, and serve asa building block of parallel computing. Our tool verifies more barriersynchronisation patterns than current state-of-the-art. To improvethe scalability of verification, we introduce a novel eventbasedrepresentation of concurrency constraints, and a graph-basedtechnique for deadlock analysis. The implementation is distributedand fault-tolerant, and can verify X10 and Java programs.To formalise the notion of barrier deadlock, we introduce a corelanguage expressive enough to represent the three most widespreadbarrier synchronisation patterns: group, split-phase, and dynamicmembership. We propose a graph analysis technique that selectsfrom two alternative graph representations: the Wait-For Graph,that favours programs with more tasks than barriers; and the StateGraph, optimised for programs with more barriers than tasks. Weprove that finding a deadlock in either representation is equivalent,and that the verification algorithm is sound and complete withrespect to the notion of deadlock in our core language.Armus is evaluated with three benchmark suites in local anddistributed scenarios. The benchmarks show that graph analysiswith automatic graph-representation selection can record a 7-foldexecution increase versus the traditional fixed graph representation.The performance measurements for distributed deadlock detectionbetween 64 processes show negligible overheads.
AU  - Cogumbreiro,T
AU  - Hu,R
AU  - Martins,F
AU  - Yoshida,N
DO  - 10.25561/95041
PB  - Department of Computing, Imperial College London
PY  - 2014///
TI  - Dynamic deadlock verification for general barrier synchronisation
T1  - Departmental Technical Report: 14/12
UR  - http://dx.doi.org/10.25561/95041
UR  - http://hdl.handle.net/10044/1/95041
ER  -
Download