Dihomotopic Deadlock Detection via Progress Shell Decomposition

The classical problem of deadlock detection for concurrent programs has traditionally been accomplished by symbolic methods or by search of a state transition system. This work examines an approach that uses geometric semantics involving the topological notion of dihomotopy to partition the state space into components, followed by search of a reduced state space. Prior work partitioned the state-space inductively. In this work, a decomposition technique motivated by recursion coupled with a search guided by the decomposition is shown to effectively reduce the size of state transition systems. The reduced state space yields asymptotic improvement in overall runtime for verification. A prototype implementation of this method is introduced here, including a description of its theoretical foundation and its performance benchmarked against the SPIN model checker.