在过去的几周里，我一直在开发一些并发程序，想知道是否有任何工具可以自动检测其操作保证的进度条件，即无等待、无锁定还是无障碍。
我在网上搜索了一下，没有找到任何这样的工具。
能告诉我们如何推导程序的进度条件吗？
假设我有一个名为等待自由决策器的程序，它可以读取描述数据结构的并发程序并检测它是否是无等待的，即"保证任何进程都可以在有限的步骤数内完成任何操作的程序"，如Herlihy的"无等待同步"。然后，给定一个单线程程序P，创建一个程序，我们将其输入等待自由决策器：
class DataStructure:
def operation(this):
P
pass
现在，当且仅当P停止时，DataStructure.operation在有限数量的步骤中完成。
这将解决停顿的问题。这是不可能的，所以，矛盾的是，我们一定不能创造一个等待自由的决定者。