Sharing Revisited

Roberto Bagnara^{∗}

       bagnara@scs.leeds.ac.uk

Patricia M. Hill^{∗}

                                  hill@scs.leeds.ac.uk

Enea Zaffanella^{†}

              zaffanella@elektra.casa.unimo.it

Abstract Although the usual goal of sharing analysis is to detect which pairs of variables share, the standard choice for sharing analysis is a domain that characterizes setsharing. In this paper, we question, apparently for the first time, whether this domain is over-complex for pair-sharing analysis. We show that the answer is yes. By defining an equivalence relation over the set-sharing domain we obtain a simpler domain, reducing the complexity of the abstract unification procedure. We present preliminary experimental results, showing that, in practice, our domain compares favorably with the set-sharing one over a wide range of benchmark programs.

1 Introduction

In logic programming, a knowledge of sharing between variables is important for optimizations such as the exploitation of parallelism. Today, talking about sharing analysis for logic programs is almost the same as talking about the set-sharing domain Sharing of Jacobs and Langen [12, 13]. The adequacy of this domain is not normally questioned. Researchers appear to be more concerned as to which add-ons are best: linearity, freeness, depth-k abstract substitutions and so on [3, 4, 5, 14, 15, 17] rather than whether it is the optimal domain for the sharing information under investigation.

What is the reason for this “standard” choice? Well, the set-sharing domain is quite accurate: when integrated with linearity information it is strictly more precise than its old challenger, the pair-sharing domain ASub of Søndergaard [18]. Indeed, Sharing encodes a lot of information. As a consequence, it is quite difficult to understand: taking an abstract element and writing down its concretization (namely, the concrete substitutions that are approximated by it) is a hard task. So the question arises: is this complexity actually needed for an accurate sharing analysis?

Before answering this question we must agree on what the purpose of sharing analysis is. This paper relies on the following

Assumption: The goal of sharing analysis for logic programs is to detect which pairs of variables are definitely independent (namely, they cannot be bound to terms having one or more variables in common).

As far as we know, this assumption is true. In the literature we can find no reference to the “independence of a set of variables”. All the proposed applications of sharing analysis (compile-time optimizations, occur-check reduction and so on) are based on information about the independence of pairs of variables.

∗School of Computer Studies, University of Leeds, Leeds, LS2 9JT, U.K. The work of R. Bagnara and P. M. Hill has been supported by EPSRC under grant GR/L19515.

†Servizio IX Automazione, Università degli Studi di Modena, and Dipartimento di Informatica, Università di Pisa, Italy.

We thus focus our attention on the pair-sharing property and assume that set-sharing is just a way to compute pair-sharing with a higher degree of accuracy: there may well be other ways. In this paper we question, apparently for the first time, whether the Sharing domain is really the best one for detecting which pairs of variables can share. The answer turns out to be negative: there exists a domain that is simpler than Sharing and, at the same time, is as precise as Sharing, as far as pair-sharing is concerned. This domain is the subject of this paper.

The paper is organized as follows. In the next section, we introduce the notation and recall the definition of the abstract domain Sharing. In Section 3, we show that Sharing is unnecessarily complex for capturing pair-sharing information. A new equivalence relation between its elements is defined which is shown to exactly factor out the unwanted information. Section 4 explains the practical consequences of these results and shows that the complexity of abstract unification using our domain is polynomial compared to the exponential complexity for Sharing. Section 5 gives the experimental results and Section 6 concludes the paper. The proofs of the presented results can be found in [2].

2 Preliminaries

In this section we introduce some mathematical notation that will be used throughout the paper, as well as recalling the set-sharing domain.

2.1 Notation

