Proving Liveness Properties of Concurrent Programs

Abstract

A liveness property asserts that program execution eventually reaches some desirable state.While termination has been studied extensively, many other liveness properties are important for concurrent programs.A formal proof method, based on temporal logic, 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.