static analysis tool developers

Abstract: 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.

Abstract: Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms can appear inside types. Such techniques are known as refinement types, occurrence typing, liquid types, and path dependent types, among others. However, the restrictions adopted by these systems often break the substitution property, because they explicitly disallow the ability to substitute arbitrary terms for variables inside types. This leads to significant complexity in the design and metatheory of these systems, increasing the possibility of significant errors. We consider a specific line of work on occurrence typing, namely, the calculus underlying Typed Racket due to Tobin-Hochstadt and Felleisen 2010. We show that the fundamental challenge of substitution into types resulted in multiple flaws in the formalism and the syntactic type soundness theorem of this work. These flaws are replicated in several other papers building on this work, and also surface as a soundness bug in Typed Racket itself. We identify and repair these problems, revising the core calculus of Typed Racket and giving a \emph{semantic type soundness} proof using step-indexed logical relations, formalized in Lean. We argue that this approach is simpler than it may seem, and easily scales to handle the complexity of the occurrence typing in Typed Racket.