Fencing off go: liveness and safety for channel-based programming
File(s)cameraready-fixed.pdf (493.28 KB)
Accepted version
Author(s)
Lange, J
Ng, C
Parente Coutinho Fernandes Toninho, B
Yoshida, N
Type
Conference Paper
Abstract
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mis-matches or partial deadlocks. This work develops a static verification framework for liveness and safety in Go programs, able to detect communication errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation, unbounded thread creation and recursion. Our approach infers from a Go program a faithful representation of its communication patterns as a behavioural type. By checking a syntactic restriction on channel usage, dubbed fencing, we ensure that programs are made up of finitely many different communication patterns that may be repeated infinitely many times. This restriction allows us to implement a decision procedure for liveness and safety in types which in turn statically ensures liveness and safety in Go programs. We have implemented a type inference and decision procedures in a tool-chain and tested it against publicly available Go programs.
Date Issued
2017-01-01
Date Acceptance
2016-12-20
Citation
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017, pp.748-761
ISBN
978-1-4503-4660-3
Publisher
ACM
Start Page
748
End Page
761
Journal / Book Title
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
Copyright Statement
© 2017 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in POPL 2017 (2017) http://doi.acm.org/10.1145/3009837.3009847
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Grant Number
ERI 025567 (EP/K034413/1)
EP/N027833/1
PO 20131167
EP/L00058X/1, PO 20131167
EP/K011715/1
612985
Source
POPL 2017
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Channel-based programming
Message-passing programming
Process calculus
Types
Safety and Liveness
Compiletime (static) deadlock detection
SESSION TYPES
PROGRESS
SYSTEM
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Channel-based programming
Message-passing programming
Process calculus
Types
Safety and Liveness
Compiletime (static) deadlock detection
SESSION TYPES
PI-CALCULUS
PROGRESS
LANGUAGES
SYSTEM
Software Engineering
Publication Status
Published
Start Date
2017-01-15
Finish Date
2017-01-21
Coverage Spatial
Paris, France