1;3409;0c Proving Liveness Properties of Concurrent Programs

Proving Liveness Properties of Concurrent Programs

ACM Transactions on Programming Languages and Systems, vol. 4, no. 3, 1982
Pages: 455-495DOI: 10.1145/357172.357178



A liveness property asserts that program execution eventually reaches ome desirable state. While termination has been studied extensively, many other liveness properties are important for concurrent programs. A formal proof method, based on temporal ogic, for deriving liveness properties is presented. It allows a rigorous formulation of simple informal arguments. How to reason with temporal logic and how to use safety (invariance) properties in proving liveness is shown. The method is illustrated using, first, a simple programming language without synchronization primitives, then one with semaphores. However, it is applicable to any programming language