Proof Rules for Communicating Sequential Processes

This thesis presents proof rules for an extension of Hoare's Communicating Sequential Processes (CSP). CSP is a notation for describing processes that interact through communication, which provides the sole means of synchronizing and passing information between processes. A sending process is delayed until some process is ready to receive the message; a receiving process is delayed until there is a message to be received. It is this delay that provides synchronization. A proof of a program is with respect to pre- and postconditions. A proof of weak correctness shows that execution of the program beginning in a state satisfying the precondition terminates in a state satisfying the postcondition, provided deadlock does not occur. A proof of strong correctness, in addition, shows that deadlock cannot occur. A proof of weak correctness has three stages: a sequential proof, a satisfaction proof, and a non-interference proof. A sequential proof reflects the effects of a process running in isolation. A satisfaction proof combines sequential proofs of processes, reflecting the message passing and synchronization aspects of communication. A non-interference proof shows that no process affects the validity of the proof of another process. The introduction of the satisfaction proof and our symmetric treatment of send and receive are important aspects of this thesis. By treating send and receive on an equal basis, we simplify our rules and allow the inclusion of send in guards. A sufficient condition for freedom from deadlock is given that depends on the proof of weak correctness; this is used to prove strong correctness. In general, freedom from deadlock can be very hard to check. Therefore, we derive special cases in which we can reduce the work needed to verify that a program is free from deadlock. We also present an algorithm for globally synchronizing processes; that is, each process can recognize that all processes are simultaneously in a given state. It works by recognizing a special class of deadlock. Having this algorithm allows us to modify programs that deadlock when the postcondition is established, so that they terminate normally