eCommons

 

Proof Rules for Communicating Sequential Processes

Other Titles

Abstract

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.

Journal / Series

Volume & Issue

Description

Sponsorship

Date Issued

1980-08

Publisher

Cornell University

Keywords

computer science; technical report

Location

Effective Date

Expiration Date

Sector

Employer

Union

Union Local

NAICS

Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)

References

Link(s) to Reference(s)

Previously Published As

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR80-435

Government Document

ISBN

ISMN

ISSN

Other Identifiers

Rights

Rights URI

Types

technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record