Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
复制标题
Go 程序的静态竞争检测和互斥安全性和活性（扩展版）
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
N. Yoshida
中科院分区：
文献类型：
--
作者：
Julia Gabet;N. Yoshida
Go是一种流行的并发编程语言，这要归功于它能够有效地将并发性和系统编程联合收割机结合起来。在Go程序中，许多并发错误可能是由数据竞争和通信问题引起的。在本文中，我们开发了一种基于行为类型的理论来静态检测Go程序中的数据竞争和死锁。首先，我们使用Go内存模型中定义的happens-before关系，在Go程序模型上指定锁安全性、活动性和数据竞争属性。我们表示这些属性的程序中的$\mu$演算模型的类型，并验证它们使用类型级模型检查。然后，我们扩展了框架，以考虑Go的通道，并实现了一个静态验证工具，可以检测并发错误。据我们所知，这是Go语言的第一个此类静态验证框架，统一分析了由共享内存访问和异步消息传递通信混合引起的并发错误。
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 and 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 $\mu$-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.