Thread-Modular Verification and Cartesian Abstraction

Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko

Max-Planck Institut für Informatik, Saarbrücken Albert-Ludwigs-Universität Freiburg EPFL IC IIF MTC, Lausanne

Accepted in 2006, last updated in January 2024.

Abstract Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of overapproximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the abstraction that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, we obtain polynomial-time algorithms based on Cartesian abstraction that enjoy increased precision with respect to the Flanagan-Qadeer method. We limit the design space for future polynomial-time algorithms by providing a characterization of minimal precision increase that leads to loss of polynomial-time complexity.

1 Introduction

Verification of multithreaded software is an important and difficult task (e.g. [10], [11]). The number of states of a multithreaded program is exponential in the number of threads. Inherent theoretical restrictions (see [8]) complicate the verification task. However, there are many successful algorithms and tools for different types of communication between components of a concurrent system. For instance, one can mention algorithms in the SPIN model-checker (see [7]). The main challenge is to design algorithms that reason about concurrent software in a modular way. Modularity allows to avoid the explicit construction of the global state space by considering each thread in isolation (see [5] and [6]). Assume-guarantee reasoning (see e.g. [9]) offers a prominent approach to devise thread-modular algorithms. The behavior of each thread with respect to global variables is described by its guarantee. We can view this guarantee as a transition system. Then we apply model-checking procedure on each thread, which is executed in the environment defined by the guarantees of other threads. Additionally we verify that each thread satisfies its own guarantee. However, assume-guarantee reasoning does not provide an insight about the abstraction process involved. All that is known about precision loss during search in a thread’s state space is that during discovering states of the thread, the behavior of all other threads is reduced to their action on global variables. Nothing was known about the loss of precision for the program as a whole. It was unclear whether or how is it possible to represent thread-modular reasoning in the standard framework of abstract interpretation. As soon as the abstraction is identified, it provides additional insight into the algorithms. For instance, one could try to increase precision of the abstraction, to optimize the algorithms, to combine with other abstractions or add refinement. One could construct modifications of the abstraction, derive the corresponding algorithms and look at their runtime and precision. We study the Flanagan-Qadeer algorithm for thread-modular verification. The distinguishing property of this algorithm lies in its low complexity. It is polynomial in the number of threads. The low complexity has its price: the algorithm is incomplete. The algorithm is also of the assume-guarantee type. Each computed guarantee is a set of pairs of valuations of unprimed and primed global variables (g, g′). While model-checking a thread, each time a thread state is discovered, we allow the global variables to be changed according to the guarantees of other threads. Each time the thread itself changes global variables from a discovered state, the corresponding pair of valuations of global variables before and after the step is added to the guarantee. Upon convergence, the environment assumptions are devised and the discovered states of each threads include the reachable thread states. We would like to identify the abstraction used by the Flanagan - Qadeer algorithm to be able to reason about the algorithm. In particular, we would like to know how far one can push the Flanagan-Qadeer algorithm while still being polynomial in time and space. In this paper we study the abstraction used in Flanagan-Qadeer algorithm and identify the boundary. Our result is that Flanagan-Qadeer algorithm implements Cartesian abstraction in special setting with threads (a so-called local Cartesian abstraction). This insight allows us to find the “least modification” of the Flanagan-Qadeer algorithm that leads to the loss of polynomial complexity. Thus, the identification of the abstraction provides the insight into the algorithm itself. Using this boundary, we overcome the inherent limitation of the algorithm, namely being too coarse for many programs of interest. We obtain polynomialtime algorithms that are far more precise, being able to prove absence of errors for a large class of programs on which the original algorithm says “don’t know”. The first method, so-called relaxed frontier search, gains as much precision as possible up to the identified boundary of the Flanagan-Qadeer algorithm. The second method, quadratic thread-modular method, improves on proving mutual exclusion for a large class of multithreaded programs where the original approach failed. These algorithms are based solely on Cartesian abstraction and thus do not exploit the structure of the underlying transition relations of threads. Their potential is that they can be can still be combined with other optimization techniques on other levels. For example, on the level of the transition relation, consider abstraction refinement (see [6]). We also suggest constructing more precise polynomial-time algorithms based on Cartesian abstraction using a particular class of lattices. On the side of the theory, local Cartesian abstraction formulation does not immediately provide a basis for complexity analysis, since the concrete domain (which is both the domain and the range of local Cartesian abstraction) admits exponentially long chains. Since local Cartesian abstraction is “the what” of Flanagan-Qadeer algorithm, we obtain a polynomial time algorithm for reachability under local Cartesian abstraction. To our best knowledge, this work is the first attempt to develop the theory of Cartesian abstraction for multithreaded programs.

Outline of the paper: First we define our program model. Then we explain the algorithm. We provide a small example. After that we define a concrete and an abstract domain and a corresponding Galois-connection that involve Cartesian products of sets. We state our first theorem saying how the output of the Flanagan-Qadeer algorithm is expressible in the standard framework of abstract interpretation. We prove this theorem. Then we define local Cartesian abstraction of multithreaded programs. We state our second theorem which says that the algorithm implements local Cartesian abstraction: the output of the algorithm represents local Cartesian abstraction of the program. We demonstrate the theorem on our example and prove it in general. After that, we give a boundary of the abstraction, i.e. a modification with a minimal precision increase that immediately breaks the polynomial-time border of the Flanagan-Qadeer algorithm. At last we look at the boundary, find two different sources of precision loss of the original algorithm and show them on examples. Then we describe the relaxed frontier search and quadratic thread-modular algorithms that overcome these sources of precision loss. We provide examples and discuss possible improvements based on the Cartesian abstraction approach. We conclude by summarizing the work.

2 Preliminaries

2.1 Programs with Threads

We are interested in proving safety properties of multithreaded programs. Each safety property can be encoded as a reachability property.

For simplicity we consider programs consisting of only two threads (the general case can be readily devised). A two-threaded program is given by a tuple

(Glob, Loc_{1}, Loc_{2}, →_{1}, →_{2}, init)

where

– Loc_{1} and Loc_{2} contain valuations of local variables of the first and second threads, we call them the local stores of the first and second thread, respectively;

– Glob contains valuations of shared variables, we call it the global store;

– the elements of States = Glob × Loc_{1} × Loc_{2} are called program states, the elements of Q_{1} = Glob×Loc_{1} and Q_{2} = Glob×Loc_{2} are called thread states;

– the relation →_{1} (resp. →_{2}) is a binary transition relation on the states of the first (resp. second) thread;

– init ⊆ States is a set of initial states. The program is equipped with the usual interleaving semantics. This means that if a thread makes a step, then it may change its own local variables and the global variables but may not change the local variables of another thread; a step of the whole program is either a step of the first or a step of the second thread. Now we define the successor operation that maps a set of program states to the set of their successors:

post : 2^{States} → 2^{States}
S ↦ {(g′, l′_{1}, l′_{2}) | ∃ (g, l_{1}, l_{2}) ∈ S :
(g, l_{1}) →_{1} (g′, l′_{1}) and l_{2} = l′_{2}
or (g, l_{2}) →_{2} (g′, l′_{2}) and l_{1} = l′_{1}} .

We are interested whether there is a computation of any length k ≥ 0 that starts in an initial state and ends in a single user-given error state f, formally:

∃ k ≥ 0 : f ∈ post^{k}(init) .

2.2 Flanagan-Qadeer Algorithm

The algorithm of Flanagan and Qadeer from [5] tests whether a given bad state f is reachable from an initial state. The test says “no” or “don’t know”. The algorithm computes sets R_{i} ⊆ Glob × Loc_{i} and G_{i} ⊆ Glob × Glob (i = 1, 2) defined by the least fixed point of the following inference rules:

INIT \overline{init_{i} ∈ R_{i}}  STEP \frac{(g, l) ∈ R_{i}  (g, l) →_{i} (g′, l′)}{(g′, l′) ∈ R_{i}  (g, g′) ∈ G_{i}}

