The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - November (1979 vol.5)
pp: 558-574
A.F. Babich , Basic Four Corporation
ABSTRACT
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, November 1979, doi:10.1109/TSE.1979.230192
35 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool