The Singularity Theory of Concurrent Programs: A Topological Characterization and Detection of Deadlocks and Livelocks
Di Zhang
本文介绍了分析和验证并发程序的新范式 - 奇点理论。 我们将并发程序的执行空间建模为分支拓扑空间,其中程序状态是点,状态转换是路径。 在这个框架中,我们将死锁描述为执行空间中的吸引和 livelocks 是非可承包的循环。 通过使用代数拓扑学的工具,特别是同源和同源组,我们定义了一系列并发拓扑不变性,以系统地检测和分类这些并发的“奇点”,而不会详尽地遍历所有状态。 这项工作旨在为并发程序验证建立几何和拓扑基础,超越传统模型检查的限制。
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 s...