Proving Liveness of Parameterized Programs

TL;DR

This paper introduces a method for proving liveness properties in parameterized multi-threaded programs, ensuring correctness regardless of thread count and considering global system behavior.

Contribution

It presents a novel approach to verify liveness in parameterized programs, addressing challenges of global behavior and arbitrary thread numbers.

Findings

Method effectively proves liveness properties in multi-threaded programs.

Ensures correctness for any number of threads.

Addresses global behavior dependencies in correctness proofs.

Abstract

Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold regardless of the number of threads that are active in the program.