Source-linked AI summary
Automatically Detecting and Fixing Deadlocks in Go Code with GoDDaR
Gustavo Feio, Jorge Coelho, Miguel Flor, João M. Lourenço, António Ravara
TL;DR
Go’s runtime detector catches only observed global deadlocks, while static deadlock detection leaves developers with limited help resolving them. GoDDaR analyzes intermediate representations to detect deadlocks and generate source-code fix diffs. Its evaluation reports stronger detection accuracy and viable resolutions that outperform existing automated methods.
Problem
Go’s runtime detector applies only to observed global deadlocks, and although static detectors exist, few tools help resolve detected bugs.
Source: §1 · p. 2Method
GoDDaR uses symbolic analysis over an intermediate representation to detect deadlocks, transforms that representation to resolve them, and outputs source-code diffs.
Source: §1 · p. 2, §3.2 · p. 5Results
GoDDaR exceeds existing alternatives in deadlock-detection accuracy and produces viable resolution strategies that outperform current automated methods.
Source: §1 · p. 3, §4.2 · p. 13Takeaways & Limitations
GoDDaR’s suggested synchronization fixes can parallelize blocking operations to restore program execution.
Source: §1 · p. 2GoDDaR depends on MiGo, which is no longer actively maintained, and most failed analyses stemmed from migoinfer’s inability to generate valid intermediate representations.
Source: §4.2 · p. 13
Abstract
from arXiv · showhide
The Go programming language provides a lightweight abstraction for concurrent programming through goroutines, which are prone to deadlocks. Go includes a runtime detector that aborts execution when all threads are blocked (a global deadlock). However, due to nondeterministic thread scheduling, this runtime mechanism only detects global deadlocks that manifest during execution and cannot identify partial deadlocks, where a subset of goroutines is permanently blocked while at least one remains runnable. Statically detecting local deadlocks is essential for developing dependable concurrent software. While several tools statically detect deadlocks in concurrent programs, few assist developers in fixing them. Detecting and resolving partial deadlocks requires reasoning about complex interleavings and communication patterns, an inherently challenging task. In this paper, we present GoDDaR, a tool that detects unobserved global or partial deadlocks in Go programs and suggests concrete fixes. GoDDaR translates Go source code into an intermediate representation reflecting message-passing communication events and composition patterns. Partial deadlocks are identified through symbolic analysis over this representation. To resolve detected deadlocks, our algorithms transform the intermediate representation to eliminate problematic synchronization patterns, allowing GoDDaR to generate fix suggestions for the original Go source code as a diff. We evaluate GoDDaR on a benchmark suite of representative deadlock examples from literature and git repositories to validate algorithm correctness and compare performance against the state of the art. Results demonstrate that GoDDaR is competitive with top approaches in partial deadlock detection and advances the state of the art in automated deadlock fixing.
1 Introduction
GoDDaR addresses the gap between detecting Go deadlocks and helping resolve them by using symbolic analysis and producing source-code diff suggestions. Its benchmark evaluation reports stronger detection and resolution results than existing tools.
1 Introduction
- Go’s runtime detector aborts on global deadlocks, but deadlocks can also be local, with only some threads blocked.A global deadlock occurs when all threads are blocked.Source: §1 · p. 2
- Static detectors can identify bugs before execution, but resolving them remains under-researched and difficult in complex concurrent programs.The paper builds on an algorithm for disentangling deadlocks in linear CCS.Source: §1 · p. 2
- GoDDaR analyzes intermediate representations to identify deadlocks, derive resolution strategies, and output modifications as diffs applicable to the original Go source.The example fix parallelizes a blocking operation to restore execution.Source: §1 · p. 2
- GoDDaR exceeds existing alternatives in deadlock-detection accuracy and produces viable resolution strategies that outperform current automated methods.The evaluation focuses on deadlocks caused by incorrect channel synchronization, not incorrect lock use for mutual exclusion.Source: §1 · p. 3
2 Related Work
Related work includes runtime monitoring and static analysis for Go concurrency. The approaches trade runtime-path precision against pre-execution detection that depends on abstractions or language subsets.
2 Related Work
- Runtime tools use garbage-collector liveness, post-test goroutine counts, or periodic stack sampling, and prioritize detection over completeness.The examples include Golf, GoLeak, and LeakProf.Source: §2 · p. 3
- Static Go tools model language subsets for property checking, while Go2Pins provides LTL-based liveness and safety verification that can identify deadlocks.Nano-Go and Mini-Go use communication-based representations.Source: §2 · p. 3
- Dynamic detectors observe runtime behavior but cover specific execution paths, while static approaches detect before execution but trade off model fidelity or computational complexity.The paper characterizes this as a trade-off between dynamic and static methodologies.Source: §2 · p. 3
3 GoDDaR
GoDDaR translates inferred Go communication into CCS, uses symbolic analysis to detect deadlocks, and derives source-code fixes. Its CCS model captures Go’s select behavior and important channel patterns.
3 GoDDaR
- GoDDaR is implemented in OCaml and Go and analyzes CCS obtained by translating MiGo programs inferred from Go source.The analysis pipeline is illustrated in Figure 1.Source: §3 · p. 3
3.1 CCS with Internal and External Choice
- The CCS model adds external choice so a Go select branch proceeds only when its communication can synchronise, and includes iteration for unbounded computation.This addresses why standard CCS internal choice does not accurately represent Go select behavior.Source: §3.1 · p. 4
3.2 Deadlock Detection Algorithm
- GoDDaR exhaustively explores CCS execution paths, reporting deadlock when no further reductions are possible while unsynchronised actions remain.It also provides the execution trace leading to the detected state.Source: §3.2 · p. 5
3.3 Deadlock Resolution Algorithms
- GoDDaR uses two recursive rewrites: parallelize problematic actions, or handle outputs similarly while adding a complementary parallel output for inputs.The second strategy preserves the action sequence while breaking the cyclic dependency in the example.Source: §3.3 · pp. 6–7
3.4 Important Go Patterns
- GoDDaR models recursion with dynamic expansion and state caching, truncating repeated states; it also accounts for channel closure and buffered-channel blocking behavior.Reads from closed channels reduce immediately, while writes to them are errors; buffered reads and writes can proceed without blocking when values or capacity are available, respectively, and block when empty or full.Source: Channel closing in Go · p. 7, Recursion · pp. 8–9, Asynchronous Channels · p. 8
4 State of the Art
The evaluation compares GoDDaR with existing tools on deadlock benchmarks and examines its fixes on representative cases. GoDDaR reports the most true positives in the detection benchmark, while the resolution evaluation shows both the patterns it fixes and cases it leaves for manual judgment.
4.1 Deadlock Detection Evaluation
- Detection used 25 benchmark cases, while the resolution comparison covered five representative deadlocks.Of 19 programs GoDDaR translated, CCS sizes ranged from 3 to 67 (median 25); it analyzed the largest in 0.65 seconds.Source: §4.1 · pp. 9, 11, §4.2 · p. 11, Table 3 · p. 12
- 19 of 25 true positives and no false negatives make GoDDaR the benchmark’s top detector; goat analyzes 24 of 25 programs, compared with GoDDaR’s 19.GoDDaR identifies two more bugs than goat (19 versus 17), but goat analyzes more programs.Source: Table 2 · p. 11, §4.1 · p. 11
4.2 Deadlock Resolution Evaluation
- The resolution examples include sequentially ordered communications, circular channel dependencies, and a cyclic dependency in a select branch, addressed by parallelizing blocked operations.The described fixes parallelize the first communication, the send on channel b, or the receive on channel c, depending on the pattern.Source: §4.2 · pp. 11–12
- GoDDaR fixes four patterns that GFix misses by parallelizing blocked operations, but leaves missing-communication cases manual; GFix resolves that case.GoDDaR avoids fixes that may alter intended semantics, such as adding a dummy write whose value could be invalid for the program logic.Source: §4.2 · pp. 12–13, Table 4 · p. 13
- Formal soundness results remain future work, and defining a minimal deadlock fix that preserves original semantics remains a key challenge.Source: §4.2 · p. 13
- The analysis depends on unmaintained MiGo, and most failed analyses stemmed from migoinfer’s inability to generate valid intermediate representations.The authors propose direct CCS translation as a future alternative to improve precision, coverage, and independence from external tools.Source: §4.2 · p. 13
- Recursion handling can loop indefinitely when repeated process-call states occur between reductions, because duplicate-state checks currently cover only reductions.The authors identify checks across all state transitions as a priority.Source: §4.2 · p. 15
- GoDDaR analyzes channel-based synchronization, not deadlocks from misuse of locks for mutual exclusion; support for sync.Mutex and sync.WaitGroup is future work.Source: §4.2 · p. 15