Publications

BibTex format

@inproceedings{Gabet:2020:10.4230/LIPIcs.ECOOP.2020.4,
author = {Gabet, J and Yoshida, N},
doi = {10.4230/LIPIcs.ECOOP.2020.4},
pages = {4:1--4:30},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
title = {Static race detection and mutex safety and liveness for Go programs},
url = {http://dx.doi.org/10.4230/LIPIcs.ECOOP.2020.4},
year = {2020}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Gabet,J
AU  - Yoshida,N
DO  - 10.4230/LIPIcs.ECOOP.2020.4
EP  - 1
PB  - Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
PY  - 2020///
SN  - 1868-8969
SP  - 4
TI  - Static race detection and mutex safety and liveness for Go programs
UR  - http://dx.doi.org/10.4230/LIPIcs.ECOOP.2020.4
UR  - http://hdl.handle.net/10044/1/80323
ER  -

Download

ProfessorNobukoYoshida

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)