License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2020.4
URN: urn:nbn:de:0030-drops-131615
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13161/
Gabet, Julia ;
Yoshida, Nobuko
Static Race Detection and Mutex Safety and Liveness for Go Programs
Abstract
Go is a popular concurrent programming language thanks to its ability to efficiently combine concurrency and systems programming. In Go programs, a number of concurrency bugs can be caused by a mixture of data races and communication problems. In this paper, we develop a theory based on behavioural types to statically detect data races and deadlocks in Go programs. We first specify lock safety/liveness and data race properties over a Go program model, using the happens-before relation defined in the Go memory model. We represent these properties of programs in a μ-calculus model of types, and validate them using type-level model-checking. We then extend the framework to account for Go’s channels, and implement a static verification tool which can detect concurrency errors. This is, to the best of our knowledge, the first static verification framework of this kind for the Go language, uniformly analysing concurrency errors caused by a mix of shared memory accesses and asynchronous message-passing communications.
BibTeX - Entry
@InProceedings{gabet_et_al:LIPIcs:2020:13161,
author = {Julia Gabet and Nobuko Yoshida},
title = {{Static Race Detection and Mutex Safety and Liveness for Go Programs}},
booktitle = {34th European Conference on Object-Oriented Programming (ECOOP 2020)},
pages = {4:1--4:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-154-2},
ISSN = {1868-8969},
year = {2020},
volume = {166},
editor = {Robert Hirschfeld and Tobias Pape},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13161},
URN = {urn:nbn:de:0030-drops-131615},
doi = {10.4230/LIPIcs.ECOOP.2020.4},
annote = {Keywords: Go language, behavioural types, race detection, happens-before relation, safety, liveness}
}
