A static verification framework for message passing in go using behavioural types
File(s)
Accepted version
Author(s)
Lange, J
Ng, CWN
Toninho, B
Yoshida, N
Type
Conference Paper
Abstract
The Go programming language has been heavily adopted in industry as a language that efficiently combines systems programming with concurrency. Go's concurrency primitives, inspired by process calculi such as CCS and CSP, feature channel-based communication and lightweight threads, providing a distinct means of structuring concurrent software. Despite its popularity, the Go programming ecosystem offers little to no support for guaranteeing the correctness of message-passing concurrent programs.
This work proposes a practical verification framework for message passing concurrency in Go by developing a robust static analysis that infers an abstract model of a program's communication behaviour in the form of a behavioural type, a powerful process calculi typing discipline. We make use of our analysis to deploy a model and termination checking based verification of the inferred behavioural type that is suitable for a range of safety and liveness properties of Go programs, providing several improvements over existing approaches. We evaluate our framework and its implementation on publicly available real-world Go code.
This work proposes a practical verification framework for message passing concurrency in Go by developing a robust static analysis that infers an abstract model of a program's communication behaviour in the form of a behavioural type, a powerful process calculi typing discipline. We make use of our analysis to deploy a model and termination checking based verification of the inferred behavioural type that is suitable for a range of safety and liveness properties of Go programs, providing several improvements over existing approaches. We evaluate our framework and its implementation on publicly available real-world Go code.
Date Issued
2018-05-27
Date Acceptance
2017-12-15
Citation
CSE '18 Proceedings of the 40th International Conference on Software Engineering, 2018, pp.1137-1148
ISBN
9781450356381
Publisher
ACM
Start Page
1137
End Page
1148
Journal / Book Title
CSE '18 Proceedings of the 40th International Conference on Software Engineering
Copyright Statement
© 2018 ACM.
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20015393
EP/K011715/1
EP/N027833/1
PO 20015391
Source
ICSE 2018
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
MODEL CHECKING
Publication Status
Published
Start Date
2018-05-27
Finish Date
2018-06-03
Coverage Spatial
Gothenburg, Sweden
Date Publish Online
2018-05-27