Issue No. 06 - November (1979 vol. 5)
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.
verification, Concurrent program, correctness, deadlock, finite delay, finite termination, infinite loops, lvelock, mutual exclusion, parallel program, termination, variant function
A. Babich, "Proving Total Correctness of Parallel Programs," in IEEE Transactions on Software Engineering, vol. 5, no. , pp. 558-574, 1979.