For a set S, # S is the cardinality of S, ℘(S) is the powerset of S, whereas ℘_{f}(S) is the set of all the finite subsets of S. The symbol Vars denotes a denumerable set of variables, whereas T_{Vars} denotes the set of first-order terms over Vars. The set of variables occurring in a syntactic object o is denoted by vars(o). A substitution σ is a total function σ: Vars → T_{Vars} that is the identity almost everywhere; in other words, the domain of σ, dom(σ) =^{def} { x ∈ Vars | σ(x) ≠ x }, is finite. Substitutions are denoted by the set of their bindings, thus σ is identified with { x ↦ σ(x) | x ∈ dom(σ) }. A substitution σ is idempotent if vars(σ(x)) ∩ dom(σ) = ∅ for each x ∈ dom(σ). The set of all the idempotent substitutions is denoted by Subst.

2.2 The Sharing Domain

The Sharing domain is due to Jacobs and Langen [12].

Definition 1 (The set-sharing lattice.) Let^{1}

SG =^{def} { S ∈ ℘_{f}(Vars) | S ≠ ∅ }

1The literature on Sharing is almost unanimous in defining sharing-sets so that they always contain the empty set. We deviate from this de facto standard: in our approach sharing-sets never contain the empty set. We do this because (1) there is no real need of having ∅ and ⊆ as the bottom element and the ordering of the domain, respectively (the original motivation for including the empty set in each sharing-set); (2) the definitions turn out to be easier; and (3) we describe the implementation (where the empty set never appears in sharing-sets) more faithfully.

and let SH =^{def} ℘(SG). The set-sharing lattice is given by the set

SS =^{def} { (sh, U) | sh ∈ SH , U ∈ ℘_{f}(Vars), ∀S ∈ sh : S ⊆ U } ∪ {⊥, ⊤}

ordered by ⪯_{SS} defined as follows, for each d, (sh_{1}, U_{1}), (sh_{2}, U_{2}) ∈ SS:

⊥ ⪯_{SS} d,
d ⪯_{SS} ⊤,
(sh_{1}, U_{1}) ⪯_{SS} (sh_{2}, U_{2}) ⟺ (U_{1} = U_{2}) ∧ (sh_{1} ⊆ sh_{2}).

It is straightforward to see that every subset of SS has a least upper bound with respect to ⪯_{SS}. Hence SS is a complete lattice.

Before introducing the abstract operations over SH we need some ancillary definitions.

Definition 2 (Auxiliary functions.) The closure under union function (·)^{⋆}: SH → SH (also called star-union) is given, for each sh ∈ SH , by

sh^{⋆} =^{def} { S ∈ SG | ∃n ≥ 1 . ∃T_{1}, …, T_{n} ∈ sh . S = T_{1} ∪ ⋯ ∪ T_{n} }.

For each sh ∈ SH and each T ∈ ℘_{f}(Vars), the operation of extracting the relevant component of s with respect to T is encoded by the function rel: ℘_{f}(Vars) × SH → SH defined as

rel(T, sh) =^{def} { S ∈ sh | S ∩ T ≠ ∅ }.

For each sh_{1}, sh_{2} ∈ SH , the binary union function bin: SH × SH → SH is given by

bin(sh_{1}, sh_{2}) =^{def} { S_{1} ∪ S_{2} | S_{1} ∈ sh_{1}, S_{2} ∈ sh_{2} }.

The function proj: SH ×℘_{f}(Vars) → SH projects an element of SH onto a set of variables of interest: if sh ∈ SH and V ∈ ℘_{f}(Vars), then

proj(sh, V) =^{def} { S ∩ V | S ∈ sh, S ∩ V ≠ ∅ }.

The auxiliary function amgu captures the effects of a binding x ↦ t onto an SH element. Let x be a variable and t a term in which x does not occur. Let also sh ∈ SH and

A =^{def} rel({x}, sh),
B =^{def} rel(vars(t), sh).

Then

amgu(sh, x ↦ t) =^{def} (sh \ (A ∪ B)) ∪ bin(A^{⋆}, B^{⋆}).

It is shown in [16] that amgu is both commutative and idempotent. Thus we can define the extension amgu: SH × Subst → SH by

amgu(sh, ∅) =^{def} sh,
amgu(sh, {x ↦ t} ∪ σ) =^{def} amgu(amgu(sh, x ↦ t), σ \ {x ↦ t}).

