Thread-Modular Verification with Arbitrary Precision

Alexander Malkis^{1}, Andreas Podelski^{1}, and Andrey Rybalchenko^{2}

1 Albert-Ludwigs-Universität Freiburg 2 EPFL

Abstract. State explosion is the curse of concurrency. Thread-modular verification of multithreaded programs is a promising method that circumvents the state explosion. The method trades its polynomial complexity for a loss of precision that limits the verification power of the method. In this paper we show why this limit can be removed and how. Our work is based on the fact that thread-modular verification is abstract interpretation with Cartesian abstraction. We show that one can parameterize the abstraction and thus adapt the degree of precision to the specific verification problem. The parameterized thread-modular verification is still polynomial in the number of threads. We formalize our approach in the abstract interpretation framework, giving a sufficient condition under which a polynomial-time abstraction can be parameterized without loss of polynomial-time complexity.

1 Introduction

Verification of multithreaded software is known to be a hard problem (see e.g. [9]). The number of states of multithreaded programs grows exponentially with the number of threads. This is known as the state-explosion problem. One way to circumvent the state explosion problem is to design thread-modular verification algorithms that reason about concurrent software in modular way. Modularity allows one to avoid the explicit construction of the global state space by considering each thread in isolation (see [5], [7] and [11]).

The thread-modular verification algorithm of Flanagan and Qadeer (see [5]) circumvents state explosion by introducing an important overapproximation. As pointed out by Flanagan and Qadeer, the overapproximation is too coarse for many verification problems, e.g. mutual exclusion protocols. The reason for this is that the algorithm “forgets” some of the dependencies between threads and even “forgets” much of the temporal succession of states in a run. It is possible to view this algorithm as an attribute-independent method, characterizing the overapproximation in the abstract interpretation framework and reformulating the Flanagan-Qadeer algorithm as an abstract interpretation with a form of Cartesian abstraction (cf. [11], [12]).

The question is whether there is a way to modify the algorithm such that its abstraction can be parameterized. This is in analogy to the situation in abstract interpretation (see [2]) where the quality of program analysis depends on the judicious choice of an abstract domain. In this paper we will present such a parameterized method that extends thread-modular verification and is still polynomial in the number of threads.

We show how the approach can be formalized in the framework of abstract interpretation. We show that it is always possible to choose the parameter in such a way that the parameterized abstraction is complete for a concrete verification task. The parameter separates the state space in two parts: the one which is still subjected to the underlying abstraction and the part which is not subjected to the abstraction, but assumed to be reachable by definition. If this second part is actually reachable, then diminishing it leads to less precise analysis. We discover sufficient conditions that allow preserving polynomial-time complexity of the underlying abstraction.

Outline of the paper: First we explain our general approach in the abstract interpretation framework. We say what does it mean to parameterize an abstraction. We describe how different choices of the parameter influence precision. Especially we prove that the parameter can be chosen in such a way that abstract fixpoint checking is complete. We give a sufficient condition so that the parameterization introduces only a polynomial-time increase in complexity.

Then we apply this approach to multithreaded programs. First we define our multithreaded program model. Then we make the reader acquainted with Cartesian abstract interpretation for multithreaded programs. After that we introduce parameterized Cartesian abstraction. We define the abstract domain and abstraction and concretization maps, that allow using the standard forward abstract fixpoint checking algorithm. After that we look at the time and space requirements of the parameterized Cartesian successor computation. Then we present examples and a large class of programs that can be handled by the approach. At last, we describe the related work.

2 Parameterizing Abstractions

2.1 Preliminaries

