Browse Prior Art Database

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]


Gary Marc Levin Ph.D. Thesis August 1980

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


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


                 A Ttiesis
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




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...