首页    期刊浏览 2024年11月05日 星期二
登录注册

文章基本信息

  • 标题:Static Race Detection and Mutex Safety and Liveness for Go Programs
  • 本地全文:下载
  • 作者:Julia Gabet ; Nobuko Yoshida
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2020
  • 卷号:166
  • 页码:1-30
  • DOI:10.4230/LIPIcs.ECOOP.2020.4
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:Go language; behavioural types; race detection; happens-before relation; safety; liveness
国家哲学社会科学文献中心版权所有