Static deadlock detection for concurrent go by global session graph synthesis
Open Access
- 17 March 2016
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 174-184
- https://doi.org/10.1145/2892208.2892232
Abstract
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.Keywords
Funding Information
- Engineering and Physical Sciences Research Council (EP/K034413/1,EP/K011715/1,EP/L00058X/1)
- Seventh Framework Programme (612985)
This publication has 30 references indexed in Scilit:
- Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session TypesLecture Notes in Computer Science, 2013
- Linear type theory for asynchronous session typesJournal of Functional Programming, 2009
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- OpenMP: an industry standard API for shared-memory programmingIEEE Computational Science and Engineering, 1998
- Interpreting Message Flow GraphsFormal Aspects of Computing, 1995
- A calculus of mobile processes, IInformation and Computation, 1992
- A distributed deadlock detection algorithm for CSP-like communicationACM Transactions on Programming Languages and Systems, 1990
- Notes on Communicating Sequential SystemsPublished by Springer Science and Business Media LLC ,1986
- On Communicating Finite-State MachinesJournal of the ACM, 1983
- Communicating sequential processesCommunications of the ACM, 1978