Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs: Intro

Table of Links

• Introduction
• Dynamic Networks of Concurret Pushdown Systems (DCPS)
• Warm-up: Non-Termination
• Fair Non-Termination
• From Progressive Runs for VASSB to Reachability
• Starvation
• Conclusion, Acknowledgment & References
• A. Strengthening Fairness to Progressive Runs
• B. Proofs from Section 4.1
• C. Proofs for Section 5
• D. Proofs for Section 5.3
• E. Proofs for Section 6

We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-bounded implies that each spawned thread can be context switched a fixed constant number of times. Our proof is technical, since fair termination requires reasoning about the composition of unboundedly many threads each with unboundedly large stacks. In fact, techniques for related problems, which depend crucially on replacing the pushdown threads with finite-state threads, are not applicable. Instead, we introduce an extension of vector addition systems with states (VASS), called VASS with balloons (VASSB), as an intermediate model; it is an infinite-state model of independent interest. A VASSB allows tokens that are themselves markings (balloons). We show that context bounded fair termination reduces to fair termination for VASSB. We show the latter problem is decidable by showing a series of reductions: from fair termination to configuration reachability for VASSB and thence to the reachability problem for VASS. For a lower bound, fair termination is known to be non-elementary already in the special case where threads run to completion (no context switches).

We also show that the simpler problem of context-bounded termination is 2EXPSPACE-complete, matching the complexity bound—and indeed the techniques—for safety verification. Additionally, we show the related problem of fair starvation, which checks if some thread can be starved along a fair run, is also decidable in the context-bounded case. The decidability employs an intricate reduction from fair starvation to fair termination. Like fair termination, this problem is also non-elementary.

1 INTRODUCTION

We study decision problems related to liveness verification of shared-memory multithreaded programs. In a shared-memory multithreaded program, a number of threads execute concurrently. Each thread executes possibly recursive sequential code, and can spawn new threads for concurrent execution. The threads communicate through shared global variables that they can read and write. The execution of the program is guided by a non-deterministic scheduler that picks one of the spawned threads to execute in each time step. If the scheduler replaces the currently executing thread with a different one, we say the current active thread is context switched.

Shared-memory multithreaded programming is ubiquitous and static verification of safety or liveness properties of such programs is a cornerstone of formal verification research. Indeed, there is a vast research literature on the problem—from a foundational understanding of the computability and complexity of (subclasses of) models, to program logics, and to efficient tools for analysis of real systems.

In this paper, we focus on decidability issues for liveness verification for multithreaded shared memory programs with the ability to spawn threads. Liveness properties, intuitively, specify that “something good” happens when a program executes. A simple example of a liveness property is termination: the property that a program eventually terminates. In fact, termination is a “canonical” liveness property: for a very general class of liveness properties, through monitor constructions, verifying liveness properties reduces to verifying termination [Apt and Olderog 1991; Vardi 1991].

Unfortunately, under the usual notion of non-deterministic schedulers, some programs may fail to terminate for uninteresting reasons. Consider the following program:

1 global bit := 1;

2 main () { spawn foo ; spawn bar ; }

3 foo () { if bit = 1 then spawn foo ; }

4 bar () { bit := 0; }

A main thread spawns two additional threads foo and bar. The thread foo checks if a global bit is set and, if so, re-spawns itself. The thread bar resets the global bit. There is a non-terminating execution of this program in which bar is never scheduled. However, a scheduler that never schedules a thread that is ready to run would be considered unfair. Instead, one formulates the problem of fair termination: termination under a fair non-deterministic scheduler. We abstract away from the exact mechanism of the scheduler, and only require that every spawned thread that is infinitely often ready to run is eventually scheduled. Then, every fair run of the above program is terminating: eventually bar is scheduled, after which foo does not spawn a new thread.

Since the high undecidability relies on an unbounded exchange of information among threads, a recent and apposite approach to verifying concurrent recursive programs is to explore only a representative subset of program behaviors by limiting the number of inter-thread interactions [Musuvathi and Qadeer 2007; Qadeer and Rehof 2005]. This approach, called context bounding by Qadeer and Rehof [2005], considers the verification problem as a family of problems, one for each K. The K-context bounded instance, for any fixed K ≥ 0, considers only those executions where each thread is context switched at most K times by the scheduler. In the limit as K → ∞, the K-bounded approach explores all behaviors where each thread runs a finite number of times. In practice, bounded explorations with small values of K have proved to be effective to uncover many safety and liveness bugs in real systems.

Our results generalize the special case of K = 0 studied by Ganty and Majumdar [2012] as asynchronous programs. When K = 0, each thread executes to completion without being interrupted in the middle. Ganty and Majumdar show the decidability of safety and liveness verification for this model. In particular, they prove safety and termination are both EXPSPACE-complete and fair termination and fair starvation are decidable but non-elementary.[2] Their proof depends on the observation that, since threads are not interrupted, one can replace the pushdown automata for each thread by finite automata that accept Parikh-equivalent languages. Unfortunately, their technique does not generalize when context switches are allowed.

For K ≥ 1, Atig et al. [2009] showed that the safety verification problem is decidable in 2EXPSPACE. Ten years later, a matching lower bound was shown by Baumann et al. [2020]. The key observation in the decision procedure is that safety is preserved under downward closures: one can analyze a related program where some spawned threads are “forgotten.” Since the downward closure of a context free language is effectively regular, one can replace the pushdown automaton for each thread by a finite automaton accepting the downward closure. In fact, our proof of termination also follows easily from this observation, as termination is also preserved by downward closures.

