The Singularity Theory of Concurrent Programs: A Topological Characterization and Detection of Deadlocks and Livelocks

TL;DR

This paper presents a topological framework for analyzing concurrent programs, modeling execution spaces as branched topological spaces to detect deadlocks and livelocks using algebraic topology tools, offering a geometric approach to verification.

Contribution

It introduces the Singularity Theory, a novel topological paradigm that characterizes and detects deadlocks and livelocks in concurrent programs through algebraic topology invariants.

Findings

Topological invariants effectively identify deadlocks and livelocks.

The framework models execution as a branched topological space.

Algebraic topology tools enable systematic detection without exhaustive search.

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.