This Article 
 Bibliographic References 
 Add to: 
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
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.