Unfortunately, fair termination and fair non-starvation are not preserved under downward closures. Thus, we cannot apply the preceding techniques to replace pushdown automata by finite automata in our construction. Thus, our proof is more intricate and requires several insights into the computational model.

The key difficulty in our decision procedure is to maintain a finite representation for unboundedly many active threads, each with unboundedly large local stacks and potentially spawning unboundedly many new threads, and to compose their context-switched executions into a global execution. In order to maintain and compose such configurations, we introduce a new model, called VASS with balloons (VASSB), that extends the usual model of a vector addition systems with states (VASS) with “balloons”: a token in a VASSB can be a usual VASS token or a balloon token that is itself a vector. Intuitively, balloon tokens represent the possible new threads a thread can spawn along one of its execution segments.

We show through a series of constructions that the fair termination problem reduces to the fair termination problem for VASSB, and thence to the configuration reachability problem for VASSB. Finally, we show that configuration reachability for VASSB is decidable by a reduction to the reachability problem for VASS. This puts VASSB in the rare class of infinite-state systems which generalize VASS and yet maintain a decidable reachability (not just coverability!) problem.

Finally, we show a reduction from the fair starvation problem to fair termination. The reduction relies on two combinatorial insights. The first is that if a program has an infinite fair run, then it has one in which there exists a bound on the number of threads spawned by each thread. The second is a novel pumping argument based on Ramsey’s theorem; it implies that it suffices to track a finite amount of data about each thread to determine whether some thread can be starved.

In conclusion, we prove decidability of liveness verification for multithreaded shared memory programs with the ability to dynamically spawn threads, an extremely expressive model of multithreaded programming. This model sits at the boundary of decidability and subsumes many other models studied before.

Related Work. Safety verification for concurrent recursive programs is already undecidable with just two threads and finite global store [Ramalingam 2000]. Many results on context-bounded safety verification consider a model with a fixed number of threads, without spawns. The complexity of safety verification for this model is well understood at this point. The key idea underlying the best algorithms reduce the problem to analyzing a sequential pushdown system [Lal and Reps 2009] by guessing the bounded sequences of context switches for each thread and using the finite state to ensure the sequential runs can be stitched together

When the model allows spawning of new threads, as ours does, existing decision procedures are significantly more complex, both in their technicalities and in computational cost. There are relatively few results on decidability of liveness properties of infinite-state systems. Atig et al. [2012a] show a sufficient condition for fair termination for context-bounded executions of a fixed number of threads, where they look for ultimately periodic executions, in which each thread is context switched at most K times in the loop. They show that the search for such ultimately periodic executions can be reduced to safety verification. In our model, fair infinite runs may involve unboundedly many threads with unbounded stacks and need not be periodic—for example, there can always be more and more newly spawned threads.

Multi-pushdown systems model multithreaded programs with a fixed number of threads. Many decision procedures are known when the executions of such systems are restricted through different bounds such as context, scope, or phase [Atig et al. 2012b, 2017; Torre et al. 2016], and also through limitations on communication patterns [Lal et al. 2008]. These problems are orthogonal to us, either in the modeling capabilities or in the properties verified.

Decidability of linear temporal logic is known for weaker models of multithreaded recursive programs, such as symmetric parameterized programs [Kahlon 2008] or leader-follower programs with non-atomic reads and writes [Durand-Gasselin et al. 2017; Fortin et al. 2017; Muscholl et al. 2017]. These programs cannot perform compare-and-swap operations, and therefore, their computational power is quite limited (in fact, LTL model checking is PSPACE-complete). A number of heuristic approaches to fair termination of multithreaded programs provide sound but incomplete algorithms, but for a more general class of programs involving infinite-state data variables [Cook et al. 2007, 2011; Farzan et al. 2016; Kragl et al. 2020; Padon et al. 2018]. The goal there is to provide a sound proof rule for verification but not to prove a decidability result.

In terms of fair termination problems for VASS, the theme of computational hardness continues. For example, the classical notion of fair runs, in which an infinitely activated transition has to be fired infinitely often, leads to undecidability [Carstensen 1987] and even Σ 1 1 - completeness [Howell et al. 1991]. However, weakly fair termination, where only those transitions that are almost always activated have to be fired infinitely often, is decidable [Jančar 1990]. A rich taxonomy of fairness notions with corresponding decidability results can be found in [Howell et al. 1991]. However, all of these notions appear to be incomparable with our fairness notion for VASSB.

Our model of VASSB treads the boundary of models that generalize VASS for which reachability can be proved to be decidable. We note that there are several closely related models, VASS with a stack [Leroux et al. 2015] and branching VASS [Verma and Goubault-Larrecq 2005], for which decidability of reachability is a long-standing open problem, and others, nested Petri nets [Lomazova and Schnoebelen 1999], for which reachability is undecidable.

[1] Recall that the class Π 1 1 in the analytic hierarchy is the class of all relations on N that can be defined by a universal second-order number-theoretic formula.

[2] Their result shows a polynomial-time equivalence between fair termination and reachability in vector addition systems with states (VASS, a.k.a. Petri nets). The complexity bounds follow from our current knowledge of the complexity of VASS reachability [Czerwinski et al. 2019].