Browse Prior Art Database

PROOF RULES FOR COMMUNICATING SEQUENTIAL PROCESSES

IP.com Disclosure Number: IPCOM000148287D
Original Publication Date: 1980-Aug-31
Included in the Prior Art Database: 2007-Mar-29
Document File: 46 page(s) / 2M

Publishing Venue

Software Patent Institute

Related People

Levin, Gary Marc: AUTHOR [+2]

Abstract

Gary Marc Levin Ph.D. Thesis August 1980 Department of Computer Science Cornell UniversityIthaca, New York 14853 PROOF RULES FOR CO@@JHICATIEG SEQUENTIAL PROCESSES A TtiesisPresented to the Faculty of the Graduate School of Corne l l Univers icyin Partial Fulfillment for the Degree of Doctor of Philosophy Q Gary Narc Levin 196Q ALL XICilTS RESERVED by Gary Ilarc Levin August 19W) The introduction of the satisfaction proof and our sywetric treatment of and receive are important aspects of this thesis. By treating &g& and receive on an equal basis. ve simplify our ruler and allov the inclusion of send in guards. A sufficient condition for freedom from deadlock is zivea tbar depends on the proof of vcak correctness; this ie used to prove strong correctness. In general. freedom from deadlock can-be very hard to check. Therefore. we Jerivc special cases in which we can reduce the work neeCed to verify that a progran is free frnm A_tad!c~k. \le also present an algorithm for globally sycchronizing processes; that is. each process can recognize that a l l processes are sinultaneously in a given state. It works by recognizing a special class of deadlock. \laving this algorithm allovs ua to modify ptob;rms that deadlock when the postcondition is established, so that they terninate noraally.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 4% of the total text.

Page 1 of 46

       PROOF RULES FOR COMMUNICATING SEQUENTIAL PROCESSES

Gary Marc Levin
Ph.D. Thesis August 1980

Department of Computer Science
Cornell University
Ithaca, New
York 14853

[This page contains 1 picture or other non-text object]

Page 2 of 46

[This page contains 1 picture or other non-text object]

Page 3 of 46

PROOF RULES FOR CO@@JHICATIEG SEQUENTIAL PROCESSES

                 A Ttiesis
Presented
to the Faculty of the Graduate School of Corne l l Univers icy
in Partial Fulfillment for the Degree of Doctor of Philosophy

Q Gary Narc Levin 196Q

-

ALL XICilTS RESERVED

by

Gary Ilarc Levin August 19W)

[This page contains 1 picture or other non-text object]

Page 4 of 46

[This page contains 1 picture or other non-text object]

Page 5 of 46

    The introduction of the satisfaction proof and our sywetric treatment of and receive are important aspects of this thesis. By treating &g& and receive on an equal basis. ve simplify our ruler and allov the inclusion of send in guards.

     A sufficient condition for freedom from deadlock is zivea tbar depends on the proof of vcak correctness; this ie used to prove strong correctness. In general. freedom from deadlock can-be very hard to check. Therefore. we Jerivc special cases in which we can reduce the work neeCed to verify that a progran is free frnm A_tad!c~k.

    \le also present an algorithm for globally sycchronizing processes; that is. each process can recognize that a l l processes are sinultaneously in a given state. It works by recognizing a special class of deadlock. \laving this algorithm allovs ua to modify ptob;rms that deadlock when the postcondition is established, so that they terninate noraally.

        Proof Rules for Conmunicating Sequential Processes

 Gary >:arc Levin. Ph.D. Cornell University. 1980

     This thesis presents proof rules for an extension of Iloare's Cmuaicating Sequential Processes (CSP!, CP i6 o nosatzon for describrng processes that interact through communication. which provides the sole leans of synchronizing and passing information betveen processes. A sen61ng process is delayed until some process 1s ready to recelve the cesasge; a receiving process is delayed until there i s a message to be received. It is this delay that provrdes synchronization.

     A proof of a program is vith respect to pre- and postconditions. A proof of veak correctness shous that execution of the progrim beginning in a state satisfyin; the precondition terminates in a state satisfying the postcocdit~on, provided deadlock does not occur. A proof of strong correctness, in addition. shovs that deadlock cannot occur.

     A proof of veak correctness has three stages: a sequential proof, a satisfaction proof. and a non-interference proof. A sequential proof reflects the effects of a process runnlng in isolation. A satisfaction proof cmbines sequential proofs of processes. reflecting the message pass~ng and synchronization aspects ot c...