ENV \frac{(g, l) ∈ R_{i}  (g, g′) ∈ G_{j}}{(g′, l) ∈ R_{i}} i ≠ j

Here, init_{1} = {(g, l_{1}) | (g, l_{1}, ) ∈ init}, similarly init_{2} = {(g, l_{2}) | (g, , l_{2}) ∈ init}. (The underscore means “anything”, i.e. an existentially quantified variable. The quantification is innermost, so in a formula, two underscores at different places denote different existentially quantified variables.) If f ∈ {(g, l_{1}, l_{2}) | (g, l_{1}) ∈ R_{1} and (g, l_{2}) ∈ R_{2}}, the algorithm says ”don’t know”, otherwise it says “no”. The rules work as follows. The STEP rule discovers successors of a state of a thread that result due to a step of the same thread. Further, it stores the information about how the step changed the globals in the sets G_{i}. The ENV rule uses this information to discover successors of a state of a thread that result due to communication between threads via globals. After the fixed point is reached, the set R_{1} (resp. R_{2}) contains those states of the first (resp. second) thread that the algorithm discovers. The discovered thread states contain those thread states that occur in computations.

3 Represented program states

The inference rules of the Flanagan-Qadeer algorithm define the sets R_{1}, R_{2} of “discovered” thread states. These sets represent those program states, whose globals and locals of the first thread are in R_{1} and globals and locals of the second thread are in R_{2}:

{(g, l_{1}, l_{2}) | (g, l_{1}) ∈ R_{1} and (g, l_{2}) ∈ R_{2}} .

Here is a small example. The program below has one global variable g that can take values 0 or 1, the first (resp. second) thread has a single local variable pc_{1} (resp. pc_{2}), representing the program counter.

Initially g = 0

A : g := 0;  C : g := 1;
B :  D :

The algorithm discovers the following thread states:

R_{1} = {(0, A), (0, B), (1, A), (1, B)}
R_{2} = {(0, C), (0, D), (1, D)}

where the pair (0, A), for instance, is a shorthand for the pair of two maps ([g ↦ 0], [pc_{1} ↦ A]). These two sets represent the set of program states

{(g, l_{1}, l_{2}) | (g, l_{1}) ∈ R_{1} and (g, l_{2}) ∈ R_{2}} =
{(0, A, C), (0, A, D), (0, B, C), (0, B, D), (1, A, D), (1, B, D)},

where the triple (0, A, C), for instance, is a shorthand for the triple of maps ([g ↦ 0], [pc_{1} ↦ A], [pc_{2} ↦ C]).

4 Cartesian Abstract Interpretation

In order to characterize the Flanagan-Qadeer algorithm in the abstract interpretation framework, we first need a concrete domain, an abstract domain and a Galois connection between them:

