DARTS.6.2.12.pdf
- Filesize: 375 kB
- 3 pages
Document
Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)
Authors
Julia Gabet 
,
Nobuko Yoshida
-
Part of:
Issue:
Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Volume: DARTS, Volume 6 (ECOOP 2020)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-11-06
Artifact Description
Document Identifiers
Author Details
Acknowledgements
The authors wish to thank Nicholas Ng for his initial collaboration on the project, David Castro-Perez and Fangyi Zhou for their comments and testing the artifact, and the anonymous reviewers for their comments and suggestions.
Cite As Get BibTex
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)
https://doi.org/10.4230/DARTS.6.2.12
Artifact
DARTS-6-2-12-artifact-0965ca24dfe6c996566c1c25c65d8a07.tgz
(Filesize: 470.66 MB)
MD5 Sum:
0965ca24dfe6c996566c1c25c65d8a07
(Get MD5 Sum)
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.
Subject Classification
ACM Subject Classification
- Software and its engineering → Concurrent programming languages
- Software and its engineering → Model checking
- Theory of computation → Process calculi
Keywords
- Go language
- behavioural types
- race detection
- happens-before relation
- safety
- liveness
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Proceedings of the 40th International Conference on Software Engineering, ICSE '18, pages 1137-1148, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3180155.3180157.