The Sharing domain is given by the complete lattice SS together with the following abstract operations needed for the analysis. Trivial operations, such as consistent renaming of variables, are omitted.

Definition 3 (Abstract operations over SS.) The lub operation over SS is given by the function ⊔: SS × SS → SS defined as follows, for each d, (sh_{1}, U_{1}), (sh_{2}, U_{2}) ∈ SS:

⊥ ⊔ d =^{def} d ⊔ ⊥ =^{def} d,
⊤ ⊔ d =^{def} d ⊔ ⊤ =^{def} ⊤,
(sh_{1}, U_{1}) ⊔ (sh_{2}, U_{2}) =^{def} \{ \begin{matrix}(sh_{1} ∪ sh_{2}, U_{1}), & if U_{1} = U_{2}; \\ ⊤, & otherwise. \end{matrix}

The projection function Proj: SS × ℘_{f}(Vars) → SS is given, for each set of variables of interest V ∈ ℘_{f}(Vars) and each description (sh, U) ∈ SS, by

Proj(⊥, V) =^{def} ⊥,
Proj(⊤, V) =^{def} ⊤,
Proj((sh, U), V ) =^{def} (proj(sh, V), U ∩ V ).

The operation Amgu: SS × Subst → SS extends the SS description it takes as an argument, to the set of variables occurring in the substitution it is given as the second argument. Then it applies amgu:

Amgu((sh, U), σ) =^{def} (amgu(sh ∪ { {x} | x ∈ vars(σ) \ U }, σ), U ∪ vars(σ)).

For the distinguished elements ⊥ and ⊤ of SS we have^{2}

Amgu(⊥, σ) =^{def} ⊥,
Amgu(⊤, σ) =^{def} ⊤.  (1)

3 Sharing is Redundant for Pair-Sharing

3.1 The Pair-Sharing Property

Let us define the pair-sharing property through a domain that captures it exactly. This domain is similar to Søndergaard’s ASub (but without the groundness and linearity information) [18].

Definition 4 (The pair-sharing domain.) Let S be a set. Then

pairs(S) =^{def} { P ∈ ℘(S) | # P = 2 }.

The pair-sharing domain is given by the complete lattice

PS =^{def} { (ps, U) | U ∈ ℘_{f}(Vars), ps ∈ ℘(pairs(U)) } ∪ {⊥, ⊤}

2Notice that the only reason we have ⊤ ∈ SS is in order to turn SS into a lattice rather than a CPO.

As the description ⊤ is never used in the analysis, Equation 1 is only provided for completeness.

ordered by ⪯_{PS}, which is defined, for each d, (ps_{1}, U_{1}), (ps_{2}, U_{2}) ∈ PS, by

⊥ ⪯_{PS} d,
d ⪯_{PS} ⊤,
(ps_{1}, U_{1}) ⪯_{PS} (ps_{2}, U_{2}) ⟺ (U_{1} = U_{2}) ∧ (ps_{1} ⊆ ps_{2}).

Clearly, PS is a strict abstraction of SS through the abstraction function α_{PS} : SS → PS given, for each (sh, U) ∈ SS, by

α_{PS}(⊥) =^{def} ⊥,
α_{PS}(⊤) =^{def} ⊤,
α_{PS}((sh, U)) =^{def} (Down(sh) ∩ pairs(Vars), U),

where

Down(sh) =^{def} { S ∈ ℘(Vars) | ∃T ∈ sh . S ⊆ T }.

An element of the pair-sharing domain is, roughly speaking, the “end-user image” of the result of the analysis. That is, the only interest of the end-user of our analysis (e.g., the optimizer module of the compiler) is knowing which pairs of variables possibly share. The PS domain will be used to measure the accuracy of the other domains in computing pair-sharing.

3.2 What is in Sharing

We now look at the information content of the elements of the Sharing domain. We refer the reader to, e.g., [6] for a formal definition of the concretization function γ: SS → Subst × ℘_{f}(Vars).

As it has been observed by several authors, the SS lattice encodes several properties, besides pair-sharing. We present them here by means of examples that show their usefulness. In what follows, the set of variables of interest is fixed as U =^{def} {x, y, z} and will be omitted from elements of SS. Moreover, the elements of SH will be written in a simplified notation, omitting the inner braces. For example, ({{x}, {x, y}, {x, z}}, {x, y, z}) will be written simply as {x, xy, xz}.

Groundness. Consider sh_{1} =^{def} {xy} and sh_{2} =^{def} {xy, z}. They encode the same pairsharing information, namely α_{PS}(sh_{1}) = α_{PS}(sh_{2}) = {xy}. In sh_{1} we know that the variable z is ground. This knowledge is useful for pair-sharing detection:

α_{PS}(amgu(sh_{1}, x ↦ z)) = ∅,
α_{PS}(amgu(sh_{2}, x ↦ z)) = α_{PS}({xyz}) = {xy, xz, yz}.

Ground dependencies. Let sh_{1} =^{def} {xy, xyz, z} and sh_{2} =^{def} {xy, xz, yz, z}. Again, they encode the same pair-sharing information. They also encode the same groundness information (no variable is ground). However, in sh_{1} the groundness of y depends on the groundness of x. Let us ground x and see what happens:

α_{PS}(amgu(sh_{1}, x ↦ a)) = ∅,
α_{PS}(amgu(sh_{2}, x ↦ a)) = α_{PS}({yz}) = {yz}.

Sharing dependencies. This example is taken from [6]. Let

sh_{1} =^{def} {x, y, z, xyz},
sh_{2} =^{def} {x, y, z, xy, xz, yz}.

They encode the same pair-sharing, groundness, and ground dependency information. Again, let us ground x and look at the results:

α_{PS}(amgu(sh_{1}, x ↦ a)) = α_{PS}({y, z}) = ∅,
α_{PS}(amgu(sh_{2}, x ↦ a)) = α_{PS}({y, z, yz}) = {yz}.

In sh_{1} the sharing between y and z depends on the (non-) groundness of x, while in sh_{2} this is not the case.

Given these three examples, one gets the impression that different elements in SH do encode different information with respect to the pair-sharing property. However, this is not always the case. Consider

sh_{1} =^{def} {x, y, z, xy, xz, yz},
sh_{2} =^{def} {x, y, z, xy, xz, yz, xyz}.

These two different elements do encode the same pair-sharing, groundness, ground dependency, and sharing dependency information. Since the set of variables of interest is U = {x, y, z}, we can observe that γ((sh_{2}, U)) = (Subst, U) What does γ((sh_{1}, U)) look like? The only relevant information in sh_{1} is that the sharing group xyz is not allowed: sh_{1} represents all the idempotent substitutions σ such that

vars(σ(x)) ∩ vars(σ(y)) ∩ vars(σ(z)) = ∅.

That is, the variables x, y, and z cannot share the same variable (but they still can share pairwise). As observed before, this difference is irrelevant from the end-user point of view. Therefore, we want to show that sh_{1} and sh_{2} are completely equivalent with respect to the pair-sharing property. This is the same as saying that the sharing group xyz is “useless” in sh_{2} and can be dropped.

Definition 5 (Redundancy.) Let sh ∈ SH and S ∈ SG. S is redundant for sh if and only if # S > 2 and

pairs(S) = ⋃{ pairs(T) | T ∈ sh, T ⊂ S }.

Read it this way: S is redundant for sh if and only if all its sharing pairs can be extracted from the elements of sh that are smaller than S. As the name suggests, redundant sharing groups can be dropped. For the moment, as we are walking on a theoretical ground, we add them so to obtain a sort of normal form. We thus define an upper closure operator over SH that induces an equivalence relation over the elements of SH .

Definition 6 (A closure operator on SH .) The function ρ: SH → SH is given, for each sh ∈ SH , by

ρ(sh) =^{def} sh ∪ { S ∈ SG | S is redundant for sh }.

A set S can be added to a sharing set sh without changing the pair-sharing information only if, for each variable x in S, every pair such as xy, is already in an element in sh. Thus S must be the union of sets in sh that contain x. This observation leads to the following alternative definition for ρ.

Theorem 7 If sh ∈ SH then

ρ(sh) = { S ∈ SG | ∀x ∈ S : S ∈ rel({x}, sh)^{⋆} }.

While the original definition refers directly to the pair-sharing concept, the alternative definition provided by Theorem 7 is very elegant and concise, and turns out to be useful for proving several results.

Abusing notation, we can easily define the overloading ρ: SS → SS such that

ρ(⊥) =^{def} ⊥,
ρ(⊤) =^{def} ⊤,
ρ((sh, U)) =^{def} (ρ(sh), U).

We have thus implicitly defined a new domain that, for lack of a better name, we will call X. The domain X is the quotient of SS with respect to the equivalence relation induced by ρ: d_{1} and d_{2} are equivalent if and only if ρ(d_{1}) = ρ(d_{2}). Clearly, X is a proper abstraction of SS.

It is straightforward to prove the following

Proposition 8 For each d ∈ SS we have α_{PS}(ρ(d)) = α_{PS}(d).

Thus the addition of redundant elements does not cause any precision loss, as far as pairsharing is concerned. In other words, X is as good as SS for representing pair-sharing. Now we show that ρ is a congruence with respect to the operations Amgu, ⊔, and Proj.

Theorem 9 Let d_{1}, d_{2} ∈ SS. If ρ(d_{1}) = ρ(d_{2}) then, for each σ ∈ Subst, each d′ ∈ SS, and each V ∈ ℘_{f}(Vars),

1. ρ(Amgu(d_{1}, σ)) = ρ(Amgu(d_{2}, σ));

2. ρ(d′ ⊔ d_{1}) = ρ(d′ ⊔ d_{2}); and

3. ρ(Proj(d_{1}, V)) = ρ(Proj(d_{2}, V)).

As a corollary of the two results above we have that X is as good as SS for propagating pair-sharing through the analysis process. Not only that. We show that any proper abstraction of X is less precise than X on computing pair-sharing.

Theorem 10 For each d_{1}, d_{2} ∈ SS, ρ(d_{1}) ≠ ρ(d_{2}) implies

∃σ ∈ Subst . α_{PS}(Amgu(d_{1}, σ)) ≠ α_{PS}(Amgu(d_{2}, σ)).

To summarize, the equivalence relation induced by ρ identifies two elements if and only if their behavior in the analysis process is indistinguishable with respect to the pair-sharing property. As a final remark, the technique we use to “extract” from SS the component that is relevant in order to compute pair-sharing is very similar to the one introduced by Cortesi, Filé, and Winsborough in [7], even though the formal definitions are slightly different.

4 Star-union is not needed

The theory developed in the previous section has at least one practical consequence: in the definition of the abstract unification for domain X, the star-union operator can be safely replaced by the binary-union operator.

Theorem 11 For each sh ∈ SH we have sh^{⋆} = ρ(bin(sh, sh)).

In our opinion, this is a very important result of this research. In the worst-case, the complexity of the star-union operator is exponential in the number of sharing groups of the input, while for the binary-union operator the complexity is quadratic.

Notice that the complexity improvement provided by Theorem 11 comes at a price. In order to test for fixpoint on X, we cannot perform a simple identity check, because two syntactically different elements can be mapped onto the same element by ρ: a suitable equivalence test is needed. In the worst case, the complexity of this test is bounded by the square of the number of sharing groups, but it is our opinion that it can be implemented quite efficiently (that is, more efficiently than in our current prototype implementation). This brings us to the next section.

5 Experimental Evaluation

The ideas presented in this paper have been experimentally validated in the context of the development of the China analyzer [1]. China is a data-flow analyzer for CLP(H_{N}) languages (i.e., Prolog, CLP(R), clp(FD) and so forth), H_{N} being an extended Herbrand system where the values of a numeric domain N can occur as leaves of the terms. China, which is written in C^{++} and Prolog, performs bottom-up analysis deriving information on both call- and success-patterns by means of program transformations and optimized fixpoint computation techniques.

We have analyzed several programs using composite domains of the kind Pattern(D), where D is one of our analysis domains and Pattern(·) [1] is a generic structural domain similar to Pat(ℜ) [8, 9]. The construction Pattern(·) upgrades a domain D (which must support a certain set of basic operations) with structural information. The resulting domain, where structural information is retained to some extent, is usually much more precise then D alone. Of course, there is a price to be paid: in the analysis based on Pattern(D), the elements of D that are to be manipulated are often bigger (i.e., they consider more variables) that those that arise in analyses that are simply based on D. The domains D that we have tried are: straight sharing à la Jacobs and Langen (SS), the domain X where star-union has been replaced by binary-union (X), and the same domain where all the elements are always maximally reduced, that is, they do not contain any redundant sharing-group (X + red), plus all the possible combinations of the three domains above with domains for linearity and freeness. These combinations have been performed following [4].

The experimental results are reported in Tables 1 and 2. Table 1 refers to our three sharing domains either taken alone or in combination with the linearity domain. The result of adding the freeness domain to such combinations is depicted in Table 2. The tables give the analysis time of each program.^{3} The computation times have been taken

3The current test-suite of China comprises more than 160 programs. Here we give the results only for those programs whose analysis time using Pattern(SS) (without linearity) are above a certain threshold.

Notice also that Tables 1 and 2 are sorted on the analysis time with Pattern(SS).

Without freeness

Without linearity  With linearity
Program  SS  X  X + red  SS  X  X + red
Life  0.89  0.6  0.67  0.55  0.55  0.61
Kalah  1.28  1.08  1.09  1.15  1.16  1.19
NRev  1.41  0.67  0.54  0.05  0.05  0.04
Queens  2.22  1.21  0.87  0.06  0.06  0.07
Meta Qsort  2.97  1.35  1.08  1.47  0.95  1.27
Neural  3.37  1.99  1.21  0.99  0.99  1.01
Mastermind  3.39  2.38  2.64  2.19  2.18  2.26
Browse  3.78  2.14  2.01  1.15  0.9  1.06
Disj  6.34  5.54  5.57  7.44  7.47  7.47
DNF  7.56  6.85  6.8  11.14 11.2  11.31
Boyer  8.93  5.07  2.65  7.8  5.31  2.3
SCC  10.16  7.39  7.56  9.9  8.98  9.49
Gabriel  14.11  7.38  4.33  11.57  6.74  3.58
CS  16.64 14.03  14.33  29.13 27.74 28.31
N and C  19.63 10.9  10.3  2.02  1.98  2.45
Palindrome 22.61 12.59  4.58  0.27  0.26  0.33
Zebra  28.29 26.56  28.14  29.58 29.63 31.5
Treeorder 177.01 105.29  35.46 115.97 78.28 19.84
Peep  258.64 145.01  48.41 117.09 76.77 27.17
Parser DCG 496.3 316.87  79.75  21.33 18.88 24.57
Read  882.83 555.85 104.06 101.46 63.37 32.71
R on P  ∞  ∞  ∞  2.67  2.69  6.65

Table 1: Experimental results obtained with the China analyzer.

on a Pentium90 machine with 24 MB of RAM running Linux 2.0.29, and the timings are in seconds of user time as provided by the getrusage system call. Many of the tested programs have become more or less standard for the evaluation of data-flow analyzers. Notice that for these tests we have switched off all the other domains currently supported by China^{4}, as well as all the mechanisms, such as widenings, that are used to throttle the complexity of the analysis.

First of all, the results indicate that, from a practical point of view, analyses based on Sharing without linearity or freeness do not make any sense: while the overhead for keeping track of these additional properties is quite small, the number of star-unions that can be avoided thanks to the extra information obtained allow for consistent, and sometimes huge, speedups (not to count the increased precision). Exceptions to this rule, such as in the case of the programs Disj, N and C, and Zebra are quite rare, and the slowdown involved is always of modest entity. This fact has already been remarked (see, e.g., [14]).

4Numerical bounds and relations, groundness, and polymorphic types.

With freeness

Without linearity  With linearity
Program  SS  X  X + red  SS  X  X + red
Life  0.67  0.6  0.7  0.58  0.57  0.64
Kalah  1.17  1.17  1.2  1.15  1.14  1.17
NRev  0.07  0.06  0.08  0.04  0.04  0.05
Queens  0.32  0.2  0.26  0.06  0.06  0.07
Meta Qsort  1.3  0.72  0.99  1.31  0.88  1.2
Neural  1.1  1.01  1.05  0.95  0.96  0.97
Mastermind  3.2  2.92  3.18  2.46  2.47  2.58
Browse  2.07  1.44  1.66  1.16  0.94  1.11
Disj  6.31  6.4  6.41  7.04  7.05  7.15
DNF  8.14  8.07  8.02  10.89 10.72 10.85
Boyer  8.46  5.4  2.31  6.85  4.58  2.18
SCC  7.9  7.51  8.03  8.66  8.63  9.09
Gabriel  12.87  6.79  3.6  10.4  5.87  3.32
CS  14.02 14.2  14.52  26.77 26.89 27.52
N and C  22.28 13.03 10.77  1.93  1.91  2.4
Palindrome  2.98  1.57  1.37  0.24  0.24  0.3
Zebra  29.71 29.94 32.18  27.75 28.06 29.99
Treeorder 128.5  80.51 19.83 103.58 67.64 18.87
Peep  140.02 85.15 31.65 104.19 66.08 26.19
Parser DCG 14.07 12.37 16.62  19.06 17.33 23.56
Read  118.43 68.83 35.22  90.68 55.17 30.89
R on P  ∞  ∞  ∞  2.33  2.3  6.32

Table 2: Experimental results obtained with the China analyzer (cont’d).

Experimentation also shown that the X domain is indeed a good idea. By replacing star-union with binary-union we have, in the worst case, an almost negligible slowdown. In the best case, instead, we obtain significant speedups. It is interesting to observe that these speedups occur when they are most needed, that is for the analysis of programs where SS, with or without linearity, behaves badly. In other words, X has a more stable behavior: this is no surprise, since we have replaced an algorithm with exponential complexity with a quadratic one. This stability is highly desirable for practical data-flow analyzers.

The last indication we can draw from the experimental results is that eliminating the redundant elements from sharing sets requires care. Even though on the toughest programs systematic reduction can give rise to a threefold increase in the analysis speed (Treeorder), it can also result in a threefold slowdown (R on P). The unfavorable case happens when reduction is repeatedly attempted on sharing sets that have few or no redundant elements. We have conducted some experimentation on the use of heuristics in order to trigger the reduction process. Even though the preliminary results we have obtained with this technique are encouraging, we do not present them here mostly because we believe that more theoretical work is needed on the subject.

Of course, analyses based on either X or X + red require less (sometimes much less) memory than those based on SS. Moreover, our prototype implementation of both X and X +red is the most natural one: we believe that there is much room for improvement.

6 Conclusion

We have questioned, apparently for the first time, whether the set-sharing domain Sharing is the most adequate for tracking pair-sharing between program variables. The answer turned out to be negative. We have presented a new domain X that is, at the same time, a strict abstraction of SS and as precise as SS on pair-sharing. We have also shown that no abstract domain weaker than X can enjoy this last property. This theoretical work has led us to an important practical result: the exponential star-union operation in the abstract unification procedure can be safely replaced by the binary-union operation, which has quadratic complexity. We have presented preliminary experimental results, showing that, in practice, our new domain compares favorably with SS over a wide range of benchmark programs.

Even though space limitations do not allow us to be more precise, it must be stressed that our theoretical results, obtained in this paper for SS, can also be obtained for the combination (as described in [4]) of SS with Lin, where Lin is the usual domain for linearity: a flag for each variable that indicates definite linearity. However, the results of Section 3, as they are, cannot be applied to the combination SS with Free and, henceforth, to SS combined with both Free and Lin (Free is the usual domain for freeness: a flag for each variable that indicates definite freeness [4]). Beside the need to consider accuracy with respect to the PS ×Free property (where ·×· indicates the reduced product operation [10]), we have to reconsider the concept of redundancy. Our definition of redundancy disregards the interactions between the sharing and the freeness components [11]: a new definition should be given that induces a finer equivalence relation. To summarize, we cannot claim that X combined with Free is as accurate as SS combined with Free with respect to the PS × Free property. However, from a practical point of view, we do claim that the results of our implementation of the combination of X with Free are as accurate as all current implementations of SS plus Free. As a matter of fact, the abstract operators formalized in [11] appear to be characterized by an unfavorable cost/precision ratio, and the optimal form of these operators has not been implemented. The same observations apply when comparing the combination X plus Free plus Lin with respect to SS plus Free plus Lin.

References

[1] R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Italy, March 1997. Printed as Report TD-1/97.

[2] R. Bagnara, P. M. Hill, and E. Zaffanella. Sharing revisited. Technical Report 97.19, School of Computer Studies, University of Leeds, 1997.

[3] M. Bruynooghe and M. Codish. Freeness, sharing, linearity and correctness — All at once. In Static Analysis, Proceedings of the Third International Workshop, volume 724 of Lecture Notes in Computer Science, pages 153–164, Padova, Italy, 1993. Springer-Verlag.

[4] M Bruynooghe, M. Codish, and A. Mulkers. Abstract unification for a composite domain deriving sharing and freeness properties of program variables. In Proceedings of the W2 Post-Conference Workshop, ICLP’94, pages 213–230, Santa Margherita Ligure, Italy, 1994.

[5] M. Codish, D. Dams, G. Filé, and M. Bruynooghe. Freeness analysis for logic programs-and correctness? In Proceedings of the Tenth International Conference on Logic Programming, pages 116–131, Budapest, Hungary, 1993. The MIT Press.

[6] A. Cortesi and G. Filé. Comparison and design of abstract domains for sharing analysis. In Proceedings of GULP’93, pages 251–265, Gizzeria, Italy, 1993.

[7] A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation for comparing static analyses. In Proceedings of GULP-PRODE’94, pages 372–397, Peñíscola, Spain, September 1994.

[8] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Conceptual and software support for abstract domain design: Generic structural domain and open product. Technical Report CS-93-13, Brown University, Providence, RI, 1993.

[9] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Conference Record of POPL’94, pages 227–239, Portland, Oregon, 1994.

[10] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL’77, pages 238–252, 1977.

[11] G. Filé. Share × Free: Simple and correct. Technical Report 15, Dipartimento di Matematica, Università di Padova, December 1994.

[12] D. Jacobs and A. Langen. Accurate and efficient approximation of variable aliasing in logic programs. In Proceedings of the North American Conference on Logic Programming, pages 154–165. The MIT Press, 1989.

[13] D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2&3):291–314, 1992.

[14] A. King. A synergistic analysis for sharing and groundness which traces linearity. In Proceedings ESOP’94, volume 788 of Lecture Notes in Computer Science, pages 363–378, Edinburgh, UK, 1994. Springer-Verlag.

[15] A. King and P. Soper. Depth-k sharing and freeness. In Proceedings of the Eleventh International Conference on Logic Programming, pages 553–568, Santa Margherita Ligure, Italy, 1994. The MIT Press.

[16] A. Langen. Static Analysis for Independent And-Parallelism in Logic Programs. PhD thesis, University of Southern California, 1990.

[17] K. Muthukumar and M. Hermenegildo. Combined determination of sharing and freeness of program variables through abstract interpretation. In Proceedings of the Eighth International Conference on Logic Programming, pages 49–63, Paris, France, 1991. The MIT Press.

[18] H. Søndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In Proceedings of ESOP’86, volume 213 of Lecture Notes in Computer Science, pages 327–338. Springer-Verlag, 1986.