Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems

This paper studies the problem of verifying temporal properties (including liveness properties) of parametrized concurrent systems executed by an unbounded number of threads. To solve this problem we introduce parametrized verification diagrams (PVDs), that extend the so-called generalized verification diagrams (GVDs) adding support for parametrized verification. Even though GVDs are known to be a sound and complete proof system for non-parametrized systems, the application of GVDs to parametrized systems requires using quantification or finding a potentially different diagram for each instantiation of the parameter (number of threads). As a consequence, the use of GVDs in parametrized verification requires discharging and proving either quantified formulas or an unbounded collection of verification conditions. Parametrized verification diagrams enable the use of asinglediagram to represent the proof that all possible instances of the parametrized concurrent system satisfy the given 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 assume that the parametrized systems are symmetric, which covers a large class of concurrent and distributed systems, including concurrent data types. Our second contribution is an implementation of PVDs and its integration into Leap, our prototype theorem prover. Finally, we illustrate empirically, using Leap, the practical applicability of PVDs by building and checking proofs of liveness properties of mutual exclusion protocols and concurrent data structures. To the best of our knowledge, these are the first machine-checkable proofs of liveness properties of these concurrent data types.