English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Go is a popular concurrent programming language thanks to its ability toefficiently combine concurrency and systems programming. In Go programs, anumber of concurrency bugs can be caused by a mixture of data races andcommunication problems. In this paper, we develop a theory based on behaviouraltypes to statically detect data races and deadlocks in Go programs. We firstspecify lock safety and liveness and data race properties over a Go programmodel, using the happens-before relation defined in the Go memory model. Werepresent these properties of programs in a $\mu$-calculus model of types, andvalidate them using type-level model-checking. We then extend the framework toaccount for Go's channels, and implement a static verification tool which candetect concurrency errors. This is, to the best of our knowledge, the firststatic verification framework of this kind for the Go language, uniformlyanalysing concurrency errors caused by a mix of shared memory accesses andasynchronous message-passing communications.

Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)