In the framework of abstract interpretation (cf. [1] for introduction), abstract fixpoint checking is usually described by a concrete domain D, an abstract domain D^{#}, a Galois connections (α, γ) between them and a monotone successor operator F. We describe characterize a class of such tuples (D, D^{#}, α, γ, F) so that parameterized abstractions enjoy arbitrary precision and abstract fixpoint checking takes polynomial time.

Here and from now on, the application of a map f on an argument x is written as fx; the parentheses are used for delimiting subterms in unclear cases. We also write fg for the composition f ∘ g with (f ∘ g)x = f(gx). A lattice is boolean if it is complemented and distributive.

Assumption: Let D be a complete boolean lattice, D^{#} a complete lattice, (α, γ) a Galois-connection with α : D → D^{#} and γ : D^{#} → D. For the bottom element of D write ∅, write ∪ for the join, ∩ for the meet, and X^{c} for the complement of X ∈ D. The bottom element of D^{#} is denoted by ⊥, the join is ⊔, the meet is ⊓. Let the concretization map bottom to bottom, i.e. γ⊥ = ∅. Further let F : D → D be monotone, i.e. ∀ x, y ∈ D : x ⊆ y ⇒ F x ⊑ F y.

As usual, we denote the image of the abstraction map by D^{#}^{+} := αD. The image of D^{#}^{+} under the concretization map is D^{+} := γD^{#}^{+}.

2.2 Exceptional Abstraction

The idea of parameterizing an abstraction is introducing a concrete element E ∈ D (called the Exception Element), which is itself not subjected to abstraction and everything below it also should not be subjected to abstraction. Formally, consider the “exceptional abstraction” and “exceptional concretization” maps

α_{E} : D → D, X ↦ X ∩ E^{c}

and

γ_{E} : D → D, X ↦ X ∪ E .

Proposition 1. The pair (α_{E}, γ_{E}) is a Galois connection. Formally:

∀ X, Y ∈ D : α_{E}X ⊆ Y ⇔ X ⊆ γ_{E}Y

Proof. Let X, Y ∈ D. “⇒”: Let α_{E}X ⊆ Y, i.e. X ∩E^{c} ⊆ Y. Then X ⊆ X ∪E = (X ∪E)∩ “top of D”

= (X ∪ E) ∩ (E^{c} ∪ E) =^{distributivity} (X ∩ E^{c}) ∪ E ⊆^{X∩E^{c}⊆Y} Y ∪ E = γ_{E}Y.

“⇐”: Let X ⊆ γ_{E}Y, i.e. X ⊆ Y ∪ E. Then α_{E}X = X ∩ E^{c} ⊆^{X⊆Y ∪E} (Y ∪ E) ∩

E^{c} =^{distributivity} (Y ∩ E^{c}) ∪ \underbrace{(E ∩ E^{c})}_{⊥} = Y ∩ E^{c} ⊆ Y.  ⊓ ⊔

The composition (αα_{E}, γ_{E}γ) of Galois connections is itself a Galois-connection. We call it the parameterized Galois connection. Let init ∈ D be any element. Our analysis computes lfp λY. αα_{E}(init ∪ F γ_{E}γY). The concretization of this least fixpoint γ_{E}γ(lfp λY. αα_{E}(init ∪ F γ_{E}γY)) overapproximates the least fixpoint of init ∪ F by a standard result of the abstract interpretation framework (cf. [1], Prop. 13), so soundness of the analysis is guaranteed.

2.3 Influence of Exceptional Element on Precision

Now we discuss in detail how the choice of the Exception Element influences precision of the abstract fixpoint when using the parameterized Galois connection.

If E = ∅, then the exceptional abstraction and concretization maps are identities. That means no difference in comparison to the abstract fixpoint computation with (α, γ).

Since for a monotone map F the map λx. init ∪ F x is also monotone, the properties derived for an arbitrary monotone F also hold for λx. init ∪ F x. In this section we formulate everything for F.

Before proceeding, first remember that a postfix point of a map F : D → D is any x with F x ⊆ x. Second, according to the Knaster-Tarski fixpoint theorem, the least fixpoint of a monotone F exists and is the meet of its all postfix points (cf. [16], Thm. 1), i.e. lfp F = ⋂{x | F x ⊆ x}.

Proposition 2. An element is a postfix point of a monotone map if and only if the parameterized concretization of the abstract fixpoint (with Galois connection parameterized by this element) gives exactly this element. Formally:

∀ F ∈ (D ⟶^{mon} D), E ∈ D : F E ⊆ E ⇔ γ_{E}γ(lfp (αα_{E}F γ_{E}γ)) = E .

Proof. Let F be monotonic and E some element. “⇒”: Let F E ⊆ E. Since γ⊥ = ∅ by the assumption on the concretization map, we have γ_{E}γ⊥ = E and by postfix point property of E we have F γ_{E}γ⊥ ⊆ E, and thus αα_{E}F γ_{E}γ⊥ = ⊥ (that alpha maps bottom to bottom follows from the definition of a Galois connection). So the abstract fixpoint lfp (αα_{E}F γ_{E}γ) = ⊥ is trivial, thus its concretization is γ_{E}γlfp (αα_{E}F γ_{E}γ) = E. “⇐”: This holds in general for all Galois connections and not only for (αα_{E}, γ_{E}γ). So let (ᾱ, γ̄) be a Galois connection between the concrete domain D and the abstract domain D^{#} and E = γ̄lfp (ᾱF γ̄). Then F E = F γ̄lfp (ᾱF γ̄). The map γ̄ᾱ is extensive (a map ρ is called extensive iff x ⊆ ρx for all x from the domain of ρ), so F E ⊆ (γ̄ᾱ)F γ̄lfp (ᾱF γ̄) = γ̄(ᾱF γ̄)lfp (ᾱF γ̄) = γ̄lfp (ᾱF γ̄) = E. ⊓ ⊔

For program analysis this means: whenever we neither gain nor lose any precision by taking a set as an exception element, this set is an inductive program invariant and vice versa.

Since the least fixpoint of F exists and is a postfix point, we obtain

Corollary 3. There is an exception set so that abstract fixpoint computation with the Galois connection parameterized by this set gives the exact answer. Formally:

∃ E : γ_{E}γ(lfp (αα_{E}F γ_{E}γ)) = lfp F .

For program analysis this means that the parameterized analysis is complete in the sense that there is a choice of the exception set that leads to the best inductive invariant.

Corollary 4. An element A is an abstract postfix point if and only if the abstract fixpoint computation with Galois connection parameterized by the concretization of A returns the concretization of A. Formally:

∀ A ∈ D^{#} : αF γA ⊑ A ⇔ γ_{γA}γlfp (αα_{γA}F γ_{γA}γ) = γA .

Proof. Since (α, γ) is a Galois connection, αF γA ⊑ A ⇔ F γA ⊆ γA. The result follows with E = γA from Prop. 2. ⊓ ⊔

For program analysis this means: whenever A is an abstract inductive invariant, the abstract analysis with parameter γA neither increases nor decreases the precision compared to γA and vice versa. Especially one cannot increase precision by taking the least abstract fixpoint lfp (αF γ) as an exception set.

Now we show how the fixpoints are related when the parameter increases or decreases.

Proposition 5. Let A be any element and X be a result of abstract fixpoint computation with abstraction parameterized by A. Then taking as an exception set any element between A and the parameterized (by A) concretization of X and performing abstract fixpoint checking parameterized with this new element increases precision both in the abstract and in the concrete. Formally:

Let A, B ∈ D, F : D ⟶^{mon} D, X = lfp (αα_{A}F γ_{A}γ), A ⊆ B ⊆ γ_{A}γX and

Y = lfp (αα_{B}F γ_{B}γ). Then

1. Y ⊑ X.

2. For U = γ_{A}γX and V = γ_{B}γY holds V ⊆ U.

Proof.

1. From B ⊆ A ∪ γX follows B ∪ γX ⊆ A ∪ γX. From A ⊆ B follows B^{c} ⊆ A^{c}. We have αα_{B}F γ_{B}γX = α((F (B ∪ γX)) ∩ B^{c}) ⊑ [monotonicity of F and α] α((F (A ∪ γX)) ∩ A^{c}) = αα_{A}F γ_{A}γX = X. So X is a postfix point of αα_{B}F γ_{B}γ, while Y is its least fixpoint, which is by Knaster-Tarski less than or equal to any of its postfix points. Thus Y ⊑ X.

2. From monotonicity of the concretization map follows γY ⊆ γX and thus B ∪ γX ⊆ A ∪ γX implies V = B ∪ γY ⊆ A ∪ γX = U. ⊓ ⊔

For program analysis this means that under certain circumstances choosing a greater exception set leads to a smaller invariant, even if the exception sets are not contained in the most precise program invariant. This could be helpful, for instance, if a larger exception set can be represented more efficiently. However, if both A and B are contained in the least invariant, then the precision of abstract fixpoint checking is increased for sure:

Corollary 6. Let A, B be any two comparable elements below the least concrete fixpoint. Then parameterizing the abstract fixpoint computation by the greater element leads to a more precise abstract fixpoint than parameterizing it by the smaller element. Formally: Let A ⊆ B ⊆ lfp F, X = lfp (αα_{A}F γ_{A}γ), Y = lfp (αα_{B}F γ_{B}γ), U = γ_{A}γX, and V = γ_{B}γY. Then Y ⊑ X and V ⊆ U.

Proof. The standard result of the abstract interpretation framework (cf. [1], Prop. 13) applied to (αα_{A}, γ_{A}γ) implies lfp F ⊆ γ_{A}γX. From B ⊆ lfp F follows B ⊆ γ_{A}γX. The result follows from Prop. 5. ⊓ ⊔

For program analysis this means that as long as the exception set grows, but remains below the best invariant, the precision of the analysis grows too.

Proposition 7. Assume some postfix point of F is an exceptional concretization of the concretization of an abstract element. Then computation of the abstract fixpoint parameterized by the exception element gives an element whose parameterized concretization is less than or equal to that postfixed point of F.

Formally: Let E ∈ D, Y ∈ D^{#}, X = γY, R = γ_{E}X, F : D ⟶^{mon} D, F R ⊆ R. Then γ_{E}γ(lfp (αα_{E}F γ_{E}γ)) ⊆ R.

Proof. Remember that for any Galois connection (ᾱ, γ̄) between D and D^{#} holds that ᾱγ̄ is reductive (i.e. ∀ y ∈ D^{#} : ᾱγ̄y ⊑ y). Moreover both abstraction and concretization are monotonic. Then α_{E}R = R ∩ E^{c} = (E ∪ X) ∩ E^{c} = (E ∩ E^{c}) ∪ (X ∩ E^{c}) = ∅ ∪ (X ∩ E^{c}) ⊆ X = γY. So γ_{E}γαα_{E}R ⊆ γ_{E}γαγY ⊆ [αγ reductive] γ_{E}γY = γ_{E}X = R. Then αα_{E}F γ_{E}γ(αα_{E}R) = αα_{E}F (γ_{E}γαα_{E})R ⊑ αα_{E}F R ⊑ [since F R ⊆ R] αα_{E}R. So αα_{E}R is a postfix point of αα_{E}F γ_{E}γ and thus greater than or equal to its least fixpoint. So γ_{E}γ(lfp (αα_{E}F γ_{E}γ)) ⊆ γ_{E}γαα_{E}R ⊆ R. ⊓ ⊔

2.4 Polynomial Exceptional Abstraction

In order to be able to argue about polynomial run time, we measure a domain by the number of elements in its longest chain and by the maximal length of the binary representation of its elements. We take the maximum of both values as the measure of the domain and formulate the run time as a function of this maximum.

Assumption:

– The map F is a join-morphism.

– The abstract domain is finite. Transforming the elements of the abstract domain to and from binary string takes polynomial time. Formally: if m is the measure of D^{#} then there is a pair of maps

ϕ : D^{#} ↪ {0, 1}^{m} ,
ϕ^{−1} : {0, 1}^{m} → D^{#} ,

so that ϕ is one-to-one, ϕ^{−1} is a left inverse of ϕ, ϕ is polynomial-time computable and ϕ^{−1} is polynomial-time computable on the image of ϕ.

– The abstract join operation needs polynomial time in m. In the following, 2^{X} is the power set of X. The next assumption on F is (in contradiction to the assumptions before) a strong restriction, so we call it a

Hypothesis: The function F maps the concretization of every abstract element to a concrete join of concretizations of polynomial many abstract elements. Formally speaking, there exists a polynomial-time computable map

F̄ : D^{#}^{+} → 2^{D^{#}^{+}} ,
y ↦ Y ,

where |Y | ≤ m^{k} (for a constant k ∈ ℕ independent on m) and where

F γy = ⋃ γY .

Proposition 8. Under the assumptions and the Hypothesis, there is a RAM program and for any exception element E there is a data structure for this program so that the program computes the best correct approximation F_{E}^{#} = αα_{E}F γ_{E}γ on D^{#}^{+} in polynomial time in the measure of the abstract domain.

Proof. Let y ∈ D^{#}^{+}. We have

F_{E}^{#}y = α(E^{c} ∩ F (E ∪ γy)) = [F join-morphism]
= α(E^{c} ∩ ((F E) ∪ (F γy))) = [distributivity]
= α((E^{c} ∩ F E) ∪ (E^{c} ∩ F γy)) = [α join-morphism]
= α(E^{c} ∩ F E) ⊔ α(E^{c} ∩ F γy).

Since E is a constant independent on y, the expression α(E^{c} ∩ F E) =: E′ is also constant and can be computed once; we view E′ as a part of representation of E. The join operation needs polynomial time, so is suffices to show that the map y ↦ α(E^{c} ∩ F γy) is polynomial computable. The hypothesis implies that this expression equals

α(E^{c} ∩ ⋃ γF̄y) = [distributivity] α(⋃{E^{c} ∩ γy′ | y′ ∈ F̄y}) =
= [α join-morphism] ⨆{α((γy′) ∩ E^{c}) | y′ ∈ F̄y} .

Since F̄y has polynomial many elements and the abstract join ⊔ is polynomialtime computable, it suffices to show that the map y′ ↦ α((γy′) ∩ E^{c}) is computable in polynomial time. Notice that α((γy′)∩E^{c}) = ϕ^{−1}ϕα((γϕ^{−1}ϕy′)∩E^{c}). Since both ϕ and ϕ^{−1} are polynomial-time computable, if suffices to show that the map

{0, 1}^{m} → {0, 1}^{m} , v ↦ ϕα((γϕ^{−1}v) ∩ E^{c})

is polynomial-time computable in m at least on the image of ϕ. This map, as any map from {0, 1}^{m} → {0, 1}^{m}, can be represented by a decision tree of size m2^{m} and depth m (or even a multiterminal binary decision diagram) on a RAM with logarithmic cost measure and built-in addition (cf. [13]). An evaluation takes O(m^{2}) time. This map doesn’t depend on F, so we view the decision tree as the second part of the representation of E. ⊓ ⊔

Theorem 9. Under the assumptions and the Hypothesis, there is a representation of the exception element so that abstract fixpoint computation takes polynomial time in the measure of the abstract domain. Formally:

Computing

lfp λY. αα_{E}(init ∪ F γ_{E}γY)

takes polynomial time in m.

Proof. The usual abstract fixpoint iteration sequence is X^{0} = ⊥ and X^{i+1} = αα_{E}(init ∪ F γ_{E}γX^{i}). This sequence is monotone and stabilizes in a finite number of steps. The abstraction maps α and α_{E} are join-morphisms, so X^{i+1} = αα_{E}init ⊔ αα_{E}F γ_{E}γX^{i}. The first term is constant, the second can be computed in polynomial time as just shown, the join operation is polynomial. So the next term of the sequence (X^{i})_{i} is computable in polynomial time from the previous one. Since the maximal chain length is at most m, the number of iterations till the sequence stabilizes is at most m. ⊓ ⊔

3 Thread-Modular Verification

3.1 Multithreaded Programs

A multithreaded program is a tuple

(Glob, Loc, (→_{i})_{i=1}^{n}, init),

where Glob and Loc are any sets, each →_{i} is a subset of (Glob × Loc)^{2} (for 1 ≤ i ≤ n) and init ⊆ Glob × Loc^{n}. The meaning of different components of the multithreaded program is the following:

– Loc contains valuations of local variables (including the program counter) of any thread, we call it the local store of the thread (without loss of generality we assume that all threads have equal local stores);

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

– the elements of States = Glob×Loc^{n} are called program states, the elements of Q = Glob×Loc are called thread states, the projection on the global store and the ith local store is the map

π_{{0,i}} : 2^{States} → 2^{Q}, S ↦ {(g, l_{i}) | (g, l) ∈ S};

– the relation →_{i} is a transition relation of the ith thread (1 ≤ i ≤ n);

– init 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 a step of some of the threads. The successor operation maps a set of program states to the set of their successors:

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

We are interested in proving safety properties of multithreaded programs. Each safety property can be encoded as a reachability property and each reachability property can be encoded as reachability between a pair of states. So 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) .

The state explosion problem in context of multithreaded programs refers to the fact that the number of program states is exponentially large in the number of threads n. We don’t address the problem of growing state space due to the number of variables, which is also common to sequential programs.

3.2 Cartesian abstract interpretation

In previous work (see [11]) the authors presented the theory of Cartesian abstraction for multithreaded programs. Here we repeat a necessary part of this background for clarity.

We present a concrete and an abstract domain and a Galois connection between them that allows us to do abstract fixpoint checking. The definitions below extend the usual notion of the dependence-free abstraction (as, for instance, formulated by Cousot in [3]):

D = 2^{States} is the set underlying the concrete lattice, D^{#} = (2^{Glob×Loc})^{n} is the set underlying the abstract lattice,

\begin{aligned}α_{cart} : & D → D^{#}, \\ & S ↦ (π_{\{0,i\}}S)_{i=1}^{n} \end{aligned}

is the abstraction map, which projects a set of program states to the tuple of sets of thread states, so that the ith component of a tuple contains all states of the ith thread that occur in the set of program states.

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

is the concretization map that combines a tuple of sets of thread states to a set of program states by putting only those thread states together that have equal global part.

The ordering on the concrete domain D is inclusion, the least upper bound is the union ∪, the greatest lower bound is the intersection ∩, the complement X^{c} of a set X.

The ordering on the abstract domain D^{#} is the product ordering, i.e. T ⊑ T′ if and only if T_{i} ⊆ T′_{i} for all i ∈ {1, ..., n}. The least upper bound ⊔ is componentwise union, the greatest lower bound ⊓ is componentwise intersection. So the abstract lattice is complete. The bottom element is the tuple of empty sets ⊥ = (∅)_{i=1}^{n}.

Notice that the image of the concrete lattice under abstraction is

D^{#}^{+} = {(R_{i})_{i=1}^{n} | ∀g ∈ Glob : (∃i ∈ ℕ_{n} : (g, ) ∈ R_{i}) ⇒ ∀j ∈ ℕ_{n} : (g, ) ∈ R_{j}} ,

where underscore ( ) means “anything”, i.e. an innermost existentially quantified variable, and ℕ_{n} = {1, ..., n} is the set of first n natural numbers.

The following is an extension of the corresponding standard result (cf. [3]).

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

α_{cart}S ⊑ T iff S ⊆ γ_{cart}T .

Proof. “⇒”: Let (g, l) ∈ S. Let T′ = α_{cart}S. Then by definition of α_{cart} we have for all i ∈ {1, ..., n} that (g, l_{i}) ∈ T′_{i} ⊆ T_{i}. So (g, l) ∈ γ_{cart}T by definition of γ_{cart}. “⇐”: Let T′ = α_{cart}S. Fix some i ∈ {1, ..., n} and let (g, l_{i}) ∈ T′_{i}. By definition of α_{cart} for each other j ≠ i there is an l_{j} so that the tuple containing all these elements (g, (l_{j})_{j=1}^{n}) is in S. But S ⊆ γ_{cart}T, so (g, (l_{j})_{j=1}^{n}) ∈ γ_{cart}T. By definition of γ_{cart} we have (g, l_{i}) ∈ T_{i}. So T′_{i} ⊆ T_{i}. Since i was arbitrarily chosen, we have T′ ⊑ T by definition of ⊑. ⊓ ⊔

4 Parameterized Cartesian Abstraction

First we prove why the conditions for parameterized abstraction to work are satisfied. We show what run time and what space requirements are needed. After that we give another algorithm computing the abstract post with different time-space requirements, thus discovering a time-space tradeoff.

4.1 Polynomial Time

Now we show why the conditions of the Theorem 9 are met for the Cartesian abstraction/concretization maps on the above domains D and D^{#}.

First, the concrete lattice D is boolean and complete. Then the concretization map γ_{cart} maps ⊥ = (∅)_{i=1}^{n} to ∅. The successor map post distributes over union, so it is a join-morphism. The maximal chain length of D^{#} is n|Glob||Loc| + 1. A single abstract element is an n-tuple (R_{1}, ..., R_{n}) of subsets R_{i} of Glob × Loc, which can be coded in polynomial time by n|Glob||Loc| boolean variables corresponding to the answers to the questions ”(g, l) ∈ R_{i}” for g ∈ Glob, l ∈ Loc and i ∈ {1, ..., n}. The abstract join operation (R_{i})_{i=1}^{n} ⊔ (R′_{i})_{i=1}^{n} = (R_{i} ∪ R′_{i})_{i=1}^{n} takes time proportional to n and the maximal possible sizes of the sets R_{i}, R′_{i} (1 ≤ i ≤ n).

To prove the hypothesis, assume we have an abstract element (R_{i})_{i=1}^{n}, which can also be written as ⨆_{g∈Glob}({g} × R_{i}^{g})_{i=1}^{n} where R_{i}^{g} = {l | (g, l) ∈ R_{i}} for 1 ≤ i ≤ n. Its concretization is ⋃_{g∈Glob}({g} × ∏_{i=1}^{n} R_{i}^{g}). So in order to show that the successors of this set are a union of polynomially many elements of D^{+}, it suffices to show that for any g ∈ Glob the successor set of {g} × ∏_{i=1}^{n} R_{i}^{g} is a union of polynomial many elements of D^{+}. For each g ∈ Glob we have post({g} × ∏_{i=1}^{n} R_{i}^{g}) =

⋃_{(g,l_{i})→_{i}(g′,l′_{i})}\{g′\} × R_{1}^{g} × ... × R_{i−1}^{g} × \{ \begin{matrix}\{l′\} & , if l ∈ R_{i}^{g} \\ ∅ & , otherwise \end{matrix} \} × R_{i+1}^{g} × ... × R_{n}^{g} ,

the number of Cartesian products being bounded by the number of transitions of all threads, which is at most n(|Loc||Glob|)^{2}. So we have proven that parameterized Cartesian abstraction is polynomial.

An exact analysis gives the run time O(G^{2}L^{4}n^{3} log(LGn)) for a single computation of the abstract post operator, while the data structure for the exception set needs space O(GL^{2}n^{2}2^{Ln}) where L = |Loc| and G = |Glob| and the machine model is RAM with logarithmic cost measure. Using unit cost measure instead one can get O(G^{2}L^{3}n^{2}) run time for a single iteration. So the whole analysis, i.e. iteration till fixpoint, takes cubic time in the number of threads under the unit cost measure. The proofs of the run times are left to the reader as an exercise.

4.2 Polynomial space

Now we try to get rid of the exponential space in the size of the local store. We develop an algorithm for computing abstract successor operator with polynomial time in the number of threads and in the size of the exception set. Since two different exception sets lead in general to different abstract fixpoints, a representation of E needs at least |Glob||Loc|^{n} space in a worst case.

Let

post_{E,cart} = α_{cart} ∘ α_{E} ∘ post ∘ γ_{E} ∘ γ_{cart}

be the best correct approximation of post.

For the following technical lemma, the numbers n and L are any natural numbers and are not necessarily related to the multithreaded program.

Lemma 11. There is an algorithm, that for n finite sets A_{i} (1 ≤ i ≤ n) with at most L elements each (represented so that |A_{i}| for each i is computable in polynomial time in L and in n), computes the size of their product |∏_{i=1}^{n} A_{i}| in polynomial time in L and in n.

Proof. The number is ∏_{i=1}^{n}|A_{i}|. Each number |A_{i}| has O(log L) digits, and the number |A_{1}| ⋯ |A_{i−1}| has O((i − 1) log L) digits. So multiplying these two numbers needs O((i−1) log^{2} L) primitive additions. Summing over i gives O(n^{2} log^{2} L) primitive additions. ⊓ ⊔

Proposition 12. The parameterized Cartesian successor operator post_{E,cart}^{#} is computable in polynomial time in n, |Glob|, |Loc| and |E|, the representation of E taking space O(|E|).

Proof. Let E be represented as a list of tuples, sorted according to the global component. Following the lines of the proof of Proposition 8, we consider the innermost computation step, namely the computation of the map

f_{E} : D^{#} → D^{#}, y′ ↦ α_{cart}((γ_{cart}y′) \ E) .

So let y′ be represented by the sets R_{i}^{g} = ({g}×Loc)∩R_{i} for g ∈ Glob, 1 ≤ i ≤ n as y′ = ⊔_{g∈Glob}(R_{i}^{g})_{i=1}^{n}. Then

f_{E}y′ = ⨆_{g∈Glob} f_{E}((R_{i}^{g})_{i=1}^{n}) .

Let E be represented by sets E^{g} = ({g} × Loc^{n}) ∩ E. We get all E^{g} from E by going through the list E once. Then it suffices to compute F_{E}((R_{i}^{g})_{i=1}^{n}) = α_{cart}((γ_{cart}(R_{i}^{g})_{i=1}^{n}) \ E) = α_{cart}((γ_{cart}(R_{i}^{g})_{i=1}^{n}) \ E^{g}) = F_{E^{g}}((R_{i}^{g})_{i=1}^{n} once for each g and join the results. So let’s fix g. Since in computation of the last term the global part remains constant g, we may as well forget it and use the standard Cartesian abstraction/concretization maps

α_{c} : 2^{(Loc^{n})} → (2^{Loc})^{n}, S ↦ (π_{i}S)_{i=1}^{n} ,

γ_{c} : (2^{Loc})^{n} → 2^{(Loc^{n})}, T ↦ ∏_{i=1}^{n} T_{i} ,

computing α_{c}((∏_{i=1}^{n} A_{i})\B) for A_{i} = {l_{i} | (g, l_{i}) ∈ R_{i}} (1 ≤ i ≤ n) and B = {l | (g, l) ∈ E}. By going through the list B once we construct B′ = B ∩ ∏_{i=1}^{n} A_{i}. It suffices to compute for each j ∈ ℕ_{n} the projection

π_{j}(α_{c}((∏_{i=1}^{n} A_{i}) \ B′)).

Let us fix some j. We have to determine for r ∈ A_{j}, whether r ∈ π_{j}(α_{c}((∏_{i=1}^{n} A_{i})\ B′)). It is the case if and only if there are strictly more tuples in the cross product ∏_{i=1}^{n} A_{i} containing r in the jth component than in B′. The number of tuples in ∏_{i=1}^{n} A_{i} with r at the jth place is ∏_{1≤i≤n,i≠j}|A_{i}|, which can be computed in polynomial time by Lemma 11. The number of tuples in B′ where r occurs in the jth component can be determined by a linear scan of B′. ⊓ ⊔

By definition, the parameterized Cartesian successor operator post_{E,cart}^{#}(R) is monotone in the argument R, so the usual fixpoint iteration of

𝔉 = λR. α_{cart}α_{E}init ⊔ post_{E,cart}^{#}R ,

produces elements on a chain:

⊥ ⊑ 𝔉⊥ ⊑ 𝔉𝔉⊥ ⊑ 𝔉𝔉𝔉⊥ ⊑ ...

The longest chains in the abstract domain D^{#} = (2^{Q})^{n} have 1 + n|Q| ≤ 1 + n|Glob × Loc| = O(nGL) elements where G is the size of the global store and L the size of a local store. Thus the parameterized Cartesian post operator enjoys the following property.

Theorem 13. Given a multithreaded program and an exception set E stored as a list, abstract fixpoint checking with the parameterized Cartesian post operator post_{E,cart}^{#} takes polynomial time in the size of program description and in the size of the exception set.

Formally: There is an algorithm that for each E ⊆ States stored as a list computes

lfp λR. α_{cart}α_{E}init ⊔ post_{E,cart}^{#}R

in polynomial time in n, |Glob|, |Loc|, |init| and |E|.

4.3 Exception Set as Union of Maximal Cartesian Products

There is a data structure for the exception set that is simple, needs polynomial space for an important large class of real-world programs and allows polynomial time abstract fixpoint computation in the size of this data structure. First we need a technical result from the set theory.

Assumption:

Let D be any complete lattice with order ≤ (strict order x < y iff (x ≤ y and x ≠ y)), and assume we have fixed some “generating” subset of D so that each element of D can be written as a join of some elements of the generating subset. Further let Y ⊆ D be any set that contains the generating set so that the supremum of each chain in Y belongs to Y.

For a ∈ D, an element y ∈ D is called a-maximal, if it is in Y, is less than or equal to a and there is no other greater element of Y that is less than or equal to a, formally: Y ∋ y ≤ a and ∄ y′ ∈ Y : y < y′ ≤ a. A set M is called maximized, if M ⊆ Y and ∀ y ∈ Y : y ≤ ⋁ M ⇒ ∃ y′ ∈ M : y ≤ y′.

In the following, statements marked by (AC) have a proof that depends on the axiom of choice in case the lattice is infinite, but not if the lattice is finite. It’s unknown whether there is a proof independent on AC for infinite lattices.

Proposition 14 (AC). Let a ∈ D. Then any element of Y less than or equal to a is less than or equal to some a-maximal element.

Proof. Remember the maximal chain principle (cf. [14]), which says that in each partial order on a set there is a maximal chain. Now let b ∈ Y and b ≤ a, then the set N = {y ∈ Y | b ≤ y ≤ a} is partially ordered by ≤, so according to the maximal chain principle there is a chain C ⊆ N which cannot be extended. It is also a chain in Y, so c := ⋁ C ∈ Y by assumption on Y. At the same time ∀ y ∈ C : y ≤ a, so c ≤ a. If there were another c′ ∈ Y with c < c′ ≤ a, then c′ ∈ N and C could be extended by c′ in contradiction to the maximality of C. So c is an a-maximal element greater than or equal to b. ⊓ ⊔

Proposition 15 (AC). Each element a of the lattice can be represented as a join of a unique maximized antichain. This maximized antichain contains exactly the a-maximal elements.

Proof. Let a ∈ D.

First we show existence. So let M contain exactly the a-maximal elements. Two a-maximal elements are incomparable by definition, so M is an antichain.

Since M contains only elements below a, we have ⋁ M ≤ a. So if y ∈ Y with y ≤ ⋁ M is given, then y ≤ a, so Prop. 14 gives us some a-maximal element that is greater than or equal to y. So M is maximized.

Now a can be written as ⋁ A for a set of generating elements A ⊆ Y which are all less than or equal to a. Each element in Y which is less than or equal to a is by Prop. 14 less than or equal to some element of M, so a = ⋁ A ≤ ⋁ M. Together with ⋁ M ≤ a we get a = ⋁ M.

Now we show uniqueness. It suffices to show that for each two maximized antichains M, M′ with a = ⋁ M = ⋁ M′ we have M ⊆ M′. So let such M and M′ be given and b ∈ M. Then b ≤ a and, since M′ is maximized and b ≤ ⋁ M′, there is a b′ ∈ M′ with b ≤ b′. Then b′ ≤ a and, since M is maximized and b′ ≤ ⋁ M, there is a b′′ ∈ M with b′ ≤ b′′. From b ≤ b′ ≤ b′′ and b, b′′ ∈ M and the antichain property of M follows b = b′ = b′′. This proves b ∈ M′. ⊓ ⊔

Proposition 16 (AC). Each maximized set contains the unique maximized antichain with the same join. Formally:

∀ maximized A ⊆ Y ∃^{1}M ⊆ A : M is a maximized antichain and ⋁ M = ⋁ A .

Proof. Let A ⊆ Y be maximized and a = ⋁ A. According to Prop. 15 there is a maximized antichain M with join a which contains exactly the a-maximal elements. Moreover, it is the only maximized antichain with join a. To show M ⊆ A, assume for the purpose of contradiction that there is some a-maximal element y which is not in A. Then Y ∋ y ≤ a = ⋁ A, so by definition of maximized there is y′ ∈ A with y ≤ y′. From y ∉ A follows y < y′. From ⋁ A = a follows y′ ≤ a. So there is an element of Y (namely y′) greater than y and less than or equal to a, in contradiction to y being a-maximal. ⊓ ⊔

Now let’s consider the Cartesian products. Recall that a function is a set of pairs so that for each first component there is exactly one second component. For an index set I, a Cartesian product of sets A_{i} (i ∈ I) is the set of maps ∏_{i∈I} A_{i} := {f : I → ∪_{i∈I}A_{i} | ∀ i ∈ I : f(i) ∈ A_{i}}. For a subset of indices J ⊆ I the projection of a subset A ⊆ ∏_{i∈I} A_{i} on the components J is π_{J}A = {f : J → ∪_{j∈J}A_{j} | ∃ g ∈ A : f ⊆ g}. A projection on a single index i ∈ I is π_{i}A = {a ∈ A_{i} | ∃ g ∈ A : (i, a) ∈ g}. For a natural number n, the set A^{n} := ∏_{i=1}^{n} A is the nth power of A.

Lemma 17 (AC). Let A_{i}, B_{i} be sets indexed by i ∈ I. Then

∏_{i∈I} A_{i} ⊆ ∏_{i∈I} B_{i} ⇔ ((∀ i ∈ I : A_{i} ⊆ B_{i}) or ∃ i ∈ I : A_{i} = ∅) .

Proof.

“⇒”: Let the Cartesian product of A_{i} (i ∈ I) be included in the Cartesian product of B_{i} (i ∈ I). If there is an index i so that A_{i} = ∅, then the claim holds trivially. Otherwise all A_{i} are nonempty (i ∈ I). Now fix some i ∈ I and let a ∈ A_{i}. The axiom of choice applied to the sets A_{j} (j ∈ J := I \ {i}) gives a choice function f : J → ⋃_{j∈J} A_{j} with f(j) ∈ A_{j} (j ∈ J). For g := f ∪ {(i, a)} follows that g ∈ ∏_{j∈I} A_{j}, so g ∈ ∏_{j∈I} B_{j}, thus g(i) ∈ B_{i}, so a ∈ B_{i}. This proves A_{i} ⊆ B_{i}.

“⇐”: If for some i ∈ I holds A_{i} = ∅, then there is no map f with f(i) ∈ A_{i}, so ∏_{i∈I} A_{i} = ∅. Otherwise all A_{i} are nonempty (i ∈ I). Now let f ∈ ∏_{i∈I} A_{i}. Then ∀ i ∈ I : f(i) ∈ A_{i} ⊆ B_{i} and ∪_{i∈I}A_{i} ⊆ ∪_{i∈I}B_{i}, so f ∈ ∏_{i∈I} B_{i}. ⊓ ⊔

For the power set D = 2^{(Loc^{n})} of all tuples of length n, ordered by inclusion, Y the set of all Cartesian products in D, and the set of singletons as a generating subset the assumption is satisfied: singletons are Cartesian products and the union of a chain of Cartesian products is a Cartesian product.

Combinatorial Problem: If the underlying set Loc is finite, how large can a maximized antichain of Cartesian products be?

We don’t know how to solve this problem at the moment.

For a set of tuples A ⊆ Loc^{n}, i ∈ ℕ_{n} and r ∈ Loc let us call

A_{i,r} = π_{ℕ_{n}\{i}}{a ∈ A | a_{i} = r}

a restriction of A (with parameters i, r). An (n − 1)-tuple lies in this set exactly if, whenever r would be inserted at the ith position, the tuple would lie in A. Since projection is monotonic, restrictions are monotonic also, i.e.

∀ A ⊆ B ⊆ Loc^{n}, i ∈ ℕ_{n}, r ∈ Loc : A_{i,r} ⊆ B_{i,r} .

Lemma 18 (AC). Let a set A ⊆ Loc^{n} be represented as a maximized antichain M of Cartesian products. Then for each i ∈ ℕ_{n}, r ∈ Loc, the set A_{i,r} has a representation as a union of a maximized antichain M′ of Cartesian products with no greater cardinality than |M|. If Loc is finite and Cartesian products are stored componentwise, the elements of the new maximized antichain can be computed in polynomial time in n, |Loc| and |M|.

Proof. Let M be the maximized antichain of Cartesian products with union A and let us fix i ∈ ℕ_{n}, r ∈ Loc. Let M_{i,r} = {C_{i,r} | C ∈ M}. First we show that its union is ⋃ M_{i,r} = A_{i,r}.

“⊆”: Each C ∈ M is contained in A, so C_{i,r} ⊆ A_{i,r} by monotony of restrictions. Thus ⋃_{C∈M} C_{i,r} ⊆ A.

“⊇”: If a ∈ A_{i,r} then b := a ∪ {(i, r)} ∈ A and there is some C ∈ M with b ∈ C. Then a ∈ C_{i,r} ⊆ ⋃ M_{i,r}.

To prove that M_{i,r} is maximized, let K = ∏_{1≤j≤n,j≠i} K_{j} be a Cartesian product of (n − 1)-tuples contained in A_{i,r} with components K_{j} ⊆ Loc (1 ≤ j ≤ n, j ≠ i) and let K̃ = {l ∈ Loc^{n} | ∃ a ∈ K : a ∪ {(i, r)} = l} so that (K̃)_{i,r} = K. Then K̃ = {f : ℕ_{n} → Loc | f(i) ∈ {r} and ∀ j ≠ i : f(j) ∈ K_{j}} is a Cartesian product in D and is thus contained in some maximal Cartesian product C ∈ M as a subset. Restrictions preserve inclusions, so K = (K̃)_{i,r} ⊆ C_{i,r}. So the set M_{i,r} is maximized.

In case Loc is infinite, Prop. 16 says there is a subset M′ of M_{i,r} which is a maximized antichain with the same union A_{i,r}. Since there is a bijection between M and M_{i,r} ⊇ M′, the set M′ is at most as large as M.

In case Loc is finite, M_{i,r} can be constructed from M in polynomial time. Then we set originally M′ := ∅. For each Cartesian product A ∈ M_{i,r} we check whether there is a strictly larger Cartesian product B ∈ M_{i,r} and if no, we add A to M′. After at most |M_{i,r}|^{2} many iterations all elements of M′ are incomparable, their union is still A_{i,r} and M′ is maximized by construction. ⊓ ⊔

In the following, we reduce the problem of computing the abstract parameterized post to a simpler problem about the “standard” Cartesian abstraction and concretization maps:

α_{c} : 2^{(Loc^{n})} → (2^{Loc})^{n}, S ↦ (π_{i}S)_{i=1}^{n} ,

γ_{c} : (2^{Loc})^{n} → 2^{(Loc^{n})}, T ↦ ∏_{i=1}^{n} T_{i} .

We call the elements of (2^{Loc})^{n} Cartesian abstract elements. There is an injection of the set of Cartesian products in Loc^{n} into the set of Cartesian abstract elements. The nonempty Cartesian products get bijectively mapped to the tuple of their components, the empty Cartesian product has a nonunique representation as a tuple of sets among which at least one set is empty (for n > 0).

Assumption: For the rest of this section let the local store be finite. Each element of (2^{Loc})^{n} is represented as a list of n entries, each entry is itself a list of some elements from Loc.

Proposition 19. The question whether a Cartesian product is a subset of a set of tuples can be solved in polynomial time.

Formally: there is an algorithm that computes the map

2^{(Loc^{n})} × (2^{Loc})^{n} → Bool, (E, A) ↦ γ_{c}A ⊆^{?} E

where E is represented as a set M of Cartesian abstract elements so that γ_{c}M is a maximized antichain and E = ⋃ γ_{c}M, in polynomial time in |M|, n and |Loc|.

Proof. The algorithm tests for each B ∈ M, whether γ_{c}A ⊆ γ_{c}B, and returns yes, if any of these tests succeeds, otherwise it returns no. The algorithm is correct, since γ_{c}M is maximized. Since γ_{c}A ⊆ γ_{c}B if and only if ((∀ i ∈ ℕ_{n} : A_{i} ⊆ B_{i}) or ∃ i ∈ ℕ_{n} : A_{i} = ∅), each such test is done in polynomial time in n and in Loc, so all the |M| tests are done in polynomial time in n, |M|, and |Loc|. ⊓ ⊔

Proposition 20. The smallest Cartesian product that contains another Cartesian product without an exception set can be computed in polynomial time.

Formally: there is an algorithm that computes the map

2^{(Loc^{n})} × (2^{Loc})^{n} → (2^{Loc})^{n}, (E, A) ↦ α_{c}(E^{c} ∩ γ_{c}A)

where E is represented as a set M of Cartesian abstract elements so that γ_{c}M is a maximized antichain and E = ⋃ γ_{c}M, in polynomial time in |M|, n and |Loc|.

Proof. Let E ⊆ Loc^{n}, A ∈ (2^{Loc})^{n}. If γ_{c}A is empty (which holds iff A_{i} = ∅ for some i ∈ ℕ_{n}), then the return value is the tuple of empty sets. Otherwise all A_{i} are nonempty.

Claim: For all r ∈ Loc, i ∈ ℕ_{n} holds:

r ∈ (α_{c}(E^{c} ∩ γ_{c}A))_{i} ⇔ r ∈ A_{i} and ∏_{j∈ℕ_{n}\{i}} A_{j} ⊈ E_{i,r} .

To prove the “⇒” direction, let r ∈ (α_{c}(E^{c} ∩ γ_{c}A))_{i} = π_{i}(E^{c} ∩ γ_{c}A). So there is an n-tuple a ∈ E^{c} ∩ ∏_{i=1}^{n} A_{i} with a_{i} = r, thus r ∈ A_{i}. Moreover a ∉ E and a_{j} ∈ A_{j} (j ∈ ℕ_{n}). So the (n − 1)-tuple a \ {(i, r)} ∈ ∏_{j∈ℕ_{n}\{i}} A_{j}, but a \ {(i, r)} ∉ E_{i,r}.

To prove “⇐”, let r ∈ A_{i} and let a be an (n−1)-tuple with a ∈ ∏_{j∈ℕ_{n}\{i}} A_{j} and a ∉ E_{i,r}. Then a ∪ {(i, r)} ∉ E, but a ∪ {(i, r)} ∈ ∏_{j=1}^{n} A_{j} = γ_{c}A. Thus a ∪ {(i, r)} ∈ E^{c} ∩ γ_{c}A, hence r ∈ π_{i}(E^{c} ∩ γ_{c}A) = (α_{c}(E^{c} ∩ γ_{c}A))_{i}.

The claim is proven. By Lemma 18, for each i ∈ ℕ_{n}, r ∈ Loc, there is a maximized antichain M′_{i,r} of Cartesian products with union E_{i,r} and componentwise representation of Cartesian products as Cartesian abstract elements, computed in polynomial time. Since M′_{i,r} is maximized, A′ ⊆ M′_{i,r} if and only if ∃ C ∈ M′_{i,r} : A′ ⊆ C for any Cartesian product A′, especially for ∏_{j∈ℕ_{n}\{i}} A_{j}. So for each r ∈ Loc, i ∈ ℕ_{n} holds:

r ∈ (α_{c}(E^{c} ∩ γ_{c}A))_{i}  ⇔  r ∈ A_{i} and ∀ C ∈ M′_{i,r} : ∏_{j∈ℕ_{n}\{i}} A_{j} ⊈ C .

Since M′_{i,r} is generated in polynomial time and inclusion of Cartesian products is polynomial-time by Lemma 17, all the components of the abstract element α_{c}(E^{c} ∩ γ_{c}A) are computable in polynomial time. ⊓ ⊔

Now we go over to the domains used in program analysis, namely to D = 2^{States} = 2^{Glob×Loc^{n}} and D^{#} = (2^{Glob×Loc})^{n}.

Proposition 21. The smallest abstract element that is greater than or equal to the concretization of another abstract element without an exception set can be computed in polynomial time.

Formally: Assume that for E ∈ D, each {l | (g, l) ∈ E} (for g ∈ Glob) is represented a set of Cartesian abstract elements whose concretizations form a maximized antichain and have {l | (g, l) ∈ E} (for g ∈ Glob) as a union. Then computing the map

D × D^{#} → D^{#}, (E, A) ↦ α_{cart}(E^{c} ∩ γ_{cart}A)

needs polynomial time in n, |Loc|, |Glob| and the maximum cardinality of an antichain.

Proof. Let A ∈ D^{#} and E ∈ D. For each g ∈ Glob and i ∈ ℕ_{n} let A_{i}^{[g]} := {l | (g, l) ∈ A_{i}} and A^{[g]} := ∏_{i∈ℕ_{n}} A_{i}^{[g]}. For all g ∈ Glob, l ∈ Loc^{n} holds: ((g, l) ∈ γ_{cart}A) iff (∀ i ∈ ℕ_{n} : (g, l_{i}) ∈ A_{i}) iff (∀ i ∈ ℕ_{n} : l_{i} ∈ A_{i}^{[g]}) iff ((g, l) ∈ {g} × ∏_{i=1}^{n} A_{i}^{[g]} = {g} × A^{[g]}). Thus

γ_{cart}A = ⋃_{g∈Glob}({g} × A^{[g]}) .  (1)

For g ∈ Glob, let E^{(g)} = {l | (g, l) ∈ E}. For any g ∈ Glob and B ⊆ Loc^{n} holds:

({g} × B) \ E = {g} × (B \ E^{(g)}) .  (2)

The map

β : Glob × (2^{Loc})^{n} → D^{#}, (g, (B_{i})_{i=1}^{n}) ↦ ({g} × B_{i})_{i=1}^{n}

makes abstract elements from Cartesian abstract elements and is computable in polynomial time. For any B ⊆ Loc^{n} holds:

α_{cart}({g} × B) = ({(g, l_{i}) | l ∈ B})_{i=1}^{n} = ({g} × π_{i}B)_{i=1}^{n} = β(g, α_{c}B) . (3)

Now

α_{cart}(E^{c} ∩ γ_{cart}A) =^{(1)} α_{cart}(E^{c} ∩ ⋃_{g∈Glob}({g} × A^{[g]})) = [distributivity]

α_{cart}( ⋃_{g∈Glob}(({g} × A^{[g]}) \ E)) = [abstraction map is a join-morphism]

⨆_{g∈Glob} α_{cart}(({g} × A^{[g]}) \ E) =^{(2)} ⨆_{g∈Glob} α_{cart}({g} × (A^{[g]} \ E^{(g)})) =^{(3)}

⨆_{g∈Glob} β(g, α_{c}((γ_{c}(A_{i}^{[g]})_{i=1}^{n}) \ E^{(g)})) .

From Prop. 20 we know that α_{c}((γ_{c}(A_{i}^{[g]})_{i=1}^{n}) \ E^{(g)}) is computable in polynomial time in n and |Loc| and the maximum cardinality of an antichain; the map β is also polynomial and the abstract join is also polynomial. ⊓ ⊔

Proposition 22. Computing the best abstract post with exceptions takes polynomial time.

Formally: Assume that for E ∈ D, each {l | (g, l) ∈ E} (for g ∈ Glob) is represented as a set of Cartesian abstract elements whose concretizations form a maximized antichain and have {l | (g, l) ∈ E} as the union. Then computing the map

D × D^{#} → D^{#}, (E, A) ↦ post_{E,cart}A

takes polynomial time in n, |Loc|, |Glob| and the maximum size of an antichain from the representation of E.

Proof. Let A := (A_{i})_{i=1}^{n} ∈ D^{#}^{+}. Proceeding as in the proof of Prop. 8 we obtain α_{cart}α_{E}postγ_{E}γ_{cart}A = α_{cart}(E^{c} ∩ postE) ⊔ α_{cart}(E^{c} ∩ postF γ_{cart}A).

In section 4.1 we have shown that F γ_{cart}A = ⋃ γ(F̄A) where F̄A ⊆ D^{#}^{+} has polynomially many elements. So α_{cart}(E^{c} ∩ postF γ_{cart}A) = α_{cart}(⋃{E^{c} ∩ γ_{cart}y | y ∈ F̄A}) = ⨆{α_{cart}(E^{c} ∩ γ_{cart}y) | y ∈ F̄A}, which can be computed in polynomial time by the assumption and Prop. 21.

Now let the representation of E be E = ∪_{g∈Glob}({g} × ⋃ γ_{c}M_{g}) where M_{g} is a set of Cartesian abstract elements so that γ_{c}M_{g} is a maximized antichain and ⋃ γ_{c}M_{g} = {l | (g, l) ∈ E}. Then α_{cart}(E^{c} ∩ postE) = α_{cart}(E^{c} ∩ ∪_{g∈Glob}post({g} × ⋃ γ_{c}M_{g})) = ⨆_{g∈Glob,C∈M_{g}} α_{cart}(E^{c} ∩ post({g} × γ_{c}C)). Repeating the argument from section 4.1 again, we obtain that post({g} × γ_{c}C) is a union of polynomially many elements of D^{+}. Applying assumption and Prop. 21 completes the proof. ⊓ ⊔

Corollary 23. Computing the least abstract fixpoint with exceptional Cartesian abstraction and representation of E so that each {l | (g, l) ∈ Loc} is a union of Cartesian products needs polynomial time.

Formally: Assume that for E ∈ D, each {l | (g, l) ∈ E} (for g ∈ Glob) is represented as a set of Cartesian abstract elements whose concretizations form a maximized antichain and have {l | (g, l) ∈ E} as the union. Then computing the map

D × D → D^{#}, (E, init) ↦ lfp (λX.α_{cart}α_{E}(init ∪ postγ_{E}γ_{cart}X))

needs polynomial time in n, |Loc|, |Glob|, in the cardinality of the largest antichain and in |init|.

Proof. The computation creates elements X^{0} = ⊥, and X^{i+1} = α_{cart}α_{E}init ⊔ post_{E,cart}X^{i}. The part α_{cart}α_{E}init is constant, the part post_{E,cart}X^{i} takes polynomial time to compute by Prop. 22, so each iteration needs polynomial time. The chain length of the abstract domain is n|Glob||Loc| + 1 which makes the number of iterations also polynomial. ⊓ ⊔

Remark that if initial states are represented the same way as the exception set then the run time is polynomial in the cardinality of the largest antichain from the representation of init instead of |init|.

4.4 Low space and low time?

After having seen three different algorithms we ask whether there is an algorithm that needs at most polynomial space (in n, |Loc|, |Glob| and |E|) for the exception set and at most polynomial time (in n, |Loc| and |Glob|). Remembering Prop. 19, we believe that the core of the question lies in the following

Open problem: Is there a unary polynomial p over integers so that for all natural numbers n, d and for each subset B ⊆ (ℕ_{d})^{n} there is an algorithm (a deterministic Turing machine or a deterministic RAM program with a data structure, with logarithmic cost measure and built-in logarithmic cost addition) of size ≤ p(d)^{p(n)} that, in time ≤ p(dn), given an n-tuple (A_{i})_{i=1}^{n} of subsets of ℕ_{d} as an input, answers the question whether ∏_{i=1}^{n} A_{i} ⊆ B ?

5 Examples

Now we present a couple of examples. For better understanding we perform the computation by definition of exceptional abstraction and not along the lines of the polynomial-time algorithms.

5.1 First Thread Waits

Let’s try to prove that the label D never gets reached in the following program:

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:

In the definition of a multithreaded program we required for simplicity that local stores of all threads are equal, so for formal reasons we let the local variable be the program counter pc taking values from {A, B, C, D, E, F, G}.

Choosing the empty exception set E = ∅ leads to A = lfp (λX.α_{cart}(init ∪ postγ_{cart}X)) = ({0A, 1A, 0B, 1B, 0C, 1C, 0D, 1D}, {0E, 1F, 0G}), whose concretization γ_{cart}A contains D as a local component of the first thread. Here, the simplified notation XY (e.g. 0A) means the pair of valuation maps ({(g, X)}, {(pc, Y)}). The precision of the Flanagan-Qadeer algorithm (which is equivalent to our approach with the empty exception set) is insufficient.

For comparison we choose the exception set E = {0CG, 0BG}. (It is a shorthand for {({(g, 0)}, {(pc, C)}, {(pc, G)}), ({(g, 0)}, {(pc, B)}, {(pc, G)})}, viewing each state as a tuple of valuation maps.) The initial state is 0AE.

The fixpoint iteration sequence is X^{0} = (∅, ∅) and X^{i+1} = α_{cart}α_{E}init ⊔ α_{cart}((post(E ∪ γ_{cart}X^{i})) \ E) for i ≥ 0:

X^{0} = (∅, ∅)
X^{1} = (\{0A\}, \{0E\}) ⊔ α_{cart} \underbrace{((post\{0CG, 0BG\}) \ \{0CG, 0BG\})}_{∅} = (\{0A\}, \{0E\})

X^{2} = (\{0A\}, \{0E\}) ⊔ α_{cart} \underbrace{((post\{0BG, 0CG, 0AE\}) \ \{OBG, OCG\})}_{\{1AF \}}

= ({0A, 1A}, {0E, 1F })
X^{3} = (\{0A\}, \{0E\}) ⊔ α_{cart} \underbrace{((post\{0BG, 0CG, 0AE, 1AF \}) \ \{OBG, OCG\})}_{\{1AF,1BF,0AG\}}

= ({0A, 1A, 1B}, {0E, 0G, 1F })
X^{4} = (\{0A\}, \{0E\}) ⊔ α_{cart} \underbrace{((post\{0BG, 0CG, 0AE, 0AG, 1AF, 1BF \}) \ \{OBG, OCG\})}_{\{1AF,1BF,0AG\}}

= ({0A, 1A, 1B}, {0E, 0G, 1F })
γ_{E}γ_{cart}X^{3} = {0BG, 0CG, 0AE, 0AG, 1AF, 1BF } .

The concretization of the fixpoint doesn’t contain D as a local state of the first thread, which is what we wanted to prove.

5.2 Mutual Exclusion for One Lock

We give an important large class of multithreaded programs where mutual exclusion can be proven in polynomial time using polynomial space for the exception set.

Consider a multithreaded program with n threads and global variables, one of which is called m, initially 0. Each thread looks like follows: … A: acquire m; … critical section … B: release m; …

where the program satisfies the following criteria:

1. Initial states don’t violate mutual exclusion, i.e. for any initial state there is at most one thread inside its critical section between the locations A and B;

2. The only jumps from inside the critical section to outside or vice versa are the acquire and release statements at A and B;

3. The only transition that sets m to zero is “B: release m”. Statements at program locations other than A or B might vary from thread to thread, include jumps or be missing completely. The statement “acquire m” atomically waits till m = 0 and sets it to some nonzero value. The statement “release m” sets m to zero.

Let (A, B] := {l ∈ Loc | A < l(pc) ≤ B} and (A, B]^{c} = Loc \ (A, B] its complement. Further for 1 ≤ i ≤ n let C(i) = ((A, B]^{c})^{i−1}×(A, B]×((A, B]^{c})^{n−i}.

Proposition 24. The set M = {C(i) | i ∈ ℕ_{n}} is a maximized antichain.

Proof. Let i, j ∈ ℕ_{n} be different and a ∈ C(i)∩C(j). Then a_{i} ∈ (A, B]∩(A, B]^{c} = ∅. So each two Cartesian products in M are disjoint, especially M is an antichain.

Now we show that M is maximized. Let H = ∏_{i=1}^{n} H_{i} ⊆ ⋃ M. Assume for the purpose of contradiction that there is no Cartesian product in M that contains H completely. Since H is contained in the union of M, there should be at least two Cartesian products in M that intersect H, say, H ∩ C(i) ≠ ∅ ≠ H ∩ C(j) for i, j ∈ ℕ_{n} and i ≠ j. Then there are tuples a ∈ H ∩ C(i) and b ∈ H ∩ C(j). We have a_{i} ∈ (A, B], b_{j} ∈ (A, B] and b_{j} ∈ H_{j}. Let ã = (a \ {(j, a_{j})}) ∪ {(j, b_{j})}. Then ã ∈ H. But (ã)_{i} ∈ (A, B] and (ã)_{j} ∈ (A, B] and i ≠ j, so ã ∉ C(k) for any k ∈ ℕ_{n}, in contradiction to H ⊆ ⋃_{k∈ℕ_{n}} C(k). ⊓ ⊔

We show that choosing E = ∪_{g∈Glob,g(m)≠0,C∈M}{g} × C as an exception set suffices to prove mutual exclusion. Let R = E ∪ (Glob × ((A, B]^{c})^{n}).

Proposition 25. R is an inductive program invariant, i.e. init ⊆ R and postR ⊆ R.

Proof. By criterion 1 each initial state has either no thread in critical section or at most one thread in critical section. So init ⊆ (Glob × ((A, B]^{c})^{n}) ∪ E = R. Now let (g, l) ∈ R and (g, l) →_{i} (g′, l′). There are several cases.

– Case g(m) = 0, l ∈ ((A, B]^{c})^{n}, l_{i}(pc) = A. Then by definition of acquire g′ ≠ 0 and l′ ∈ (A, B], so (g′, l′) ∈ E.

– Case g(m) ≠ 0, l ∈ ((A, B]^{c})^{n}, l_{i}(pc) = A. Then transition “acquire m” cannot fire, especially (g′, l′) cannot occur due to a step of the ith thread.

– Case l ∈ ((A, B]^{c})^{n}, l_{i}(pc) ≠ A. From criterion 2 follows l′_{i} ∉ (A, B], so (g′, l′) ∈ Glob × ((A, B]^{c})^{n}.

– Case g(m) ≠ 0 and l ∈ C(i) ∈ M, l′_{i} ∈ (A, B]. Then g′(m) ≠ 0 by criterion 3 and (g′, l′) ∈ E.

– Case g(m) ≠ 0 and l ∈ C(i) ∈ M, l′_{i} ∈ (A, B]^{c}. Then (g′, l′) ∈ Glob × ((A, B]^{c})^{n}.

– Case g(m) ≠ 0 and l ∈ C(j) ∈ M, j ≠ i, l′_{i} ∈ (A, B]. From l ∈ C(j) follows l_{i} ∈ (A, B]^{c}. From criterion 2 follows l_{i}(pc) = A and the transition is “acquire m”. But this contradicts to g(m) ≠ 0.

– Case g(m) ≠ 0 and l ∈ C(j) ∈ M, j ≠ i, l′_{i} ∈ (A, B]^{c}. Then l_{i} ∈ (A, B]^{c} and criterion 3 implies g′(m) ≠ 0. So l′ ∈ C(j) and (g′, l′) ∈ E. ⊓ ⊔

Notice that for Y := (Glob×(A, B]^{c})_{i=1}^{n} holds R = γ_{E}γY, so applying Prop. 7 to R, Y and F = init∪post gives γ_{E}γ_{cart}(lfp (λZ.α_{cart}α_{E}(init∪postγ_{E}γ_{cart}Z))) ⊆ R. Since R shows mutual exclusion and the set generated by the parameterized fixpoint computation is a subset of R, mutual exclusion is proven by abstract fixpoint checking parameterized with E. Moreover, all antichains in the representation of E have linear cardinality in n, so the algorithm from section 4.3 run on the “maximized antichains”-representation consumes polynomial time and space. No state explosion occurs.

5.3 Mutual Exclusion for Many Locks

We show how does the exception set look like for programs with a variable number of threads and a variable number of lock variables.

We describe now a class of multithreaded program with n threads and k locks. For simplicity, we number the lock variables by natural numbers. Let Glob = 2^{ℕ_{k}} be the set of global stores. If a set G ∈ Glob is a part of a program state, then in this state exactly the locks in G are held. Let Loc = ℕ_{L} be the set of control locations of each thread. For simplicity, we assume no other local variables except the program counters and no other global variables except locks. The only allowed statements for any thread i are

– “j: acquire lck; j + 1:”, representing all transitions (g, j) →_{i} (g ∪ {lck}, j + 1) where lck ∉ g;

– “j: release lck; j +1:”’, representing all transitions (g, j) →_{i} (g \{lck}, j +1);

– “j: if (ϕ) goto j′; j + 1:”, representing all transitions (g, j) →_{i} (g, j′) where (g, j) satisfies the formula ϕ and all transitions (g, j) →_{i} (g, j + 1) where (g, j) doesn’t satisfy ϕ. Given the program text of a thread, a critical section is a contigious sequence

of control locations that starts right after a statement “acquire lck” and ends just before the next following “release lck” statement, for the same lock variable lck. If there is no following “release lck” statement, the critical section ends at the end of the thread. The lock variable “lck” is said to protect all the locations in this critical section. A program state has the mutual exclusion property if in this state, for every lock, at most one thread is in any of its critical sections protected by this lock. The whole program has the mutual exclusion property if there is no execution that starts in an initial state and ends in a state that violates mutual exclusion. The programs, for which we would like to derive the exception set, should satisfy the following criteria:

1. For any initial state, if a lock variable lck is held, then there is exactly one thread inside some of its critical sections protected by lck, and if it’s not held, there is no thread inside any of its critical sections protected by lck.

2. The only jumps from inside a critical section to outside or vice versa is via the acquire and release statements.

3. Within any thread, for any lck ∈ ℕ_{k} and statement “release lck”, there is a preceding statement “acquire lck” without other “release lck” in between. An example of a thread of such a program is

1: acquire lck_{1}; 2: acquire lck_{2}; 3: release lck_{1}; 4: if (lck_{1}) goto 7; 5: acquire lck_{3}; 6: release lck_{3}; 7:

The description of the program class is finished, now we are going to define the exception set for such a program.

An n-partition of a set X is an tuple of n disjoint subsets of X with union X. For G ∈ Glob, let P_{n}(G) be the set of n-partitions of G. For G ∈ Glob and 1 ≤ i ≤ n, let C(G, i) = {j ∈ Loc | ∀ lck ∈ ℕ_{k} : lck protects j in thread i iff lck ∈ G} be the set of control locations of thread i which are protected by exactly all the locks in G. For each n-partition S = (S_{i})_{1≤i≤n} of a global store, let C(S) = ∏_{i=1}^{n} C(S_{i}, i). For each G ∈ Glob, let M(G) = {C(S) | S ∈ P_{n}(G)} and E(G) = ⋃ M(G). Let the exception set be defined as E = ⋃_{G∈Glob,G≠∅}{G} × E(G). Let N = {∅} × E(∅) and R = E ∪ N.

Lemma 26. The set R is an inductive invariant.

Proof. By criterion 1 each initial state (G, l) ∈ init has either no thread in critical section or, for each lock, there is at most one thread in a critical section protected by this lock. In the first case (G, l) ∈ {∅} × ∏_{i=1}^{n} C(∅, i) = {∅} × C(∅) = N ⊆ R. In the second case let P (i) = {lck ∈ G | lck protects l_{i} in thread i} for all 1 ≤ i ≤ n. If we have P (i) ∩ P (j) ≠ ∅ for some 1 ≤ i, j ≤ n, i ≠ j, then some lck ∈ G would protect both l_{i} and l_{j} in threads i and j, respectively, in contradiction to criterion 1. So P (i) and P (j) are disjoint for different 1 ≤ i, j ≤ n. By the same criterion, each lck ∈ G protects a critical section in some thread 1 ≤ i ≤ n, implying lck ∈ P (i). So (P (i))_{i=1}^{n} is a n-partition of G. Now let 1 ≤ i ≤ n. For all lck ∉ G, neither lck ∈ P (i), nor lck protects l_{i} in thread i. For all lck ∈ G, the fact lck ∈ P (i) is equivalent to lck protecting l_{i} in thread i. So for all lck ∈ ℕ_{n}, the facts lck ∈ P (i) and lck protects l_{i} in thread i are equivalent. This proves l_{i} ∈ C(P (i), i). So l ∈ C((P (i))_{i=1}^{n}) ⊆ E(G). Thus (G, l) ∈ E. We have shown init ⊆ R.

Now let (G, l) ∈ R with a successor (G′, l′). Let i be the thread that contains the statement τ that induced the transition. Let S be a n-partition of G with l ∈ C(S). Case split on τ.

– “l_{i}: acquire lck; l′_{i}:”. So lck ∉ G and G′ = G ∪ {lck}. Let S′_{i} = S_{i} . ∪ {lck} and S′_{j} = S_{j} for j ≠ i. Then S′ = (S_{j})_{j=1}^{n} is a partition of G′. We have l_{i} ∈ C(S_{i}, i), so for all lck′ ∈ ℕ_{k} \ {lck}, we have that lck′ protects l_{i} in thread i if and only if lck′ ∈ S_{i}. Thus for all lck′ ∈ ℕ_{k} \ {lck}, we have that lck′ protects l′_{i} in thread i if and only if lck′ ∈ S′_{i}. We also have that lck′ protects l′_{i} in thread i and lck′ ∈ S′_{i}. So l′_{i} in C(S′_{i}, i). Knowing that l′_{j} = l_{j} ∈ C(S_{j}, j) = C(S′_{j}, j) for j ≠ i, we have l′ ∈ E(G′) and (G′, l′) ∈ E.

– “l_{i}: release lck; l′_{i}:”. So G′ = G \ {lck}. Let S′_{i} = S_{i} \ {lck} and S′_{j} = S_{j} for j ≠ i. If lck ∈ S_{i} then the tuple S′ = (S′_{j})_{j=1}^{n} is a partition of G′. If lck ∈ S_{j} for some j ≠ i, then lck ∉ S_{i}, so l_{i} ∈ C(S_{i}, i) implies that lck doesn’t protect l_{i} in thread i, so there is no critical section for lck ending at l_{i}, thus “release lck” at l_{i} has no preceding “acquire lck”, contradicting criterion 3. If lck ∉ S_{j} for any j ∈ ℕ_{n}, then S′ = S is a partition of G′ = G. So in both cases lck ∈ G and lck ∉ G the tuple S′ is a partition of G′. We have l_{i} ∈ C(S_{i}, i), so for all lck′ ∈ ℕ_{k} \ {lck} we have that lck′ protects l_{i} in thread i if and only if lck′ ∈ S_{i}. Thus for all lck′ ∈ ℕ_{k} \ {lck}, we have that lck′ protects l′_{i} in thread i if and only if lck′ ∈ S′_{i}. Also neither lck protects l′_{i}, nor lck ∈ S′_{i}. So l′_{i} ∈ C(S′_{i}, i). Knowing that l′_{j} = l_{j} ∈ C(S_{j}, j) = C(S′_{j}, j) for j ≠ i, we have l′ ∈ E(G′) and (G′, l′) ∈ R.

– “l_{i}: if(ϕ) goto b; c:”. So G = G′. By criterion 2, no critical section is quit or entered by the jump statement. So we have “∀ lck ∈ ℕ_{k} : lck protects l_{i} in thread i” if and only if “∀ lck ∈ ℕ_{k} : lck protects b in thread i” if and only if “∀ lck ∈ ℕ_{k} : lck protects c in thread i”. Thus l_{i} ∈ C(S_{i}, i) implies b, c ∈ C(S_{i}, i). Knowing that l′_{i} ∈ {b, c} and l′_{j} = l_{j} for j ≠ i, we have l′ ∈ C(S) and thus (G′, l′) ∈ R. ⊓ ⊔

Lemma 27. All states in R satisfy the mutual exclusion property.

Proof. Let (G, l) ∈ R. Then l ∈ C(S) for some n-partition of G, so l_{i} ∈ C(S_{i}, i) for all 1 ≤ i ≤ n. Let lck ∈ ℕ_{k} and i ≠ j be two threads. If lck ∉ G, then lck ∉ S_{i} ∪ S_{j}, so, by definition of C, the lock lck protects neither l_{i} nor l_{j}. If lck is in one of two sets S_{i}, S_{j}, say, in S_{i}, then lck ∉ S_{j}, so lck protects l_{i}, but not l_{j} by definition of C. ⊓ ⊔

Notice that for Y = ({∅} × C(∅, i))_{i=1}^{n} we have γ_{cart}Y = N, so applying Proposition 7 to F = λx. init ∪ post x, R = γ_{E}γY gives us γ_{E}γ_{cart}(lfp (λx . α_{cart}α_{E}(init∪postγ_{E}γ_{cart}x))) ⊆ R. Thus doing thread-modular verification with exception set E proves mutual exclusion.

Lemma 28. For every G ∈ Glob, the set M(G) is a maximized antichain of Cartesian products.

Proof. To show that M(G) is an antichain, let S and S′ be two different npartitions of G. Then there is some component 1 ≤ i ≤ n so that S_{i} ≠ S′_{i}. Without loss of generality, let lck ∈ S_{i} \ S′_{i} (if no such lck exists, swap S and S′). Assume that j ∈ C(S_{i}, i) ∩ C(S′_{i}, i). Since j ∈ C(S_{i}, i) and lck ∈ S_{i}, the lock lck protects j in thread i. Since j ∈ C(S′_{i}, i) and lck ∉ S′_{i}, the lock lck doesn’t protect j in thread i. This is a contradiction, so the assumption was false and C(S_{i}, i) ∩ C(S′_{i}, i) = ∅, proving that C(S) and C(S′) are incomparable with repect to product ordering.

To show that M(G) is maximized, let’s assume the contrary, namely that some Cartesian product C = ∏_{i=1}^{n} C_{i} is a subset of E(G), but not a subset of any C(S) for an n-partition of G. So let C nontrivially intersect C(S) and C(S′) for different S, S′ ∈ P_{n}(G). Let a ∈ C ∩ C(S) and b ∈ C ∩ C(S′). There is a component i ∈ ℕ_{n} in with S_{i} ≠ S′_{i}. We have a_{i} ∈ C(S_{i}, i), but C(S_{i}, i) is disjoint from C(S′_{i}, i), so a_{i} ∉ C(S′_{i}, i). But b_{i} ∈ C(S′_{i}, i). Let a′ = (a\{(i, a_{i})})∪{(i, b_{i})}. Then a′_{i} ∈ C_{i}, so a′ ∈ C. Knowing S_{i} ≠ S′_{i}, there are two cases.

In one case, S′_{i} ⊊ S_{i}. Let d ∈ E(G). Let lck ∈ ℕ_{k} be any lock that protects d_{j} in some thread j ∈ ℕ_{n}. There is a n-partition S′′ of G with d ∈ C(S′′). Then d_{j} ∈ C(S′′_{j}, j). Thus lck ∈ S′′_{j} ⊆ G. On the other hand, let lck ∈ G. There is a n-partition S′′ of G with d ∈ C(S′′). There is a 1 ≤ j ≤ n with lck ∈ S′′_{j}. We have d_{j} ∈ C(S′′_{j}, j). Then lck protects d_{j} in thread j. We have proven that the set of locks that protect components of d ∈ E(G) is exactly G:

{lck ∈ ℕ_{k} | ∃ j ∈ ℕ_{n} : lck protects d_{j} in thread j} = G .

Knowing a ∈ C ⊂ E(G), the components of a are protected by totally |G| locks. From S′_{i} ⊊ S_{i}, a′_{i} = b_{i} ∈ C(S′_{i}, i) and a_{i} ∈ C(S_{i}, i), we follow that the set of locks that protect a′_{i} in thread i is strictly smaller than the set of locks that protect a_{i} in thread i. For other threads j ≠ i, the set of locks that protect a_{j} = a′_{j}, is S_{j}, which is disjoint from S_{i}. So a′ is protected by less locks than a, thus, using our claim, a′ ∉ E(G). It’s a contradiction to a′ ∈ C ⊆ E(G).

In another case S′_{i} \ S_{i} ≠ ∅. Since S and S′ both have G as a union, there is some component j ≠ i so that S_{j} contains at least one lock, say, lck, from S′_{i} \S_{i}. So a′_{j} = a_{j} ∈ C(S_{j}, j) is protected by lck. But lck ∈ S′_{i} and a′_{i} = b_{i} ∈ C(S′_{i}, j), so a′_{i} is protected by lck also. But any element d ∈ E(G) has the property that for different components ī, ī′, the locations dī and dī′ are protected by disjoint sets of locks. This property doesn’t hold for a′, so a′ ∉ E(G), in contradiction to a′ ∈ C ⊆ E(G). ⊓ ⊔

Lemma 29. On a RAM with logarithmic cost measure, the representation of the exception set E as a list of antichains of Cartesian products, one antichain per global part, needs space O(nL(n + 1)^{k}).

Proof. We have |M(G)| = ∑_{k_{1}+...+k_{n}=|G|} \binom{|G|}{k_{1},...,k_{n}} = n^{|G|}. For storing a Cartesian product C(S) for any partition S, we need Ln memory cells, storing each component as a bitvector, using one bit per addressed memory cell. The consumed space per Cartesian product is thus Ln. Storing M(G) as an array needs |M(G)|Ln + log(|M(G)|) = n^{|G|+1}L + |G| log n space. All such arrays, for each G ∈ Glob \ {∅}, stored again as an array, need the following space :

∑_{G∈Glob,G≠∅}(n^{|G|+1}L + |G| log n) + log(Glob − 1) =

=nL( ∑_{ℕ_{k}⊇G≠∅} n^{|G|} + log n ∑_{∅≠G⊆ℕ_{k}}|G|) + log(2^{k} − 1) ≤
≤nL((n + 1)^{k} − 1 + (log n)(2^{k} − 1)) + k ≤ nL((n + 1)^{k} + (log n)^{k}2^{k}) + k =
=nL((n + 1)^{k} + (2 log n)^{k}) + k ≤ nL((n + 1)^{k} + (n + 1)^{k}) + k ≤ 3nL(n + 1)^{k}.
⊓ ⊔

For a constant number of locks, and a variable number of threads, the exception set still needs polynomial space, and thus allows computing the abstract fixpoint in polynomial time in the number of threads.

6 Experiments and Implementation

6.1 Experiments

We have experimented with the algorithm from Corollary 23. We run it on the example 5.2, where each thread consists of an acquire and a release statement but nothing else. Computing the best invariant with the usual forward search needed several hours for 18 threads, with run time growing exponentially with base 3. Thread-modular algorithm needed half a minute for a program of 30 threads; its run time grew at most in cubic time. Given the absolutely unoptimized implementation, small efforts to keep it going and excellent run times, we expect that this method to have a much greater potential than it shows now.

6.2 Towards an Implementation

Now we talk about practical aspects of a serious (non-experimental) implementation.

The current proof of Thm. 9 relies on the use of decision diagrams, each of them has in general exponential size in the measure of the domain, since it can have up to 2^{m} leaves, for example if the exception element is the bottom of the lattice (E = ∅). To deal with this issue one can use the usual methods like generating each bit of the answer alone, using m diagrams instead of one, a diagram for a bit of answer. This enables a vast amount of sharing isomorphic subgraphs in the diagrams, e.g. for E = ∅ the m diagrams compute projections on each of m positions in a bitstring, so each of the diagrams would have linear number of nodes in the number of variables m, thus reducing the size of the data structure from exponential to polynomial.

Attention should also be payed to generating these binary decision diagrams. We suggest doing it on-the-fly, i.e. given the representation of the exception set as a list of tuples or as a set of Cartesian products, we suggest the low-space algorithm at the first iteration. Then the results of the involved computations of {0, 1}^{m} → {0, 1}^{m} , v ↦ ϕα_{cart}((γ_{cart}ϕ^{−1}v) \ E) (where ϕ and ϕ^{−1} convert abstract elements to and from the binary representations) get cached in the decision diagrams, each of which allows three outcomes 0, 1 and “don’t know”. In the following iterations, first a lookup in these decision diagrams is done and then, if it returns “don’t know”, the low-space algorithm with the usual representation of the exception set is started. More caching is possible as follows. Notice that the above map is monotone wtih respect to product order. It’s possible to derive the value of a monotone map f : {0, 1}^{m} → {0, 1} on some x ∈ {0, 1}^{m}, if it’s known that either f(x′) = 1 for some x′ < x or f(x′) = 0 for some x′ > x. There is a representation of monotone maps, based on the results of Kleitmann and Markowsky on the Dedekind’s problem, that allows doing poly-time queries with derivation of some (not all derivable) values.

7 Other directions

The parameter can be chosen arbitrarily for Cartesian abstraction. However, some values of the parameter give you a precise answer and some don’t. In this article we don’t address the issue of how to find a value of the parameter that suits for a specific verification task.

8 Related work

The term “Cartesian abstraction” is also known as “independent attribute method” for more than 25 years (see [10]) in program analysis. To the best of our knowledge, it is unknown in its current form in analysis of multithreaded programs.

Thread-modular verification, inspired by assume-guarantee reasoning, was suggested by Flanagan and Qadeer in [5]: they use the same model of multithreaded programs as we do. Their algorithm for proving safety was a starting point of our research.

Henziger and al. adapted the Flanagan-Qadeer algorithm to the BLAST verification tool (see [7]) by combining with abstraction refinement of the transition relation of threads.

In [11] the authors discovered the relationship between the thread-modular algorithm and Cartesian abstract interpretation in the special setting of multithreaded programs. They gave an abstract lattice and a Galois-connection so that the algorithm computation could be formulated as abstract fixpoint checking in the abstract lattice. Comparing that abstraction to the parameterized Cartesian abstraction, one can show that if the exception set is empty, then the parameterized Cartesian successor operator post_{∅,cart}^{#} is exactly the abstract post from [11]. So parameterized Cartesian post is a parameterized version of Cartesian post. In [11] the authors also gave an approximation operator on the concrete lattice so that the Flanagan-Qadeer algorithm has an equivalent formulation in terms of fixpoint checking on the concrete lattice. Two polynomial-time techniques based solely on Cartesian abstraction were presented that increased the precision of the abstraction for some important classes of programs. But these techniques had fixed precision and thus remained incomplete. In contradiction, the parameterized Cartesian abstraction can show every provable non-reachability property by a judicious choice of the parameter.

Giacobazzi and Ranzato develop the theory of complete abstract interpretation in [6]. We would like to exploit connections to that theory, including connections to a recent work of Dave Schmidt [15].

9 Conclusion

We have examined the problem of proving non-reachability in multithreaded programs. We suggested an algorithm based on Cartesian abstraction whose precision can be altered by a parameter, namely by the exception set, which contains program states that are not going to be involved into Cartesian abstraction. The parameterized algorithm takes time which is polynomial in the number of threads, while the choice of parameter allows successor computation with arbitrary precision. We discovered a time-space tradeoff for the abstract fixpoint computation. The larger the exception set is (as long as it is included in the set of reachable states), the more precise the successor computation is going to be. In the limit case, if the set contains exactly the reachable states of the program, no overapproximation happens. We formalized our approach in the abstract interpretation framework. We showed a large class of programs that allow checking mutual exclusion in polynomial time and space. We discussed some aspects of possible practical implementation.

References

1. Blanchet, B., Introduction to Abstract Interpretation, 2002, lecture script,

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

2. Cousot, P., Cousot, R., Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs By Construction or Approximation of Fixpoints, fourth ACM symposium on principles of programming languages, 1977.

3. Cousot, P., Cousot, R., Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation, in Conference Record of FPCA ’95 SIG-PLAN/SIGARCH/WG2.8 Conference on Functional Programming and Computer Architecture, pp. 170–181, La Jolla, California, U.S.A., 25–28 June 1995, ACM Press, New York, U.S.A.

4. Cousot, P., Partial Completeness of the Abstract Fixpoint checking, SARA 2000, LNAI 1864, pp. 1–25, 2000.

5. Flanagan, C., and Qadeer, S., Thread-Modular Model Checking, in T.Ball and S.K. Rajamani (Eds.): SPIN 2003, LNCS 2648, pp. 213–224, 2003, Springer-Verlag Berlin Heidelberg 2003.

6. Giacobazzi, R., Ranzato, F., Making Abstract Interpretations Complete, JACM, 1997.

7. Henzinger, T. A., Jhala, R., Majumdar, R., Qadeer, S., Thread-modular abstraction refinement, 15th Conference on Computer-Aided Verification, 2003.

8. Holzmann, G., The Model Checker Spin, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279–295.

9. Kozen, D., Lower Bounds for Natural Proof Systems, FOCS 1977, pp. 261–262.

10. Jones, N. D., Muchnick, S. S., Complexity of Flow Analysis, Inductive Assertion Synthesis, and a Language Due to Dijkstra, in Program Flow Analysis, theory and applications, Eds. Steven S. Muchnick and Neil D. Jones, Prentice-Hall, Inc., Englewood Cliffs, New Jersey 07632, 1981.

11. Malkis, A., Podelski, A., Rybalchenko, A., Thread-Modular Verification and Cartesian Abstraction, presented at the Thread Verification workshop, Seattle, 21–22 August 2006.

12. Malkis, A., Podelski, A., Rybalchenko, A., Thread-Modular Verification Is Cartesian Abstract Interpretation, 3rd International Colloquium on Theoretical Aspects of Computing, Tunis, Tunisia, 20–24 November 2006.

13. Mehlhorn, K., Data Structures and Algorithms 1: Sorting and searching, Springer-Verlag Berlin Heidelberg, 1984.

14. Oberschelp, A., Allgemeine Mengenlehre, Bibliographisches Institut & F.A. Brockhaus AG, Mannheim 1994

15. Schmidt, D., Comparing completeness properties of static analyses and their logics, APLAS’06, Springer LNCS 4279, pp. 183–199.

16. Tarski, A., A Lattice-theoretical Fixpoint Theorem and Its Applications, Pacific J. Math. 5 (1955), 285–309.