This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
November 1979 (vol. 5 no. 6)
pp. 558-574
A.F. Babich, Basic Four Corporation
An approach to proving paralel programs correct is presented. The steps are 1) model the paralel program, 2) prove partial correctness (proper synchronization), and 3) prove the absence of deadlock, livelock, and infinite loops. The parallel program model is based on KeUler's model. The main contributions of the paper are techniques for proving the absence of deadlock and livelock. A connection is made between Keler's work and Dijkstra's work with serial non-deterministic programs. It is shown how a variant function may be used to prove finite termination, even if the variant function is not strictly decreasing, and how finite termination can be used to prove the absence of livelock. Handling of the finite delay assumption is also discussed. The illustrative examples indude one which occurred in a commercial environment and a classic synchronization problem solved without the aid of special synchronization primitives.
Index Terms:
verification, Concurrent program, correctness, deadlock, finite delay, finite termination, infinite loops, lvelock, mutual exclusion, parallel program, termination, variant function
Citation:
A.F. Babich, "Proving Total Correctness of Parallel Programs," IEEE Transactions on Software Engineering, vol. 5, no. 6, pp. 558-574, Nov. 1979, doi:10.1109/TSE.1979.230192
Usage of this product signifies your acceptance of the Terms of Use.