论文标题
GO计划的静态比赛检测和MUTEX安全性和livese（扩展版）
Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
论文作者
论文摘要
GO是一种流行的并发编程语言，这要归功于其有效地结合并发和系统编程的能力。在GO程序中，许多并发错误可能是由数据竞赛和通信问题的混合物引起的。在本文中，我们开发了一种基于行为类型的理论，可以在GO计划中静态检测数据和僵局。我们首先使用GO内存模型中定义的关系，在GO计划模型上指定锁定安全性，可感知和数据竞赛属性。我们以$ $ $ $ calculus类型的模型表示程序的这些属性，并使用类型级的模型检查来验证它们。然后，我们扩展框架以说明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 $μ$-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.
