eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6393
Title:  Axiomatic Proof Techniques for Parallel Programs 
Authors:  Owicki, Susan S. 
Keywords:  computer science technical report 
Issue Date:  Jul1975 
Publisher:  Cornell University 
Citation:  http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR75251 
Abstract:  This thesis presents an axiomatic method for proving certain correctness properties of parallel programs. Axioms and inference rules for partial correctness are given for two parallel programming languages: The General Parallel Language and the Restricted Parallel Language. The General Language is flexible enough to represent most standard synchronizers (e.g. semaphores, events), so that programs using these synchronizers may be verified using the GPL deductive system. However, proofs for GPL programs are in general quite complex. The Restricted Language reduces this complexity by requiring shared variables to be protected by critical sections, so that only one process at a time has access to them. This discipline does not significantly reduce the power of the language, and it greatly simplifies the process of program verification. Although the axioms and inference rules are primarily intended for proofs of partial correctness, there are a number of other important properties of parallel programs. We give some practical techniques which use information obtained from a partial correctness proof to derive other correctness properties, including program termination, mutual exclusion, and freedom from deadlock. A number of examples of such proofs are given. Finally, the axioms and inference rules are shown to be consistent and complete (in a special sense) with respect to an interpretive model of parallel execution. Thus the deductive system gives an accurate description of program execution and is powerful enough to yield a proof of any true partial correctness formula. 
URI:  http://hdl.handle.net/1813/6393 
Appears in Collections:  Computer Science Technical Reports

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
