并发程序的奇点理论：拓扑特征与死锁与活锁检测

本文引入了一种新颖的并发程序分析与验证范式——奇点理论。我们将并发程序的执行空间建模为分支拓扑空间，其中程序状态为点，状态转换为路径。在此框架下，我们将死锁表述为吸引子，将活锁表述为执行空间中的非收缩环。通过运用代数拓扑工具，特别是同伦与同调群，我们定义了一系列并发拓扑不变量，以系统性地检测和分类这些并发“奇点”，而无需穷举遍历所有状态。本工作旨在为并发程序验证建立几何与拓扑基础，超越传统模型检查的局限性。