An axiomatic proof technique for parallel programs I |
| |
| Authors: | Susan Owicki David Gries |
| |
| Affiliation: | (1) Computer Science Dept., Cornell University, 14853 Ithaca, NY, USA;(2) Dept. of Computer Science, Cornell University, Upson Hall, 14850 Ithaca, N.Y., USA |
| |
| Abstract: | Summary A language for parallel programming, with a primitive construct for synchronization and mutual exclusion, is presented. Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language. The proof method lends insight into how one should understand and present parallel programs. Examples are given using several of the standard problems in the literature. Methods for proving termination and the absence of deadlock are also given.This research was partially supported by National Science Foundation grant GJ-42512. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
