Skip to main content

Bounded Verification of Message-Passing Concurrency in Go

Dilley, Nicolas (2022) Bounded Verification of Message-Passing Concurrency in Go. Doctor of Philosophy (PhD) thesis, University of Kent,. (doi:10.22024/UniKent/01.02.98644) (KAR id:98644)

Language: English

Download (1MB) Preview
[thumbnail of 78main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Go is a programming language that has gained increased popularity due to its good support for system programming and its channel-based message passing concurrency mechanism. These features rendered Go the language of choice of many platform software developers. Go offers a wide range of primitives to coordinate lightweight threads, e.g., channels, waitgroups, and mutexes. Although, these concurrency primitives help mitigate data races, they introduce additional complications due to the complexity of reasoning about concurrency. In this thesis, we first perform an empirical analysis on concurrent Go programs which analyses 125 Go projects from GitHub in order to understand how concurrency is used in publicly available code. Our results include the following findings: (1) concurrency primitives are used frequently and intensively, (2) most projects use synchronous communication channels over asynchronous ones, and (3) most Go projects use simple concurrent thread topologies, which are however currently not fully supported by existing static verification frameworks. To address these limitations, we propose a novel static checker for Go programs that relies on performing bounded model checking of their concurrent behaviours. In contrast to previous works, our approach deals with large codebases, supports programs that have statically unknown parameters and is extensible to additional concurrency primitives. Our work includes an empirical analysis that studies the usage of concurrency in Go projects, a detailed presentation of the extraction algorithm from Go programs to Promela models, an algorithm to automatically check programs with statically unknown parameters, and a large scale evaluation of our approach. The latter shows that our approach outperforms the state-of-the-art.

Item Type: Thesis (Doctor of Philosophy (PhD))
Thesis advisor: Lange, Julien
DOI/Identification number: 10.22024/UniKent/01.02.98644
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: University of Kent (
SWORD Depositor: System Moodle
Depositing User: System Moodle
Date Deposited: 02 Dec 2022 12:10 UTC
Last Modified: 06 Dec 2022 10:12 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year