Fencing off go: liveness and safety for channel-based programming
Open Access
- 1 January 2017
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 748-761
- https://doi.org/10.1145/3009837.3009847
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 mismatches or partial deadlocks. This work develops a static verification framework for bounded 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 and infinite 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 bounded verification procedures (akin to bounded model checking) to check for liveness and safety in types which in turn approximates liveness and safety in Go programs. We have implemented a type inference and liveness and safety checks in a tool-chain and tested it against publicly available Go programs. Updated on 27th Feb 2017. See Comments.Keywords
Funding Information
- Engineering and Physical Sciences Research Council (EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1)
- Seventh Framework Programme (612985)
This publication has 33 references indexed in Scilit:
- A hybrid type system for lock-freedom of mobile processesACM Transactions on Programming Languages and Systems, 2008
- Asynchronous Session Types and Progress for Object Oriented LanguagesLecture Notes in Computer Science, 2007
- Resource Usage Analysis for the Pi-CalculusLogical Methods in Computer Science, 2006
- Type-based information flow analysis for the π-calculusActa Informatica, 2005
- A generic type system for the Pi-calculusTheoretical Computer Science, 2004
- Comparing Recursion, Replication, and Iteration in Process CalculiLecture Notes in Computer Science, 2004
- Replication vs. Recursive Definitions in Channel Based CalculiLecture Notes in Computer Science, 2003
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- Notes on Communicating Sequential SystemsPublished by Springer Science and Business Media LLC ,1986
- On Communicating Finite-State MachinesJournal of the ACM, 1983