concurrency - 可以对并发代码进行静态检查吗？

Question

在霍尔的 Communicating Sequential Processes书(也是 Wikipedia )，在用餐哲学家示例的末尾，它说:

There is no hope that a computer will ever be able to explore all these possibilities. Proof of the absence of deadlock, even for quite simple finite processes, will remain the responsibility of the designer of concurrent systems.

他是在说，还是在暗示，并发系统的静态检查是不可能的？

Answer 1

Is he saying, or implying, that static checking of concurrent systems is impossible?

是也不是:)

检查并发系统是不可能的，是的。他是说有时即使是一个更简单的问题也是不可能的。

众所周知(可以证明)并发系统的重要属性通常是不可判定的。以下是有关活锁的此类结果之一:

M.G.Gouda、C.H.Chow、S.S.Lam:关于通信有限状态机网络中活锁检测的可判定性，协议(protocol)规范、测试和验证，IV，Elsevier，1985

关于 CSP 和死锁我不能给出具体的引用，但它们确实存在。引自

Mike R. Jane、Raymond J. Fawcett、Terry P. Mawby:晶片机应用:进展与前景:SERC/DTI 计划在晶片机工程应用方面的闭幕研讨会论文集， IOS 出版社，1992 年 1 月 1 日

The second problem is the result of undisciplined complexity in the communications structure of the design. Unfortunately, deadlock-freedom is not a disciple that can be fully secured through language design -- like the "halting problem", the detection of potential deadlock is not generally computable.

[第 163 页，P.H 韦尔奇 (P.H Welch) 关于奥卡姆的文章]

然而，一般不可判定性并不排除存在可以通过构建证明或使用应用枚举和检查方法的工具来确定感兴趣属性的问题类别。

您问题中的引用指的是后者。它说，当要考虑的状态数量是天文数字时，即使是枚举和检查方法在实践中也是无望的。