Static trace-based deadlock analysis for synchronous Mini-Go

DOI10.1007/978-3-319-47958-3_7MaRDI QIDQ3179284zbMATH OpenOpenAlexFDO

Authors Kai Stadtmüller, Martin Sulzmann, Peter J. Thiemann

Publication date 21 December 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1608.08330

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We consider the problem of static deadlock detection for programs in the Go programming language which make use of synchronous channel communications. In our analysis, regular expressions extended with a fork operator capture the communication behavior of a program. Starting from a simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods to check for deadlock-freedom. The approach is implemented and evaluated with a series of examples.

Recommendations

• Fencing off Go: liveness and safety for channel-based programming
• Process-local static analysis of synchronous processes
• An automatic technique for static deadlock prevention
• Deadlock analysis of unbounded process networks
• Towards static deadlock resolution in the -calculus

Cites work

• scientific article; zbMATH DE number 1670564 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• A New Type System for Deadlock-Free Processes
• Communicating sequential processes
• Concurrent Programming in ML
• Derivatives of Regular Expressions
• Forkable regular expressions
• Type-based information flow analysis for the \(\pi\)-calculus

Cited in

(4)

• Fencing off Go: liveness and safety for channel-based programming
• Deadlock detection for actor-based coroutines
• Process-local static analysis of synchronous processes
• Static analysis based on formal models and incremental computation in Go programming

Describes a project that uses

Uses Software

• GitHub
• TyPiCal
• Gopherlyzer
• go
• RacerX

This page was built for publication: Static trace-based deadlock analysis for synchronous Mini-Go

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179284)