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.
considers systems that consist of unboundedly many finite-state processes running in parallel @cite_32 @cite_8 @cite_21 @cite_18 @cite_25 @cite_3 . In this paper, we develop an approach to the problem of verifying liveness properties of parameterized , in which processes are infinite state. This demands substantially different techniques than those used in parameterized model checking. The techniques used in this paper are more closely related to and .
@cite_18 @cite_8 @cite_21 @cite_32 @cite_3 @cite_25
2761734916 1861590051 2129073086 1988987404
We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We present regular model checking, a framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized linear topology. States are represented by strings over a finite alphabet and the transition relation by a regular length-preserving relation on strings. Major problems in the verification of parameterized and infinite-state systems are to compute the set of states that are reachable from some set of initial states, and to compute the transitive closure of the transition relation. We present two complementary techniques for these problems. One is a direct automata-theoretic construction, and the other is based on widening. Both techniques are incomplete in general, but we give sufficient conditions under which they work. We also present a method for verifying ω-regular properties of parameterized systems, by computation of the transitive closure of a transition relation. We analyze the model-checking problems for safety and liveness properties in parameterized broadcast protocols. We show that the procedure suggested previously for safety properties may not terminate, whereas termination is guaranteed for the procedure based on upward closed sets. We show that the model-checking problem for liveness properties is undecidable. In fact, even the problem of deciding if a broadcast protocol may exhibit an infinite behavior is undecidable. This paper introduces parametrized verification diagrams (PVDs), a formalism that allows to prove temporal properties of parametrized concurrent systems, in which a given program is executed by an unbounded number of processes. PVDs extend general verification diagrams (GVDs). GVDs encode succinctly a proof that a non-parametrized reactive system satisfies a given temporal property. Even though GVDs are known to be sound and complete for non-parametrized systems, proving temporal properties of parametrized systems potentially requires to find a different diagram for each instantiation of the parameter (number of processes). In turn, each diagram requires to discharge and prove a different collection of verification conditions. PVDs allow a emph[single] diagram to represent the proof that all instances of the parametrized system for an arbitrary number of threads running concurrently satisfy the temporal specification. Checking the proof represented by a PVD requires proving only a finite collection of quantifier-free verification conditions. The PVDs we present here exploit the symmetry assumption, under which process identifiers are interchangeable. This assumption covers a large class of concurrent systems, including concurrent data types. We illustrate the use of PVDs in the verification of an infinite state mutual exclusion protocol.