2 Search Results for "Gabet, Julia"

Document
Artifact
DOI: 10.4230/DARTS.6.2.12
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-dev.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}
}
  • Refine by Author
  • 2 Gabet, Julia
  • 2 Yoshida, Nobuko

  • Refine by Classification
  • 2 Software and its engineering → Concurrent programming languages
  • 2 Software and its engineering → Model checking
  • 2 Theory of computation → Process calculi

  • Refine by Keyword
  • 2 Go language
  • 2 behavioural types
  • 2 happens-before relation
  • 2 liveness
  • 2 race detection
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact