This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
19th Annual Symposium on Foundations of Computer Science (FOCS 1978)
Consistent and complete proof rules for the total correctness of parallel programs
October 16-October 18
We describe a formal theory of the total correctness of parallel programs, including such heretofore theoretically incomplete properties as safety from deadlock and starvation. We present a consistent and complete set of proof rules for the total correctness of parallel programs expressed in nondeterministic form. The proof of consistency and completeness is novel in that we show that the weakest preconditions for each correctness criterion are actually fixed-points (least or greatest) of continuous functions over the complete lattice of total predicates. We have obtained proof rule schemata which can universally be applied to least or greatest fixed points of continuous functions. Therefore, our proof rules are a priori consistent and complete once it is shown that certain weakest preconditions are extremum fixed-points. The relationship between true parallelism and nondeterminism is also discussed.
Citation:
Lawrence Flon, Norihisa Suzuki, "Consistent and complete proof rules for the total correctness of parallel programs," focs, pp.184-192, 19th Annual Symposium on Foundations of Computer Science (FOCS 1978), 1978
Usage of this product signifies your acceptance of the Terms of Use.