The Singularity Theory of Concurrent Programs: A Topological Characterization and Detection of Deadlocks and Livelocks
Di Zhang
TL;DR
This work reframes concurrent program verification through Singularity Theory by modeling the execution space as a directed topological space $X_P$ and identifying deadlocks as attractors and livelocks as non-contractible loops in the fair subspace $X_{\text{fair}}$. It introduces the fair homology invariant $H_1^{\text{fair}}(X_P)$ to detect livelocks without exhaustive path enumeration, and defines related concepts such as the future homotopy set and battle-tested notions of reachability. The framework is designed to be functorial and robust under refinement, offering a geometry-based complement to model checking and theorem proving while enabling approximation via finite simplicial complexes and persistent homology. The approach promises a shape-based verification paradigm that reveals fundamental architectural vulnerabilities in concurrent systems and suggests practical pathways to scalable analysis and tool development.
Abstract
This paper introduces a novel paradigm for the analysis and verification of concurrent programs -- the Singularity Theory. We model the execution space of a concurrent program as a branched topological space, where program states are points and state transitions are paths. Within this framework, we characterize deadlocks as attractors and livelocks as non-contractible loops in the execution space. By employing tools from algebraic topology, particularly homotopy and homology groups, we define a series of concurrent topological invariants to systematically detect and classify these concurrent "singularities" without exhaustively traversing all states. This work aims to establish a geometric and topological foundation for concurrent program verification, transcending the limitations of traditional model checking.