π-calculus, Session Types research at Imperial College
Nick gave a talk on Static Deadlock Detection for Go at Golang UK. Details and slides of the talk can be found on the talks page.
Abstract
Go’s concurrency features differ from mainstream programming languages in that they are based on the high-level and formal model of CSP (or process calculi) by Tony Hoare in 1978. Over the years, a large body of research work was developed for understanding concurrency based on process calculi, but rarely applied directly in programming languages. I will talk about a static analyser we developed for detecting deadlocks in Go, inspired by a research area which gives “types” to process calculi. In a nutshell, the tool infers “types” for communication between goroutines from Go source code, then construct a bird’s eye view of all communication (also called choreography or global graph) possible at runtime, through which deadlocks and communication problems are discovered.
This talk will focus on the work-in-progress aspects of the tool. No knowledge of CSP/process calculi are needed but some understanding of concurrency in Go and static analysis concepts are expected.
About Golang UK
Golang UK is an annual conference on the Go Programming Language and related technologies.
Also featured on department news.