Static checking of concurrent code possible?

Question

In Hoare's Communicating Sequential Processes book (also Wikipedia), at the end of the dining philosophers example, it says:

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.

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

Answer 1

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

Yes and no :)

Checking of concurrent systems is impossible, yes. He is saying that even a simpler problem is impossible sometimes.

It is known (can be proven) that important properties of concurrent systems are undecidable in general. One of such results concerning livelock is the following:

M.G.Gouda,C.H.Chow,S.S.Lam: On the decidability of livelock detection in networks of communicating finite state machines, in Protocol Specification, Testing, and Verification, IV, Elsevier, 1985

I cannot give references concerning CSP and deadlock specifically, but they certainly exist. A quote from

Mike R. Jane, Raymond J. Fawcett, Terry P. Mawby: Transputer Applications: Progress and Prospects : Proceedings of the Closing Symposium of the SERC/DTI Initiative in the Engineering Applications of Transputers, IOS Press, Jan 1, 1992

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.

[page 163, P.H Welch writing about Occam]

General undecidability does not exclude however, that there are classes of problems for which properties of interest can be decided, either by constructing proofs, or using tools which apply an enumerate-and-check approach.

The quote in your question refers to the latter. It says that even the enumerate-and-check approach is hopeless in practice when the number of states to consider is astronomical.