DROPS

Document

Artifact

Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)

Authors: Julia Gabet and Nobuko Yoshida

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

This artifact contains a version of the Godel tool that checks MiGo+ types - an extension of MiGo from [Lange et al., 2018] including GoL. Given the extracted MiGo+ types, the tool can analyse them using the mCRL2 model checker to check several properties including liveness, safety and data race freedom as defined in our paper. The artifact also includes examples, shipped with both the source of the Godel tool and the benchmark repository. The latter also contains the Go source for the benchmark examples. We provide compiled binaries of the artifact in a Docker image, with instructions on how to use them. Finally, for convenience, the Docker image also contains a binary version of the migoinfer+ tool, developed as a fork from the original migoinfer by Nicholas Ng in [Lange et al., 2018]. This new version adds the ability to extract shared memory pointers as well as Mutex and RWMutex locks.

Cite as

Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{gabet_et_al:DARTS.6.2.12,
  author =	{Gabet, Julia and Yoshida, Nobuko},
  title =	{{Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)}},
  pages =	{12:1--12:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Gabet, Julia and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.12},
  URN =		{urn:nbn:de:0030-drops-132096},
  doi =		{10.4230/DARTS.6.2.12},
  annote =	{Keywords: Go language, behavioural types, race detection, happens-before relation, safety, liveness}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2020.4

Static Race Detection and Mutex Safety and Liveness for Go Programs

Authors: Julia Gabet and Nobuko Yoshida

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

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.

Cite as

Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gabet_et_al:LIPIcs.ECOOP.2020.4,
  author =	{Gabet, Julia and Yoshida, Nobuko},
  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 =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.4},
  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}
}

Search Results

Documents authored by Gabet, Julia

Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)

Abstract

Cite as

Static Race Detection and Mutex Safety and Liveness for Go Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message