The Hoare Logic Of CSP, and All That

I felt that in [40], I had presented the right way to do assertional (also known as Owicki-Gries style) reasoning about concurrent programs. However, many people were (and perhaps still are) hung up on the individual details of different programming languages and are unable to understand that the same general principles apply to all of them. In particular, people felt that “distributed” languages based on rendezvous or message passing were fundamentally different from the shared-variable language that was considered in [40]. For example, some people made the silly claim that the absence of shared variables made it easier to write concurrent programs in CSP than in more conventional languages. (My response is the equally silly assertion that it’s harder to write concurrent programs in CSP because the control state is shared between processors.)

Schneider agreed with me that invariance was the central concept in reasoning about concurrent programs. He was also an expert on all the different flavors of message passing that had been proposed. We demonstrated in this paper that the basic approach of [40] worked just was well with CSP; and we claimed (without proof) that it also worked in other “distributed” languages. I found it particularly funny that we should be the ones to give a Hoare logic to CSP, while Hoare was using essentially behavioral methods to reason about CSP programs. I’m still waiting for the laughter.