D = 2^{States} is the set underlying the concrete lattice, D^{#} = 2^{Q_{1}} × 2^{Q_{2}} is the set underlying the abstract lattice,

α_{cart} : D → D^{#}, S ↦ (T_{1}, T_{2}) where
T_{1} = {(g, l) | (g, l, ) ∈ S}
T_{2} = {(g, l) | (g, , l) ∈ S},

\begin{aligned}γ_{cart} : & D^{#} → D, \\ & (T_{1}, T_{2}) ↦ \{(g, l_{1}, l_{2}) | (g, l_{1}) ∈ T_{1} and (g, l_{2}) ∈ T_{2}\}. \end{aligned}

The ordering on the concrete lattice D is inclusion, the least upper bound is the union ∪, the greatest lower bound is the intersection ∩. The ordering on the abstract lattice D^{#} is the product ordering, i.e. (T_{1}, T_{2}) ⊑ (T′_{1}, T′_{2}) if and only if T_{1} ⊆ T′_{1} and T_{2} ⊆ T′_{2}. The least upper bound ⊔ is componentwise union, the greatest lower bound ⊓ is componentwise intersection.

Remark that if a pair of sets (T_{1}, T_{2}) is in the image of α_{cart}, then if some global part g ∈ Glob occurs in a thread state of one set (say, T_{1}), then g also occurs in a thread state of another set (i.e. T_{2}). So the image of the abstraction map α_{cart} is always contained in

D^{#+} = {(T_{1}, T_{2}) ∈ D^{#} | ∀ g ∈ Glob : (g, ) ∈ T_{1} ⇔ (g, ) ∈ T_{2}} .

Now we show that for the finite-state case both the cardinality and the maximal chain length of the abstract domain are in general smaller than that of the concrete domain.

Proposition 1. Let Glob, Loc_{1}, Loc_{2} be finite. Let G := |Glob| ≥ 1 be the cardinality of the global store and L_{1} := |Loc_{1}|, L_{2} := |Loc_{2}| be the cardinalities of the local stores, both at least 2 and l := min{L_{1}, L_{2}}, L := max{L_{1}, L_{2}}. Then the size and the maximal chain length of abstract domain are smaller and also asymptotically smaller than the size and the maximal chain length of the concrete domain. Formally:

a) |D^{#}| ≤ |D|;

b) lim_{L→∞} \frac{|D^{#}|}{|D|} = 0 ;

c) (maximal chain length of D^{#}) ≤ (maximal chain length of D) ;

d) lim_{l→∞} \frac{maximal chain length of D^{#}}{maximal chain length of D} = 0 .

Proof. a)
|D^{#}| = |2^{Glob×Loc_{1}} | |2^{Glob×Loc_{2}} | = 2^{GL_{1}}2^{GL_{2}} =
2^{G(L_{1}+L_{2})} ≤ 2^{GL_{1}L_{2}} = 2^{|States|} = |D| .

b)

\frac{|D^{#}|}{|D|} = \frac{|2^{Glob×Loc_{1}} | |2^{Glob×Loc_{2}} |}{2^{|States|}} = \frac{2^{GL_{1}}2^{GL_{2}}}{2^{GL_{1}L_{2}}} =

= (2^{G})^{L_{1}+L_{2}−L_{1}L_{2}} = (2^{−G})^{(L_{1}−1)(L_{2}−1)−1} ≤

≤ (2^{−G})^{(L−1)(2−1)−1} = 2^{−G(L−2)} ⟶^{L→∞} 0 .

c) A longest chain in the concrete domain D = 2^{Glob×Loc_{1}×Loc_{2}} has 1 + |Glob × Loc_{1} × Loc_{2}| = 1 + GL_{1}L_{2} elements, its minimum is the empty set ∅ and its maximum is States. Here is a longest chain in the abstract domain:

(∅, ∅) ⊏ ... ⊏ (Q_{1}, ∅) ⊏ ... ⊏ (Q_{1}, Q_{2}) ,

where first the elements of Q_{1} are added to the first component in some order one by one and then the elements of Q_{2}. This chain has 1 + |Q_{1}| + |Q_{2}| = 1 + G(L_{1} + L_{2}) elements, which is smaller than the maximal chain length in the concrete domain. Assume some other longest chain in the concrete domain is given. Then for each two adjacent elements (A_{1}, A_{2}) ⊏ (B_{1}, B_{2}) of the chain we have that either A_{1} = B_{1} and A_{2} ._{∪} { } = B_{2} or A_{2} = B_{2} and A_{1} ._{∪} { } = B_{1} (otherwise the chain could be made longer). So one can construct the chain by starting with (∅, ∅) and adding elements one by one in some order to the first or to the second component. The number of such additions is bounded by the sizes of the components, namely, by |Q_{1}| and |Q_{2}|. So totally |Q_{1}| + |Q_{2}| additions can be performed. The number of elements in the chain is thus also |Q_{1}| + |Q_{2}| + 1.

d)

lim_{l→∞} \frac{maximal chain length of D^{#}}{maximal chain length of D} = lim_{l→∞} \frac{1 + G(L_{1} + L_{2})}{1 + GL_{1}L_{2}} =

\underbrace{lim_{l→∞} \frac{1}{1 + GL_{1}L_{2}}}_{0} + lim_{l→∞} \frac{G(L_{1} + L_{2})}{1 + GL_{1}L_{2}} = lim_{l→∞} \frac{1}{\frac{1}{GL_{1}} + L_{2}} + lim_{l→∞} \frac{1}{\frac{1}{GL_{2}} + L_{1}} = 0 .

⊓ ⊔

Two remarks should be made. First, if only one local store grows but the other remains constant-size, then the quotient \frac{maximal chain length of D^{#}}{maximal chain length of D} approaches some small positive value between 0 and 1. In case the number of threads is not two, but variable (say, n), we get similar asymptotic results for n → ∞.

From now on, we sometimes omit the parentheses around the argument of a map, writing, e.g. fx for f(x).

Proposition 2. The pair of maps (α_{cart}, γ_{cart}) is a Galois connection, i.e. for all S ∈ D, (T_{1}, T_{2}) ∈ D^{#} holds

α_{cart}S ⊑ (T_{1}, T_{2}) iff S ⊆ γ_{cart}(T_{1}, T_{2}) .

Proof. “⇒”: Let (g, l_{1}, l_{2}) ∈ S. Let (T′_{1}, T′_{2}) = α_{cart}S. Then by definition of α_{cart} we have (g, l_{1}) ∈ T′_{1} ⊆ T_{1} and (g, l_{2}) ∈ T′_{2} ⊆ T_{2}. So (g, l_{1}, l_{2}) ∈ γ_{cart}(T_{1}, T_{2}) by definition of γ_{cart}. “⇐”: Let (T′_{1}, T′_{2}) = α_{cart}S. Let (g, l_{1}) ∈ T′_{1}. By definition of α_{cart} there is an l_{2} with (g, l_{1}, l_{2}) ∈ S ⊆ γ_{cart}(T_{1}, T_{2}). By definition of γ_{cart} we have (g, l_{1}) ∈ T_{1}. So T′_{1} ⊆ T_{1}. Analogously we get T′_{2} ⊆ T_{2}. ⊓ ⊔

Other definitions of Galois connection in the literature require that the abstraction and concretization maps are monotonic. However, this follows from our definition of Galois connection; the proof is left as an exercise for the reader.

5 Flanagan-Qadeer Algorithm as Cartesian Abstract Fixpoint Checking

5.1 Theorem and Example

We know (e.g. from [2]) that if the abstraction and concretization maps are given by a Galois connection (α, γ) between an abstract and a concrete domain, then the abstraction of the program is usually defined as the least fixed point of λT.α(init ∪ postγT). Recall that the Flanagan-Qadeer algorithm computes R_{1} and R_{2}, the sets of “discovered” states of the first and second thread.

Theorem 3. [Thread-Modular Model Checking is Cartesian Abstract Interpretation] The output of the Flanagan-Qadeer algorithm is the least fixed point of the abstract fixpoint checking operator with the abstraction map α_{cart} and concretization map γ_{cart}. Formally:

(R_{1}, R_{2}) = lfp λT. α_{cart}(init ∪ postγ_{cart}T) .

It is not clear why this is so and how the assumptions are connected. For our tiny example, the right hand of the above equation (i.e. the least fixed point) is

({(0, A), (0, B), (1, A), (1, B)}, {(0, C), (0, D), (1, D)}) ,

which coincides with (R_{1}, R_{2}) computed by the algorithm. We prove that the left and right hand side always coincide in the next section.

5.2 Proof

First we transform the inference rules of the Flanagan-Qadeer algorithm by getting rid of the sets G_{1} and G_{2}. We get an equivalent system of inference rules

INIT′_{1} \overline{init_{1} ∈ R_{1}}  STEP′_{1} \frac{(g, l) ∈ R_{1}  (g, l) →_{1} (g′, l′)}{(g′, l′) ∈ R_{1}}
ENV′_{1} \frac{(g, l) ∈ R_{1}  (g, l_{2}) ∈ R_{2}  (g, l_{2}) →_{2} (g′, )}{(g′, l) ∈ R_{1}}

The rules INIT′_{2}, STEP′_{2} and ENV′_{2} are analogous to INIT′_{1}, STEP′_{1} and ENV′_{1} where the indices 1 and 2 are exchanged. Remark that init_{1} and init_{2} contain thread states with the same global parts. Also remark that whenever (g, l) ∈ R_{1} and (g, l) →_{1} (g′, ) and there is some thread state (g, ) in R_{2}, then both rules STEP′_{1} and ENV′_{2} apply, giving two thread states for R_{1} and R_{2} with the same global part g′. Similarly, whenever (g, l) ∈ R_{2} and (g, l) →_{2} (g′, ) and there is some thread state (g, ) in R_{1}, then both rules STEP′_{2} and ENV′_{1} apply, giving two thread states for R_{2} and R_{1} with the same global part g′. By induction follows that whenever there is a thread state in R_{i} with some global part g, there is a thread state in R_{j} with the same global part g (i ≠ j). This means that we can combine the STEP’ and ENV’ rules into one rule. The following system of inference rules defines the same sets R_{1}, R_{2} as the system above:

INIT′_{1} \overline{init_{1} ∈ R_{1}} INIT′_{2} \overline{init_{2} ∈ R_{2}}
POST_{1}^{#} \frac{(g, l_{1}) ∈ R_{1}  (g, l_{2}) ∈ R_{2}  (g, l_{2}) →_{2} (g′, l′_{2})}{(g′, l_{1}) ∈ R_{1}  (g′, l′_{2}) ∈ R_{2}}
POST_{2}^{#} \frac{(g, l_{2}) ∈ R_{2}  (g, l_{1}) ∈ R_{1}  (g, l_{1}) →_{1} (g′, l′_{1})}{(g′, l_{2}) ∈ R_{2}  (g′, l′_{1}) ∈ R_{1}}

Each POST^{#} rule takes two sets (called R_{1} and R_{2} above) and gives new elements for the first and new elements for the second set. All possible applications of the POST^{#} rules on any fixed pair of sets (T_{1}, T_{2}) can be expressed as computing

p^{#}(T_{1}, T_{2}) = {((g′, l′_{1}), (g′, l′_{2})) | ∃ ((g, l_{1}), (g, l_{2})) ∈ T_{1} × T_{2} :
(g, l_{1}) →_{1} (g′, l′_{1}) and l_{2} = l′_{2}
or (g, l_{2}) →_{2} (g′, l′_{2}) and l_{1} = l′_{1}},

the new elements being the first and second projection of the result. Thus, applying the POST^{#} rules corresponds to computing

post^{#}(T_{1}, T_{2}) := (π_{1}p^{#}(T_{1}, T_{2}), π_{2}p^{#}(T_{1}, T_{2})) ,

i.e. applying the map

λ(T_{1}, T_{2}) . post^{#}(T_{1}, T_{2}) .

Remark that (init_{1}, init_{2}) = α_{cart}init. Then the pair of computed sets (R_{1}, R_{2}) is the least fixed point of

λT . α_{cart}init ⊔ post^{#}T .

It is interesting to see that post^{#} can be expressed in terms of post and the abstraction/concretization maps:

Proposition 4. For any T ∈ D^{#} holds:

post^{#}T = α_{cart}postγ_{cart}T .

Proof. Let (T_{1}, T_{2}) := T. “⊑”: Let (g′, l′_{1}) ∈ π_{1}p^{#}T. Then there is an l′_{2} so that the pair ((g′, l′_{1}), (g′, l′_{2})) ∈ p^{#}T. Then there are g, l_{1}, l_{2} with (g, l_{1}) ∈ T_{1}, (g, l_{2}) ∈ T_{2} and

(g, l_{1}) →_{1} (g′, l′_{1}) and l_{2} = l′_{2}
or (g, l_{2}) →_{2} (g′, l′_{2}) and l_{1} = l′_{1} .

Then (g, l_{1}, l_{2}) ∈ γ_{cart}(T_{1}, T_{2}) = γ_{cart}T by definition of γ_{cart}. So (g′, l′_{1}, l′_{2}) ∈ postγ_{cart}T by definition of the successor map post and thus (g′, l′_{1}) is in the first component of α_{cart}postγ_{cart}T. So π_{1}p^{#}T is included in the first component of α_{cart}postγ_{cart}T. Analogously follows that π_{2}p^{#}T is included in the second component of α_{cart}postγ_{cart}T. “⊒”: Let (g′, l′_{1}) be in the first component of α_{cart}postγ_{cart}T. Then there is an l′_{2} with (g′, l′_{1}, l′_{2}) ∈ postγ_{cart}T. So there are g, l_{1}, l_{2} with (g, l_{1}, l_{2}) ∈ γ_{cart}T and

(g, l_{1}) →_{1} (g′, l′_{1}) and l_{2} = l′_{2}
or (g, l_{2}) →_{2} (g′, l′_{2}) and l_{1} = l′_{1} .

From (g, l_{1}, l_{2}) ∈ γ_{cart}T we know that (g, l_{1}) ∈ T_{1} and (g, l_{2}) ∈ T_{2}. By definition of p^{#} we have ((g′, l′_{1}), (g′, l′_{2})) ∈ p^{#}(T_{1}, T_{2}). So (g′, l′_{1}) ∈ π_{1}p^{#}T. We have shown that the first component of α_{cart}postγ_{cart}T is included in π_{1}p^{#}T, which is the first component of post^{#}T. Analogously one can show that the second component of α_{cart}postγ_{cart}T is included in π_{2}p^{#}T, which is the second component of post^{#}T.

⊓ ⊔

So the algorithm computes the least fixed point of

λT . α_{cart}init ⊔ α_{cart}postγ_{cart}T
= λT . α_{cart}(init ∪ postγ_{cart}T) .

So

(R_{1}, R_{2}) = lfp λT. α_{cart}(init ∪ postγ_{cart}T) .

6 Local Cartesian Abstraction

Up to now we identified the Flanagan-Qadeer model-checking as abstract fixpoint checking on an abstract domain. However, it turns out that the output of the Flanagan-Qadeer algorithm can also be characterized by a very simple abstraction of multithreaded programs which is defined on the concrete domain. Now we define this abstraction. First recall that the Cartesian abstraction of a set of pairs is the smallest Cartesian product containing this subset. We define it formally as

C^{#} : 2^{X_{1}×X_{2}} → 2^{X_{1}×X_{2}},
P ↦ {(s_{1}, s_{2}) | (s_{1}, ) ∈ P and ( , s_{2}) ∈ P } ,

where X_{1} and X_{2} are any sets (e.g. Q_{1} and Q_{2}). We have C^{#}P = π_{1}P × π_{2}P. An analog of Cartesian abstraction on the concrete domain D = 2^{States} is

C : D → D
S ↦ {(g, l_{1}, l_{2}) | (g, l_{1}, ) ∈ S and (g, , l_{2}) ∈ S} .

We call this map local Cartesian abstraction of a set of program states since it simplifies to the Cartesian abstraction of a set of pairs if Glob is a singleton. It turns out that local Cartesian abstraction is representable in the abstract interpretation framework.

Proposition 5. Local Cartesian abstraction is approximation with the abstraction map α_{cart} and the concretization map γ_{cart}. Formally:

C = γ_{cart}α_{cart}

Proof. Let S ⊆ States. We have to show CS = γ_{cart}α_{cart}S. Let (T_{1}, T_{2}) = α_{cart}S. We have (g, l_{1}, l_{2}) ∈ CS iff [definition of C] (g, l_{1}, ) ∈ S and (g, , l_{2}) ∈ S iff [definition of α_{cart}] (g, l_{1}) ∈ T_{1} and (g, l_{2}) ∈ T_{2} iff [definition of γ_{cart}] (g, l_{1}, l_{2}) ∈ γ_{cart}(T_{1}, T_{2}) = γ_{cart}α_{cart}S. ⊓ ⊔

7 Thread-Modular Model-Checking as Local Cartesian Abstraction

7.1 Theorem and Example

Given an abstraction map α and a concretization map γ between an abstract and a concrete domain, we can alternatively perform the abstract fixed point checking in the concrete domain (in contradiction to the computation in the abstract domain as before). Then the least fixed point of λS.γα(init ∪ postS) is computed. For our special Galois connection (α_{cart}, γ_{cart}) this means the following. We can enumerate the states of the program by iterative successor computation and at each step overapproximate by local Cartesian abstraction. Naively implemented, this algorithm would require exponential time (in number of threads, if it is not constant). However, it turns out that the Flanagan-Qadeer algorithm solves the same problem in polynomial time.

Theorem 6. [Thread-Modular Model-Checking as Local Cartesian abstraction] The concretization of the output of the Flanagan-Qadeer algorithm is equal to the result of abstract fixpoint checking with local Cartesian abstraction. Formally:

γ(R_{1}, R_{2}) = lfp λS. C(init ∪ postS).  (1)

For our tiny example, let us compute the least fixed point of λS.C(init ∪ postS) by definition. The corresponding chain is

{(0, A, C)}
⊏ {(0, A, C), (0, B, C), (1, A, D)}

⊏ {(0, A, C), (0, B, C), (1, A, D), (1, B, D), (0, B, D), (0, A, D)} (fixed point) ,

the last term being the right hand side of (1). The left and the right hand side coincide in this example. Now we prove that they always coincide.

7.2 Proof Preparations

Before we start proving the theorem, let us prove a basic fact about the abstract fixpoint checking. Let D be a complete lattice with ordering ⊆, bottom element ∅, join ∪, meet ∩ (concrete lattice). Further, let D^{#} be a complete lattice with ordering ⊑, bottom element ⊥, join ⊔ and meet ⊓ (abstract lattice). Let a pair of maps α : D → D^{#} and γ : D^{#} → D be a Galois connection between the concrete and abstract lattices, i.e. for all concrete elements x ∈ D and all abstract elements y ∈ D^{#} we have αx ⊆ y iff x ⊑ γy. Let F : D → D be any monotone map and init ∈ D any concrete element. Further, we call ρ := γα : D → D the overapproximation operator. (Compare these standard definitions to the original Cousots’ work [4].) One way to perform abstract fixpoint checking is to compute the least fixed point of G^{#} = λT. α(init ∪ F γT) in the abstract lattice. The other way is to compute the least fixed point of G = λS. γα(init ∪ F S) in the concrete lattice. One would expect that these two fixed points are the same up to abstraction/concretization. Now we show that this is indeed the case under a special assumption about the concretization map γ.

Hypothesis: The concretization map γ is semi-continuous, i.e. for all ascending chains X ⊆ D^{#} we have γ(⊔X) = ∪γX. This hypothesis is especially satisfied for a continuous γ, i.e. when for all chains X ⊆ D^{#} we have γ(⊔X) = ∪γX.

Let μ be any ordinal that is strictly greater than the cardinalities of D and D^{#}. Let us define two sequences with indices from μ:

For k = 0 :  T^{0} = αinit  S^{0} = ρ init ,
for successor ordinals k + 1 ∈ μ : T^{k+1} = G^{#}T^{k}  S^{k+1} = GS^{k} ,
for limit ordinals k ∈ μ :  T^{k} = ⨆_{k′<k} T^{k′} S^{k} = ⋃_{k′<k} S^{k′} .

From [3] Cor. 3.3 we know that the sequences (S^{k})_{k}, (T^{k})_{k} are stationary increasing chains and the limits are the least fixed points over αinit and ρ init, respectively. One can show that if we start the sequences (T^{k})_{k} and (S^{k})_{k} with the bottom elements ⊥ and ∅ (instead of αinit and ρ init), the limits would be the same, so the limits are the least fixed points (over ⊥ and ∅). The hypothesis immediately implies that for each limit ordinal k ∈ μ holds

γ ⨆_{k′<k} T^{k′} = ⋃_{k′<k} γT^{k′} and γ ⨆_{k′<k} αS^{k′} = ⋃_{k′<k} γαS^{k′} .  (2)

Using this formula we show step by step that the least fixed points of G and G^{#} coincide up to abstraction and concretization. We need some basic facts about Galois connections and about the overapproximation operator (see e.g. [1], [4]). From the definition of Galois connection one can prove that the abstraction and concretization maps α and γ are monotone. Further overapproximation map ρ is idempotent. Further, overapproximating and then abstracting is the same as abstracting: αρ = α (since γα is extensive, αγ reductive and both are monotone). First we show that overapproximating S^{k} doesn’t change it.

Proposition 7. Each S^{k} is invariant under overapproximation. Formally:

∀ k ∈ μ : ρS^{k} = S^{k} .

Proof. We use transfinite induction. For k = 0, we have ρS^{0} = ρρ init =^{ρ idempotent} ρ init = S^{0}. For a successor ordinal k + 1, we have ρS^{k+1} = ρρ(init ∪ F S^{k}) =^{ρ idempotent} ρ(init ∪ F S^{k}) = S^{k+1}. If k is a limit ordinal, then ρS^{k} = γα ⋃_{k′<k} S^{k′} =^{α complete join morphism} γ ⨆_{k′<k} αS^{k′}

=^{formula(2)} ⋃_{k′<k} γαS^{k′} =^{ρ=γα} ⋃_{k′<k} ρS^{k′} =^{induction assumption} ⋃_{k′<k} S^{k′} = S^{k}.

⊓ ⊔

Proposition 8. Each T^{k} is the abstraction of S^{k}. Formally:

∀ k ∈ μ : T^{k} = αS^{k} .

Proof. Transfinite induction. For k = 0 we have T^{0} = αinit =^{α=αρ} αρinit = αS^{0}. For a successor ordinal k + 1 we have T^{k+1} = α(init ∪ F γT^{k}) =^{induction assumption}

α(init∪F γαS^{k}) =^{γα=ρ} α(init∪F ρS^{k}) =^{ρS^{k}=S^{k}} α(init∪F S^{k}) =^{α=αρ} αρ(init∪F S^{k}) =

αS^{k+1}. If k is a limit ordinal, then T^{k} = ⨆_{k′<k} T^{k′} =^{induction assumption} ⨆_{k′<k} αS^{k′}

=^{α complete join morphism} α ⋃_{k′<k} S^{k′} = αS^{k}. ⊓ ⊔

Proposition 9. Each S^{k} is the concretization of T^{k}. Formally:

∀ k ∈ μ : γT^{k} = S^{k} .

Proof. Transfinite induction. For k = 0 we have γT^{0} = γαinit = ρinit = S^{0}.

For a successor ordinal k + 1 we have γT^{k+1} = γα(init ∪ F γT^{k}) = ρ(init ∪ F γT^{k}) =^{induction assumption} ρ(init ∪ F S^{k}) = S^{k+1}.

If k is a limit ordinal, γT^{k} = γ ⨆_{k′<k} T^{k′} =^{formula(2)} ⋃_{k′<k} γT^{k′} =^{induction assumption} ⋃_{k′<k} S^{k′} = S^{k}.

⊓ ⊔

Let λ ∈ μ be any ordinal at which both sequences are stationary, i.e. S^{λ} = S^{λ+1} and T^{λ} = T^{λ+1}. Then the least fixed point of G is S^{λ} and the least fixed point of G^{#} is T^{λ}. Propositions 8 and 9 imply the following

Theorem 10. The least fixed points of G and G^{#} coincide up to abstraction and concretization:

γ lfp G^{#} = lfp G and lfp G^{#} = α lfp G .

7.3 Proof conclusion and remarks

We now show that for our Galois connection (α_{cart}, γ_{cart}) between our domains D and D^{#} the hypothesis holds.

Proposition 11. γ_{cart} is continuous, i.e. for all chains X ⊆ D^{#} holds:

γ_{cart}(⊔X) = ∪ γ_{cart}X .

Proof. “⊆”. Let (g, l_{1}, l_{2}) ∈ γ_{cart}(⊔X). Then (g, l_{1}) (resp. (g, l_{2})) is in the first (resp. second) component of ⊔X. Then there are (T_{1}, T_{2}) and (T′_{1}, T′_{2}) in X with (g, l_{1}) ∈ T_{1} and (g, l_{2}) ∈ T′_{2}. Since X is a chain, we have either (T_{1}, T_{2}) ⊒ (T′_{1}, T′_{2}) or (T_{1}, T_{2}) ⊑ (T′_{1}, T′_{2}). Without loss of generality let (T_{1}, T_{2}) ⊒ (T′_{1}, T′_{2}). Then (g, l_{2}) ∈ T_{2}, so (g, l_{1}, l_{2}) ∈ γ_{cart}(T_{1}, T_{2}) ⊆ ∪γ_{cart}X. “⊇” holds by monotonicity of γ_{cart} and definition of the least upper bound. ⊓ ⊔

The map post : D → D is monotone. Proposition 5 and Theorems 3 and 10 imply

γ(R_{1}, R_{2}) = lfp λS. C(init ∪ postS) ,

which concludes the proof of Theorem 6.

The whole proof is very general and would get shorter for the finite-state case. The current proof depends only on the fact that the concretization map is semicontinuous. It depends neither on the exact structure of the abstract and the concrete lattices, nor on the exact definition of the abstraction/concretization maps, nor on the structure of the monotone map F. In applications of the abstract interpretation framework, the concretization map is often semi-continuous, so that Theorem 10 can be reused.

8 Precision vs. Runtime

For speaking about runtime, assume that all the domains are finite. The definitions of the abstract and concrete domains as well as the corresponding Galois connection and the resulting local Cartesian abstraction extend to n threads in the natural way: States = Glob × ∏_{i=1}^{n} Loc_{i}, D = 2^{States}, D^{#} = ∏_{i=1}^{n} Glob × Loc_{i}, (T_{1}, ..., T_{n}) ⊑ (T′_{1}, ..., T′_{n}) iff for all 1 ≤ i ≤ n holds T_{i} ⊆ T′_{i},

α_{cart} : D → D^{#}, S ↦ (T_{1}, ...T_{n}) where
T_{i} = π_{Glob×Loc_{i}}S (i = 1, ..., n),

\begin{aligned}γ_{cart} : & D^{#} → D, \\ & (T_{1}, ..., T_{n}) ↦ \{(g, l_{1}, ..., l_{n}) | ∀i : (g, l_{i}) ∈ T_{i}\}, \end{aligned}

C = γ_{cart}α_{cart}, post^{#} = α_{cart}postγ_{cart},

where π_{Glob×Loc_{i}} is the projection map onto the component Glob × Loc_{i}. The previous results formulated for n = 2 also hold for all numbers of threads

n ≥ 2.

8.1 Boundary of the Flanagan and Qadeer algorithm

Now we try to push the Flanagan-Qadeer algorithm to increase precision without losing polynomial complexity.

A usual way to change a search algorithm is to use “frontier search”, which forgets the nodes of the search graph that were expanded in the past. The idea is to apply local Cartesian abstraction not to all of the discovered states, but only to the latest discovered states:

T^{0} = α_{cart}init and T^{i+1} = post^{#}T^{i} (i ≥ 0).

The sequence stops when γ_{cart}T^{k+1} ⊆ ∪_{i=0}^{k}γ_{cart}T^{i}. For this k we can show that X := ∪_{i=0}^{k}γ_{cart}T^{i} is an inductive invariant, i.e. init ⊆ X and postX ⊆ X. We can implement this iteration in the abstract domain D^{#} as follows. Consider following inference rule (i ≠ j):

POST_{ij}^{#} \frac{(g, l_{i}) ∈ R_{i}  (g, l_{j}) ∈ R_{j}  (g, l_{j}) →_{j} (g′, l′_{j})}{(g′, l_{i}) ∈ R′_{i}  (g′, l′_{j}) ∈ R′_{j}} .

Except for the primed versions R′_{i} and R′_{j} in the conclusion of the rule, this is the same rule that is used in the reformulation of the Flanagan-Qadeer algorithm. If T^{i} = (R_{1}, ..., R_{n}) is the ith element of the iteration sequence then T^{i+1} = (R′_{1}, ..., R′_{n}) is computed by the above rule. So each step of the new iteration scheme is polynomial. It turns out that frontier search breaks the polynomialtime boundary of the method:

Theorem 12. Frontier search with Cartesian abstraction has exponential worstcase runtime in the number of threads.

Proof. It suffices to give an example program on which the new algorithm needs exponential time in the number of threads n. However, even the Flanagan-Qadeer may have exponential runtime in n if the size of the global store is exponential in n. So we require that the size of the description of the program (the global store, the local stores, the transition relations of the threads and the initial state set) is polynomial in n. It suffices to present a family of multithreaded programs so that:

1. the nth program in the family has n threads;

2. the sizes of the global store and local stores are polynomial in n;

3. each program of the family has exactly one run which is exponentially long in n.

Assume such a program with a single initial state is given. If for some i ≥ 0 the components of the tuple T^{i} contain at most one element each, then γ_{cart}T^{i} contains at most one element, and hence postγ_{cart}T^{i} has at most one element, so T^{i+1} = α_{cart}postγ_{cart}T^{i} is a tuple of sets which are either all empty sets or all singletons. Since γ_{cart}T^{i} contains post^{i}(init), we inductively follow that γ_{cart}T^{i} = post^{i}(init) for all i ≥ 0, i.e. no approximation happens. Especially the sequence (T^{i})_{0≤i≤k} is exponentially long.

Now we give a family of programs satisfying the conditions above.

Example 13. Below you see a program with n threads whose single run has length at least 2^{n}. The size of the global store is n + 1, the local stores have two elements each. The statements in brackets <> are atomic.

Global boolean variable with initial value: t = 1 (takes values from {0, ..., n}) Thread 1:

0: wait until t = 1;
1: <t := 2;   goto 0;>

Thread i (1 < i < n):

0: <wait until t = i; t := 1;>
1: <wait until t = i; t := i + 1;   goto 0;>

Thread n:

0: <wait until t = n; t := 1;>
1: <wait until t = n; t := 0;   goto 0;>

The program implements a binary counter. The program performs repeated increment with the school addition method. The local store of the ith thread represents the position i − 1 of the number (1 ≤ i ≤ n). The carry position is stored in the global variable t. The value t = 0 means the carry is nowhere.

Below is the single run for n = 3 where pc_{i} is the program counter of the ith thread. Each column represents a state of the whole program, a successor state is to the right of its predecessor:

variable ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
t  1 1 2 1 1 2 3 1 1 2 1 1 2 3 0
pc_{1}  0 1 0 0 1 0 0 0 1 0 0 1 0 0 0
pc_{2}  0 0 0 1 1 1 0 0 0 0 1 1 1 0 0
pc_{3}  0 0 0 0 0 0 0 1 1 1 1 1 1 1 0

Let us consider the columns marked by the star (*), i.e the columns with t = 1 (the carry is above the 0th position). One sees that the values of the program counters (pc_{3}, pc_{2}, pc_{1}) evolve like a binary counter. The formal inductive proof that this program implements the binary counter is left as an exercise for the reader. ⊓ ⊔

So frontier search is the precision limit of Cartesian Abstraction.

Remark that the set of reachable states of binary counter in Example 13 is so big that the output of the Flanagan-Qadeer algorithm is exact:

R_{1} =  {(1, 0), (1, 1), (2, 0),  (3, 0),  (0, 0)} ,
R_{2} =  {(1, 0), (1, 1), (2, 0),(2, 1),  (3, 0),  (0, 0)} ,
R_{3} =  {(1, 0), (1, 1), (2, 0),(2, 1),  (3, 0),(3, 1),  (0, 0)} .

Namely, the concretization of the output γ_{cart}(R_{1}, R_{2}, R_{3}) gives exactly the set of reachable states. So this is also an example of when an attempt of regaining precision by frontier search doesn’t increase precision but requires exponential time.

The binary counter example has a property that the size of the global store grows linearly with the number of threads. Can one get states reachable only by exponentially long runs with a sublinear or even constant size of the global store? This would give an answer to the question whether exponentially long runs occur only due to the growing number of threads or need a growing global store. We pose the following

Problem 14. Prove or give a counterexample. There is no family (P_{n})_{n≥1} of multithreaded programs so that

1. the nth program P_{n} consists of n threads;

2. the sizes of the global and local stores are bounded by a constant (independent on n);

3. the diameter of the transition graph of the nth program P_{n} is asymptotically exponential in n, i.e. there is a constant c > 1 so that for almost all n ∈ ℕ the diameter of the transition graph of P_{n} exceeds c^{n}.

We do not see how to solve this problem at the moment.

8.2 Regaining precision

The inherent problem of the original Flanagan-Qadeer algorithm is that its abstraction is too coarse. We show two techniques that overcome precision loss and give practical polynomial-time algorithms based on it.

There are two sources of precision loss. One is that local Cartesian abstraction “forgets” temporal properties of the program. That means that a state of one thread that occurs late in any computation can be combined with a state of another thread that occurs early in any computation.

Example 15. In this example, the Flanagan-Qadeer algorithm cannot prove that the first thread never reaches label D: Global variable g=0

Thread 1:          Thread 2:
A: wait until g=1; E: g:=1;
B: wait until g=0; F: g:=0;
C: wait until g=1; G:

D:

The algorithm computes the sets

R_{1} ={(0, A), (0, B), (0, C), (0, D),
(1, A), (1, B), (1, C), (1, D)} ,
R_{2} ={(0, E), (0, G), (1, F)} .

Since ( , D) ∈ R_{1}, the label D is discovered.

The second source of precision loss is that local Cartesian abstraction “forgets” dependencies between threads even in successors of a single program state. For instance, the Flanagan-Qadeer algorithm is unable to prove mutual exctusion with locks (see example in [5]) of the following program.

Example 16. In the program below, execution never reaches the state pc_{1} = pc_{2} = B. Global variable m=0

Thread 1:           Thread 2:
A: <wait until m=0; A: <wait until m=0;
      m:=1;>  m:=1;>
B:                  B:

The algorithm computes the sets R_{1} = R_{2} = {(0, A), (1, A), (1, B)}, whose concretization γ_{cart}(R_{1}, R_{2}) contains (1, B, B), which violates mutual exclusion.

Now we give two techniques that solve the above problems while still being polynomial in time.

Relaxed Frontier Search. Frontier search is a boundary of the thread-modular method. It takes exponential time in the worst case. Our new method is a combination of the original Flanagan-Qadeer algorithm and the frontier search. It has polynomial runtime.

Definition 17 (Relaxed Frontier Sequence). Let the sequence (T^{i})_{i≥0} of elements of D^{#} be defined recursively by T^{0} = α_{cart}init,

T^{i+1} = \begin{cases}post^{#}T^{i} , if post^{#}T^{i} ⋢ ⊔_{j=0}^{i}T^{j}, \\ T^{i} ⊔ post^{#}T^{i} , if post^{#}T^{i} ⊑ ⊔_{j=0}^{i}T^{j}. \end{cases}

Let k = min{i | T^{i+1} ⊑ T^{i}}.

This (in general non-monotone) sequence is the basis of our algorithm, which needs only elements of the sequence up to position k. First we prove that k is well-defined, and is at most quadratic in the number of threads. Let G = |Glob| the size of the global store and L the maximal size of the local store, i.e. L = max_{i} |Loc_{i}|.

Proposition 18. The value k is well-defined and is at most nGL(nGL + 1) = O((nGL)^{2}).

Proof. First we prove that k is well-defined. The set D^{#} is finite, so the monotone sequence (⊔_{i=0}^{k′}T^{i})_{k′≥0} stabilizes for some k′ ≥ 0, i.e. T^{j} ⊑ ⊔_{i=0}^{k′}T^{i} for all j ≥ k′. Take the smallest such k′. For all j ≥ k′ we have T^{j+1} ⊒ post^{#}T^{j} and thus post^{#}T^{j} ⊑ ⊔_{i=0}^{k′}T^{i}. By definition of the algorithm, the sequence (T^{j})_{j≥k′} is monotonic increasing. The domain is finite, so there is a k ≥ k′ with T^{k+1} = T^{k}.

Now we derive the number of iteration steps. The set D^{#} has chains of length at most nGL + 1, so in the increasing sequence (⊔_{i=0}^{j}T^{i})_{j≥0} there are at most nGL positions with a strict increase. Let us take two such “neighbour” positions a < b with

⊔_{i=0}^{a−1}T^{i} ≠ ⊔_{i=0}^{a}T^{i} and ⊔_{i=0}^{b−1} T^{i} ≠ ⊔_{i=0}^{b}T^{i}

so that for all c with a < c < b we have

⊔_{i=0}^{c−1}T^{i} = ⊔_{i=0}^{c}T^{i} .

The sequence (T^{c})_{a≤c<b} is increasing by the definition of the relaxed frontier sequence. The maximal chain length gives b − a ≤ nGL + 1 and finally k − k′ ≤ nGL. Each of at most nGL positions with a strict increase in the sequence (⊔_{i=0}^{j}T^{i})_{j} can be followed by at most nGL positions with a strict increase of T^{j} before the next increase of ⊔_{i=0}^{j}T^{i} or termination. So the number of all increases is at most nGL(nGL + 1) = O((nGL)^{2}).

Now we show that the elements of the sequence up to position k represent a superset of states reachable from the initial ones.

Proposition 19. The set X := ∪_{i=0}^{k}γ_{cart}T^{i} is an inductive invariant, i.e.

init ⊆ X and postX ⊆ X .

Proof. Recall that γ_{cart}α_{cart} is extensive (i.e. for any S ∈ D we get S ⊆ γ_{cart}α_{cart}S). So the initial states are in X since init ⊆ γ_{cart}α_{cart}init = γ_{cart}T^{0} ⊆ X. Now let s ∈ postX. Since post distributes over union, there is an i with 0 ≤ i ≤ k so that s ∈ postγ_{cart}T^{i}. Since γ_{cart}α_{cart} is extensive, we get s ∈ γ_{cart}α_{cart}postγ_{cart}T^{i} = γ_{cart}post^{#}T^{i} ⊆ γ_{cart}T^{i+1} ⊆ ∪_{i=1}^{k+1}γ_{cart}T^{i}. Since T^{k+1} ⊑ T^{k}, we get γ_{cart}T^{k+1} ⊆ γ_{cart}T^{k} and thus s ∈ ∪_{i=1}^{k}γ_{cart}T^{i} ⊆ X.

An algorithm that implements relaxed frontier search in linear space in quadratic number of iterations is given below.

Algorithm 20 (Relaxed Frontier Search). The input is init (the initial states) and f (an error state). T := ⊥; T' := α_{cart}init;

AllT := T';
while (T' ⋢ T ∧ α_{cart}{f} ⋢ T') do
     T := T';
     P := post^{#}T;
     if P ⊑ AllT then T' := T ⊔ P; else T' := P;
     AllT := AllT ⊔ T';
od;
if α_{cart}{f} ⋢T' then print ``program safe''
else print ``don't know'';

The runtime is polynomial, since post^{#} can be computed by the Post_{ij}^{#} rule and the number of iterations is quadratic in the number of threads. The used space is dominated by the size of AllT, which can be stored in O(nGL) space, which is linear in the number of threads.

Now we look at the example 15 and show that the relaxed frontier search method is able to handle it. Below we derive the relaxed frontier sequence:

i elements of the  elements of the
first component of T^{i} second component of T^{i}
0 (0, A)  (0, E)
1 (1, A)  (1, F)
2 (1, B), (0, A)  (1, F), (0, G)
3 (0, B)  (0, G)
4 (0, C)  (0, G)

The elements after position k = 4 are all ((0, C), (0, G))

The thread states ( , D) are not in T^{i} for any i. In this special example, the computation was equivalent to that of the pure frontier search, since on each step a new thread state was discovered. This will be the case for linear loop-free programs.

For the binary counter example 13, the computed invariant is equal to that of the pure Flanagan-Qadeer method, since the latter contains exactly the reachable states. However, the number of iterations is greater.

Quadratic Thread-Modular Method Now we show a technique based on local Cartesian abstraction that is able to prove mutual exclusion in some of those cases where the original algorithm was too coarse. We overcome the inherent coarseness of the abstraction by walking along chains in the bigger lattice (D^{#})^{n} with product ordering. The longest chains in the new domain have length O(n^{2}GL). So the price we pay for proving mutual exclusion is squared complexity in comparison to the Flanagan-Qadeer algorithm.

Our algorithm maintains n^{2} sets R_{i}^{j} ⊆ Glob × Loc_{i} (1 ≤ i, j ≤ n). The sets are generated by the following rules.

QInit:

\overline{init_{i} ⊆ R_{i}^{j}}

QStep:

\frac{(g, l_{i}) ∈ R_{i}^{j}  (g, l_{i}) →_{i} (g′, l′_{i})  (g, l_{k}) ∈ R_{k}^{j}}{(g′, l′_{i}) ∈ R_{i}^{i}  (g′, l_{k}) ∈ R_{k}^{i}} i ≠ k

where init_{i} is the ith component of α_{cart}init. Let f be a user-given error state. If α_{cart}{f} ⊑ (R_{1}^{j}, ..., R_{n}^{j}) for some 1 ≤ j ≤ n, then the algorithm says “don’t know”, otherwise the answer is “the program is safe”.

Now we describe an intended meaning of the sets R_{i}^{j} (1 ≤ i, j ≤ n). Let us view all the discovered thread states as partitioned into n tuples, namely (R_{1}^{1}, ..., R_{n}^{1}), ..., (R_{1}^{n}, ..., R_{n}^{n}). Those thread states are added to the ith tuple which resulted due to a step of the ith thread. The QStep rule can be described informally as an iterative application of the following procedure:

- Take any tuple (R_{1}^{j}, ..., R_{n}^{j});

- Compute the successors that resulted due to a step of the ith thread;

- Add these successors to the ith tuple (R_{1}^{i}, ..., R_{n}^{i}).

It is unclear why these rules should be sound and give a preciser answer than the original Flanagan-Qadeer rules. First we show

Theorem 21. The set

X := ⋃_{j=1}^{n} γ_{cart}(R_{1}^{j}, ..., R_{n}^{j})

is an inductive invariant. Formally:

init ⊆ X and postX ⊆ X.

Proof. We have init ⊆ γ_{cart}α_{cart}init ⊆ γ_{cart}(R_{1}^{j}, ..., R_{n}^{j}) ⊆ X for any j, e.g. j = 1. Now take some program state (g′, l′_{1}, ..., l′_{n}) ∈ postX. We want to show that this state is in X. The successor operator post distributes over union, so there is an index j ∈ {1, ..., n} so that (g′, l′_{1}, ..., l′_{n}) ∈ postγ_{cart}(R_{1}^{j}, ..., R_{n}^{j}). By definition of the successor map there is a thread i ∈ {1, ..., n} which made a step from some state (g, l_{1}, ..., l_{n}) ∈ γ_{cart}(R_{1}^{j}, ..., R_{n}^{j}) so that (g, l_{i}) →_{i} (g′, l′_{i}) and for k ≠ i the other local parts remain the same, i.e. l_{k} = l′_{k} for k ≠ i. By definition of γ_{cart} for all k ∈ {1, ..., n} holds (g, l_{k}) ∈ R_{k}^{j}. Especially (g, l_{i}) ∈ R_{i}^{j}, so by the QStep rule we have (g′, l′_{i}) ∈ R_{i}^{i} and (g′, l′_{k}) = (g′, l_{k}) ∈ R_{k}^{i} for k ≠ i. So for all k ∈ {1, ..., n} we have (g′, l′_{k}) ∈ R_{k}^{i}. By definition of the concretization map (g′, l′_{1}, ..., l′_{n}) ∈ γ_{cart}(R_{1}^{i}, ..., R_{n}^{i}) ⊆ X.

Before proving that this method is at least as precise as the method of Flanagan-Qadeer, recall that the Flanagan-Qadeer system of inference rules is equivalent to the following:

Init:

\overline{init_{i} ⊆ R_{i}}

Post^{#}:

\frac{(g, l_{i}) ∈ R_{i}  (g, l_{i}) →_{i} (g′, l′_{i})  (g, l_{k}) ∈ R_{k}}{(g′, l′_{i}) ∈ R_{i}  (g′, l_{k}) ∈ R_{k}} i ≠ k.

Proposition 22. The quadratic thread-modular method is at least as precise as the Flanagan-Qadeer method. Especially, for all threads i ∈ {1, ..., n} holds

⋃_{j=1}^{n} R_{i}^{j} ⊆ R_{i} .

Proof. View the inference rules as rules that take the sets R_{i}^{j} (1 ≤ i, j ≤ n for the quadratic thread-modular method) and R_{i} (1 ≤ i ≤ n for the Flanagan-Qadeer method) in the premises and produce bigger sets R_{i}^{′j} resp. R′_{i} in the conclusion. We use structural induction. We assume that ∪_{j=1}^{n}R_{i}^{j} ⊆ R_{i} holds for the sets in the premises of the rules QInit and QStep and show that this statement holds after applying each rule, i.e. ∪_{j=1}^{n}R_{i}^{′j} ⊆ R′_{i} (1 ≤ i ≤ n). First consider the rule QInit. From R_{i}^{′j} = init_{i} ∪ R_{i}^{j} follows

⋃_{j=1}^{n} R_{i}^{′j} = init_{i} ∪ ⋃_{j=1}^{n} R_{i}^{j} ⊆ init_{i} ∪ R_{i} = R′_{i}.

Now consider the rule QStep. Let (g′, l′_{i}) ∈ R_{i}^{′i} for some i ∈ {1, ..., n}. If this element is in R_{i}^{i}, it is also in R_{i} by induction assumption. Otherwise it is added by the rule. Then there is a thread state (g, l_{i}) ∈ R_{i}^{j} for some j with (g, l_{i}) →_{i} (g′, l′_{i}). By induction assumption (g, l_{i}) ∈ R_{i} and by the Post^{#} rule (g′, l′_{i}) ∈ R′_{i}. So R_{i}^{′i} ⊆ R′_{i}. Now let (g′, l_{k}) ∈ R_{k}^{′i} for k ≠ i from {1, ..., n}. If (g′, l_{k}) is in R_{k}^{i}, it is also in R_{k} by induction assumption. Otherwise it is added by the rule. Then there is an index j ∈ {1, .., n} and a thread state (g, l_{i}) ∈ R_{i}^{j} with (g, l_{i}) →_{i} (g′, ) so that (g, l_{k}) ∈ R_{k}^{j}. By induction assumption (g, l_{i}) ∈ R_{i}, (g, l_{k}) ∈ R_{k} and by the Post^{#} rule (g′, l_{k}) ∈ R′_{k}. So R_{k}^{′i} ⊆ R′_{k}.

Now let us turn to the mutual exclusion example 16. Now we show a broader class of programs that can now be handled by the quadratic thread-modular method.

Example 23. For any n, consider a program that consists of a single global variable m with initial value 0 and n copies of the following thread:

A: <wait until m=0;
       m:=1;>
B: m:=0;

The quadratic thread-modular algorithm generates the following sets: R_{j}^{j} = {(0, A), (1, B), (0, C)} for j ∈ {1, ..., n}, R_{i}^{j} = {(0, A), (1, A), (0, C), (1, C)} for i ≠ j in {1, ..., n}.

For each j ∈ {1, ..., n}, only one set from R_{1}^{j}, ..., R_{n}^{j} contains a thread state ( , B), namely, (1, B) ∈ R_{j}^{j}. So the invariant ∪_{j=1}^{n}γ_{cart}(R_{1}^{j}, ..., R_{n}^{j}) contains only states with at most one thread in critical section at label B.

It is not immediately clear why mutual exclusion can be proven in the above example. If you look at the QStep rule, you see that whatever value the index j has, the rule puts the thread states that resulted due to a step of the thread i into the sets R_{i}^{i} and R_{k}^{i} (k ≠ i). So whenever a program enters the critical section of the thread i, the abstraction of the corresponding program state is in R_{1}^{i}, ..., R_{n}^{i}. Whenever another thread i′ enters its critical section, the abstraction of the corresponding program state goes into R_{1}^{i′}, ..., R_{n}^{i′}. The concretization of each tuple (R_{1}^{i}, ..., R_{n}^{i}) is done separately for each thread i (see Theorem 21), so states of one thread in its critical section are not mixed with states of another thread in its critical section.

An implementation of the quadratic thread-modular method needs O(n^{2}GL) space and polynomial time. The exact runtime depends on how the sets R_{i}^{j} and the transition relation are represented. One can consider implementing the rule QStep in the assume-guarantee style of the original algorithm by introducing auxiliary sets G_{i}^{j} ⊆ Glob^{2} that contain changes of the global variables induced by thread states in R_{i}^{j} (1 ≤ i, j ≤ n).

8.3 Devising new algorithms

The presented two techniques of relaxed frontier search and quadratic threadmodular method can be combined gaining even more precision while producing a polynomial-time algorithm. This is left as an exercise for the reader.

Now consider the lattice (D^{#})^{p(n)} with product ordering where p(n) is some polynomial. Its longest chains have p(n)nGL + 1 elements. Any algorithm that iteratively produces elements of an ascending chain would inevitably need polynomial number of iterations. It would be interesting to investigate the ability of proving results by walking along chains in these domains.

9 Summary

We have examined an approach for verifying concurrent programs. On the one hand, we have examined the Flanagan-Qadeer algorithm for checking safety of multithreaded programs. We have characterized it in a well-known framework of abstract interpretation. Using this characterization, we have shown the boundary of this algorithm. On the other hand, we have started developing the theory of Cartesian abstraction for multithreaded programs. We have shown two equivalent approaches for abstract fixpoint checking on the abstract and the concrete domain. We have seen that local Cartesian abstraction is polynomial in the number of threads. Using ideas from both points of view, we have devised two new polynomial-time algorithms based on Cartesian abstraction that substantially increase precision of the thread-modular method. These contributions seem to be first steps in a systematic study of similar abstractions of the state explosion problem.

10 Acknowledgements

We would like to thank anonymous reviewers for their constructive comments and suggestions.

References

1. Bruno Blanchet. Introduction to abstract interpretation, 2002. Lecture script,

http://bblanche.gitlabpages.inria.fr/absint.pdf.

2. Patrick Cousot. Partial completeness of abstract fixpoint checking. In Berthe Y. Choueiry and Toby Walsh, editors, SARA, volume 1864 of Lecture Notes in Computer Science, pages 1–25. Springer, 2000.

3. Patrick Cousot and Radhia Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Math., 82(1):43–57, 1979.

4. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In POPL, pages 269–282, 1979.

5. Cormac Flanagan and Shaz Qadeer. Thread-modular model checking. In Thomas Ball and Sriram K. Rajamani, editors, SPIN, volume 2648 of Lecture Notes in Computer Science, pages 213–224. Springer, 2003.

6. Thomas Anton Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In Warren A. Hunt Jr. and Fabio Somenzi, editors, CAV, volume 2725 of Lecture Notes in Computer Science, pages 262–274. Springer, 2003.

7. Gerard J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.

8. Dexter Kozen. Lower bounds for natural proof systems. In FOCS, pages 261–262. IEEE, 1977.

9. Patrick Maier. A framework for circular assume-guarantee reasoning, 2002. Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, research report MPI-I-2002-2-007.

10. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.

11. Zohar Manna and Amir Pnueli. Temporal verification of reactive systems: safety. Springer-Verlag, May 1995.