Imperial College London

ProfessorNobukoYoshida

Faculty of EngineeringDepartment of Computing

Academic Visitor
 
 
 
//

Contact

 

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

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Ng:2016:10.1145/2892208.2892232,
author = {Ng, N and Yoshida, N},
doi = {10.1145/2892208.2892232},
pages = {174--184},
publisher = {ACM},
title = {Static deadlock detection for concurrent go by global session graph synthesis},
url = {http://dx.doi.org/10.1145/2892208.2892232},
year = {2016}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - Go is a programming language developed at Google, with channel-based concurrent features based on CSP. Go can detect global communication deadlocks at runtime when all threads of execution are blocked, but deadlocks in other paths of execution could be undetected. We present a new static analyser for concurrent Go code to find potential communication errors such as communication mismatch and deadlocks at compile time. Our tool extracts the communication operations as session types, which are then converted into Communicating Finite State Machines (CFSMs). Finally, we apply a recent theoretical result on choreography synthesis to generate a global graph representing the overall communication pattern of a concurrent program. If the synthesis is successful, then the program is free from communication errors. We have implemented the technique in a tool, and applied it to analyse common Go concurrency patterns and an open source application with over 700 lines of code.
AU - Ng,N
AU - Yoshida,N
DO - 10.1145/2892208.2892232
EP - 184
PB - ACM
PY - 2016///
SP - 174
TI - Static deadlock detection for concurrent go by global session graph synthesis
UR - http://dx.doi.org/10.1145/2892208.2892232
UR - http://hdl.handle.net/10044/1/34139
ER -