Widening Sharing

Enea Zaffanella, Roberto Bagnara, Patricia M. Hill

Abstract

We study the problem of an efficient and precise sharing analysis of (constraint) logic programs. After recognizing that neither plain Sharing nor its non-redundant (but equivalent) abstraction scale well to real programs, we consider the domain proposed by C. Fecht [11, 12]. This domain consists of a combination of Pos with a quite weak abstraction of Sharing. While verifying that this domain is truly remarkable, in terms of both precision and efficiency, we have revealed significant precision losses for several real programs. This loss concerns groundness, pair-sharing and linearity. We define a simple domain for sharing analysis that supports the implementation of several widening techniques. In particular, with this domain it is straightforward to turn Fecht’s idea into a proper widening. More precise widenings are also considered. However, in spite of thorough experimentation we found that, provided Pos is included in the domain, the first widening we propose is hard to improve on.

Keywords: Abstract Interpretation, Mode Analysis, Sharing Analysis, Widening.

1 Introduction

For (constraint) logic programs, the main purpose of sharing analysis is to detect pair-sharing, that is, which pairs of variables are definitely independent. In a previous work [3] we observed that the Sharing domain of Jacobs and Langen (denoted here as SH ) [14] is redundant for pair-sharing. This achievement has important theoretical consequences (some of which will be exploited in the present work) and also has a practical interest. In fact, it allows sharing-sets (the elements of SH ) to be kept as small as possible without any precision loss and replace the star-union operation, whose complexity is exponential, by self-bin-union, which is quadratic. Even though significant speed-ups have been observed in practice (up to 3 orders of magnitude) the problem of scalability of the analysis to real programs, both in terms of precision (that is, the number of pairs that are detected as being definitely independent) and of resource usage, was still to be solved.

Enea Zaffanella is with the Servizio IX Automazione, Università degli Studi di Modena, Italy; Email: zaffanella.enea@unimo.it. Roberto Bagnara is with the Dipartimento di Matematica, Università degli Studi di Parma, Italy; Email: bagnara@cs.unipr.it. Patricia M. Hill is with the School of Computer Studies, University of Leeds, Leeds, U.K.; Email: hill@scs.leeds.ac.uk.

This research was partly supported by EPSRC, grant GR/M05645.

APPIA-GULP-PRODE’99

C. Fecht [11, 12] proposed a domain ↓ SH for sharing analysis based on SH . This domain is the same as SH but the concretization of a set of variables in ↓ SH is equivalent to the concretization of its powerset in SH . The advantage of ↓ SH is not just that an element can be normalized by removing all but the maximal ones, thereby reducing its size, but because it enables more efficient (but less precise) abstract operations than those used for SH and its non-redundant version SH^{ρ} [3].

One of the problems with the domain ↓ SH is that it does not capture ground dependencies. These are important for tracking sharing dependencies and, hence, sharing. Fecht solved this by deriving the ground dependencies through the Pos component of the combined domain Pos + ↓ SH (where Pos is the usual domain of positive Boolean formulas for groundness analysis) and also Pos + ↓ SH + Lin (where Lin is a domain for representing variables that are definitely bound to linear terms). Fecht tested both these domains and showed that, with his benchmarks, they compared favorably with equivalent ones using SH for the sharing and ground dependencies. He reported a negligible loss of precision and demonstrated that large programs could be analyzed using both Pos + ↓ SH and Pos + ↓ SH + Lin in a reasonable time scale. The results, although inconclusive, demonstrated real promise for an analyzer based on the ↓ SH approach. We say the results were inconclusive. The reason for this is that only a few non-trivial programs were tested and, for most of these, precision was not compared. (His SH analyzer could not cope with large programs possibly due to the problem that there was no redundancy elimination.) We note that Fecht did not present the domain ↓ SH as a widening and did not discuss how a widening based on his domain might be achieved.

1.1 Precision Results for SH and ↓ SH

We have compared the domain of Fecht enhanced with Free, the domain representing freeness information, that is Pos + ↓ SH + Free + Lin, with the same combination where ↓ SH is substituted by the non-redundant sharing domain SH^{ρ} [3]. The precision of the analysis is measured by summing results over the success-patterns, for goal-independent (GI) analysis, and over both the call- and success-patterns, for goal-dependent (GD) analysis, for each procedure. For the domains tested, that is, Pos+↓ SH +Free+Lin, abbreviated as P+DSH+F+L, and Pos+SH^{ρ} +Free+Lin, abbreviated as P+NSH+F+L, the precision results consist of: the total number of definitely non-sharing pairs of program variables, NSP, the total number of definitely ground variables, GV, and the total number of definitely linear variables that are possibly not ground, LV. The freeness results are not compared because, as we have shown in [18], freeness is not affected, neither by abstracting SH to ↓ SH , nor by redundancy elimination.

The comparison involved all the 92 Prolog programs in our current test-suite. On 73 of them there was no difference in precision. This is really remarkable considering that the ↓ SH approximation is rather crude. The combined domain Pos+↓ SH +Lin is isomorphic to ASub + Pos (where ASub is the pair-sharing domain of Søndergaard [17]), and the domain Pos + ↓ SH is exactly the domain ASub^{+} defined by Cortesi and Filé in [8]. However, they considered this domain only en passant and only from a theoretical point of view. In other words, Fecht has the whole merit for having

Goal-Independent  Goal-Dependent
P+DSH+F+L P+NSH+F+L P+DSH+F+L P+NSH+F+L
Program NSP GV LV NSP GV LV NSP GV LV NSP GV LV
aqua c 10749 ⋆406 2753 ? ? ? 16306 ⋆1186 2028 ? ? ?
bmtp  1451 136 972 1461 136 976
bryant  784 10 146 1088 10 223 1033 141 58 1781 141 58
caslog 6456 ⋆466 1588 7027 ⋆474 1615 11073 ⋆1625 1079 ? ? ?
cg pars  136 31 159 138 31 160
dpos an 92 40 76 95 40 76 183 76 53 183 76 53
lg sys  7274 645 2260 7334 645 2261
nand  473 23 182 475 23 182 1341 481 70 1341 481 70
nbody  261 52 104 262 52 104  477 151 41 478 151 41
ochina  2185 285 1163 2193 285 1166 3985 802 760  ?  ? ?
quot an  288 37 160 288 37 160  639 159 122 646 159 122
reg  774 42 272 796 42 284  207  67 52 207 67 52
rubik  70 ⋆55 110  73 ⋆76 93  174 ⋆110 124 201 ⋆200 103
scc  63  0 37  63  0 37  503 174 46 506 174 46
sfecht  28  0 14  85  0 31  221  0 47 278  0 64
simple  370 27 139 373 27 139  572  82 76 639 82 76
slice  427 126 453 428 126 453
spsys  788 81 386 800 81 394
trs  32  6 22  53  6 22  73 ⋆12 20 104 ⋆12 20

Table 1: Pos + ↓ SH + Free + Lin vs Pos + SH^{ρ} + Free + Lin: precision.

trusted on this domain from a precision/efficiency perspective. The results for the remaining 19 programs are summarized in Table 1.

The blank entries in the goal-dependent columns are for those programs whose goal-dependent analysis is pointless. This usually happens because the program contains a procedure call to an unknown procedure (e.g., by means of call/1). The China analyzer (i.e., our system [1]) promptly recognizes these cases and reverts to a goal-independent analysis. This is one of the reasons why focusing only on goal-dependent analyses is, in our opinion, a mistake. The other reason being that the ability of analyzing libraries once and for all is desirable and, more generally, so is the separate analysis of different program modules, especially in very large projects. Focusing only on goal-independent analyses is the opposite mistake: GD analyses, when possible, are more precise than GI ones. For these reasons, we insist in presenting experimental results for both.

A star symbol (⋆) in the GV column signifies that one of the widenings we employ on the GER representation of Pos fired. This is a widening imposing a limit on the number of ROBDD nodes simultaneously allocated. It makes approximations of the R (ROBDD) component when this limit is reached^{1}, while retaining full precision on the G (definitely ground variables) and the E (classes of equivalent variables) components [2, 4]. The scarcity of stars in this and the following tables, shows how seldom this widening is actually required.^{2}

Apart from sfecht, which is a synthetic benchmark designed in order to show that arbitrary precision losses are possible with ↓ SH , Table 1 illustrates how heavy precision penalties can be incurred by ↓ SH even on real programs. Most notably, for bryant we see a precision loss as high as 28% on GI analysis and 42% on GD analysis. In addition, simple loses 10% (GD), while trs loses 40% (GI) and 30% (GD). Note that, for these programs, the Pos widening fires only on the GD analysis of trs. The rubik program shows an interesting phenomenon: here the Pos widening fires incurring a precision loss of exactly 1 ground variable (a critical one indeed), but SH^{ρ} saves the day by recovering the lost groundness information. A similar thing happens for caslog. Thus, the widely held opinion (now proved in [7]) that Sharing does not help Pos on groundness does not carry through when widenings are considered.

1That is, by approximating x ∧ y with x or with y, x ∨ y with true and so forth.

2Indeed, the newest version of China avoids also the widening for the caslog program.

While space limitations do not allow us to report full timing information, we can easily confirm Fecht’s claim: the speedup is dramatic. Just a few examples: the fixpoint computation time in seconds for bmtp, caslog, lg sys, and spsys drops from 15.6, 614.7, 735.9, and 2.2, to 0.8, 2.0, 3.3, and 0.6, respectively. All the experiments described in this paper were performed on a PC equipped with an AMD K6@400MHz, 128MB of main memory, and running Linux 2.2.1.

1.2 The Present Work

The objective of this work, after having recognized that Fecht’s approach incurs significant precision loss on several real programs, is to improve the state of the art in mode analysis, in general, and sharing analysis in particular.

The present work is not intended for achieving the fastest ever analysis, since high speeds are often achieved at the expense of precision. The real problem, we believe, is how to increase precision yet avoid the concrete effects of exponential complexity. Consider groundness analysis, for instance. The cruder domains do not pose any efficiency problem. In contrast, the more refined domains for groundness, such as Pos, work perfectly until you bump into a “nasty” program clause (i.e., with more than, say, fifty variables for which the analyzer knows too little at that point of the analysis). When this happens, Pos will exhaust your computer’s memory. One would like to have a more linear, or stable behavior. The right solution, as indicated in [10], is not to revert to the simpler domains. We should use complex domains instead, together with widening (and maybe narrowing) operators. With this technique we can try to limit precision losses to those cases where we cannot afford the refined domains.

We moved from the observation that, when the sharing-sets become large, then they are at the same time heavy to manipulate and, at least for a subset of the variables involved, light as far as information content is concerned. We thus introduce a new representation SH^{W} for set-sharing made of two components. They are both sharing-sets. However, while the second one is interpreted in the usual way, the first component records worst-case sharing assumptions of sets of variables. We define the operations required for the analysis with SH^{W}, and we prove them correct. We also introduce a safe optimization that is very effective in practice.

We then show how SH^{W} supports a variety of widenings. One of those is a simple adaptation of Fecht’s idea. Others are much more sophisticated and involve only a limited precision loss. However, in spite of thorough experimentation (of which only a tiny fraction can be reported here) we found that the first widening we propose is hard to improve on, provided Pos is included in the domain. This suggests that what is lost by this widening is mostly constituted by ground dependencies, and these can be recovered (and improved) by the Pos component. We show that when Pos is not included, a widening based on cliques of sharing pairs is preferred. Since some authors advocate the use of SH without coupling it with Pos (we do not share this view), this is an important message for them.

In this work as in Fecht’s work, the combination of a sharing domain with Pos is the simplest possible. For any operation of the analysis, abstract mgu in particular, the Pos component is evaluated first. All sharing groups containing at least one variable that is definitely ground according to the resulting Pos formula are removed from the sharing component. This combination is made particularly efficient by the ready availability of definite groundness information allowed by the GER representation introduced in [4], where obtaining the set of definitely ground variables (and also the classes of groundness-equivalent variables) is a constant-time operation. Note that more sophisticated combinations are possible [7].

Following several other authors, we observed in [3], that, from a practical point of view, sharing analysis without freeness or linearity does not make sense. Both these properties allow, in a significant proportion of cases, to dispense with costly operations (such as star-union or, better, self-bin-union) increasing the precision of sharing information at the same time, and this with very little overhead. Moreover, freeness is a useful property in itself. For details on how the combination with freeness is realized, we refer the reader to [16, 18]. See [6] for the combination of both freeness and linearity information.

Among the contributions of this paper we would like to stress the following: we present a data-flow analysis for groundness, freeness, pair-sharing, and linearity, with unprecedented levels of precision and efficiency. With the implementation described in this paper, the China analyzer is able to honor one of its most important design goals: never crash (e.g., by exhausting all the available memory), always terminate with a correct result and in reasonable time.

The paper is structured as follows: In Section 2 we briefly recall the required notions and notations, even though we assume general acquaintance with the topics of abstract interpretation, sharing analysis and groundness analysis. Section 3 introduces SH^{W} and the abstract operations for this domain. With SH^{W}, it is straightforward to turn Fecht’s idea into a proper widening. This is done in Section 4, after the introduction of an infinite family of widenings and a statement of their safety. More precise widenings are also considered. The experimental evaluation of the proposed approach is presented in Section 5. Section 6 concludes with some final remarks. The reader is referred to [18] for full proofs of all the results presented in this paper, and for more material on this subject.

2 Preliminaries

For any set S, ℘(S) denotes the powerset of S and # S is the cardinality of S. A monotone and idempotent self-map ρ: P → P over a poset ⟨P, ⪯⟩ is called a closure operator (or upper closure operator) if it is also extensive, namely ∀x ∈ P : x ⪯ ρ(x). In this paper, we assume there is a fixed and finite set of variables of interest denoted by VI . If t is a first-order term over VI , then vars(t) denotes the set of variables in t. Bind denotes the set of equations of the form x = t where x ∈ VI and t is a first-order term over VI . Note that we do not impose the occur-check condition x ∉ vars(t), since we have proved in [13] that this is not required to ensure correctness of the operations of SH and its derivatives. The following definitions are a simplification of the standard definitions for the Sharing domain [9, 13, 14] and assume that the set of variables of interest is fixed and finite.

Definition 1 (The set-sharing domain SH .) The set SH is defined as a powerset: SH =^{def} ℘(SG), where SG =^{def} { S ∈ ℘(VI ) | S ≠ ∅ }.

We now introduce the required abstract operations over SH .

Definition 2 (Some operations over SH .) Projecting an element of SH onto a subset of VI is performed through the binary function proj: SH × ℘(VI ) → SH : if sh ∈ SH and V ∈ ℘(VI ), then proj(sh, V) =^{def} { S ∩ V | S ∈ sh, S ∩ V ≠ ∅ }.

For each sh ∈ SH and each V ∈ ℘(VI ), the extraction of the relevant component of sh with respect to V is encoded by the function rel: ℘(VI ) × SH → SH defined as rel(V, sh) =^{def} { S ∈ sh | S ∩ V ≠ ∅ }.

For sh ∈ SH and V ∈ ℘(VI ), the exclusion of the irrelevant component of sh with respect to V is encoded by the function \overline{rel}: ℘(VI ) × SH → SH defined as \overline{rel}(V, sh) =^{def} sh \ rel(V, sh).

The 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_{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} }.

We also use the self-bin-union function sbin: SH → SH , which is given, for each sh ∈ SH , by sbin(sh) =^{def} bin(sh, sh).

The function amgu captures the effects of a binding on an SH element. Let (x = t) ∈ Bind, sh ∈ SH , V_{x} = {x}, V_{t} = vars(t), and V_{xt} = V_{x} ∪ V_{t}. Then

amgu(sh, x = t) =^{def} \overline{rel}(V_{xt}, sh) ∪ bin(rel(V_{x}, sh)^{⋆}, rel(V_{t}, sh)^{⋆}).

The domain SH captures set-sharing. However, the property we wish to detect is pair-sharing and, for this, it has been shown that SH includes unwanted redundancy [3].

Definition 3 (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 } where pairs(S) =^{def} { P ∈ ℘(S) | # P = 2 }.

Definition 4 (The domain SH^{ρ}.) The function ρ: SH → SH is given, for each sh ∈ SH , by ρ(sh) =^{def} sh ∪ { S ∈ SG | S is redundant for sh }. Then SH^{ρ} =^{def} ρ(SH ) =^{def} { ρ(sh) | sh ∈ SH }.

We use the notation sh_{1} =_{ρ} sh_{2} and sh_{1} ⊆_{ρ} sh_{2} to denote ρ(sh_{1}) = ρ(sh_{2}) and ρ(sh_{1}) ⊆ ρ(sh_{2}), respectively. The advantage of SH^{ρ} is that we can replace the star-union operation in the definition of the amgu by self-bin-union without loss of precision [3]. In particular, it is shown:

amgu(sh, x = t) =_{ρ} \overline{rel}(V_{xt}, sh) ∪ bin(sbin(rel(V_{x}, sh)), sbin(rel(V_{t}, sh))). (1)

3 A New Representation for Set-Sharing

We introduce here a new representation for set-sharing. It is made up of two components: one is the original set-sharing domain while the other represents all possible subsets of each of its elements and, for this reason, is called a clique-set.

Definition 5 (Clique-set.) A clique-set is an element of CL and CL =^{def} SH .

An element of a clique-set is called a clique.

Definition 6 (Sharing-sets representation for clique-sets.) The (overloaded) functions ↓: SG → SH and ↓: CL → SH are given, for each C ∈ SG and each cl ∈ CL, by ↓ C =^{def} ℘(C) \ {∅} and ↓ cl =^{def} ⋃_{C∈cl} ↓ C. Observe that ↓ is an upper closure operator over SH . If cl ∈ CL and C ∈ SG then we say that C is downredundant in cl if there exists C′ ∈ cl such that C ⊂ C′.

The addition or removal of down-redundant elements to or from a clique-set makes no difference to the sharing-sets that it represents. So, a clique represents a worst case^{3} pair-sharing condition on the set of variables it contains. In an implementation, as we need to keep the clique sets as small as possible, down-redundant elements are removed via a normalization function.

Definition 7 (Normalization of Clique-Sets.) For each cl ∈ CL, the normalization function |·|: CL → CL is given by

|cl| =^{def} cl \ { C ∈ cl | C is down-redundant for cl }.

We now define abstract unification over clique-sets and state its soundness.

Definition 8 (Abstract Unification over CL.) For each V ∈ ℘(VI ) and each cl ∈ CL, the function \overline{rel}^{CL} : ℘(VI ) × CL → CL is given by

\overline{rel}^{CL}(V, cl) =^{def} \{ C \ V | C ∈ cl \} \ \{∅\}.

The function amgu^{CL} : CL × Bind → CL is given, for each cl ∈ CL and each binding (x = t) ∈ Bind, by

amgu^{CL}(cl, x = t) =^{def} \overline{rel}^{CL}(V_{xt}, cl) ∪ bin(sbin(cl_{x}), sbin(cl_{t})),

where cl_{x} = rel(V_{x}, cl), cl_{t} = rel(V_{t}, cl), V_{x} = {x}, V_{t} = vars(t), and V_{xt} = V_{x} ∪ V_{t}.

3While this terminology is due to Langen [15], our definition differs from the one he used.

Theorem 9 For each clique-set cl ∈ CL and each binding (x = t) ∈ Bind, we have that amgu(↓ cl, x = t) ⊆_{ρ} ↓ amgu^{CL}(cl, x = t).

We next define our new sharing domain for widening.

Definition 10 (The SH^{W} Representation.) The set SH^{W} is given by

SH^{W} =^{def} { (cl, sh) | cl ∈ CL, sh ∈ SH }

and is ordered by ⊑ defined as follows, for each shw, (cl_{1}, sh_{1}), (cl_{2}, sh_{2}) ∈ SH^{W}: (cl_{1}, sh_{1}) ⊑ (cl_{2}, sh_{2}) ⟺ (cl_{1} ⊆ cl_{2}) ∧ (sh_{1} ⊆ sh_{2}). It can be seen that SH^{W} is a complete lattice. The sharing-set represented by an element of SH^{W} is given, for each (cl, sh) ∈ SH^{W}, by the function I(·): SH^{W} → SH where

I((cl, sh)) =^{def} ↓ cl ∪ sh.

The normalization of an element of SH^{W} is given, for each (cl, sh) ∈ SH^{W}, by the function |·|: SH^{W} → SH^{W} where

|(cl, sh)| =^{def} (|cl|, sh \ ↓ cl).

The normalization removes unnecessary elements from a description in SH^{W}. We now define an upper closure operator ϱ inducing an equivalence relation on the elements of SH^{W}.

Definition 11 (The ϱ(SH^{W}) domain.) The function ϱ: SH^{W} → SH^{W} is given, for each shw ∈ SH^{W} with shw =^{def} (cl, sh), by

ϱ(shw) =^{def} (ρ(↓ cl), ρ(I(shw))).

Then ϱ is an upper closure operator for SH^{W} [18]. We will use the notation shw_{1} =_{ϱ} shw_{2} to denote ϱ(shw_{1}) = ϱ(shw_{2}) and shw_{1} ⊑_{ϱ} shw_{2} to denote ϱ(shw_{1}) ⊑ ϱ(shw_{2}).

The ordering ⊑_{ϱ} is used for modeling the relative precision between widenings in Section 4. When shw_{1} =_{ϱ} shw_{2}, shw_{1} and shw_{2} behave the same way as far as representing pair-sharing and groundness is concerned.

Proposition 12 If shw ∈ SH^{W}, then I(shw) =_{ρ} I(ϱ(shw)) and shw =_{ϱ} |shw|.

Definition 13 (Operations over SH^{W}.) For each (cl, sh), (cl_{i}, sh_{i}) ∈ SH^{W}, with i = 1, 2, and each V ∈ ℘(VI ), the functions rel^{W}, \overline{rel}^{W} : ℘(VI ) × SH^{W} → SH^{W} and ∪^{W}, bin^{W} : SH^{W} × SH^{W} → SH^{W}, the functions sbin^{W} : SH^{W} → SH^{W} and, finally, amgu^{W} : SH^{W} × Bind → SH^{W}, are defined as follows:

rel^{W}(V, (cl, sh)) =^{def} (rel(V, cl), rel(V, sh)),
\overline{rel}^{W}(V, (cl, sh)) =^{def} (\overline{rel}^{CL}(V, cl), \overline{rel}(V, sh)),
(cl_{1}, sh_{1}) ∪^{W} (cl_{2}, sh_{2}) =^{def} (cl_{1} ∪ cl_{2}, sh_{1} ∪ sh_{2}),
bin^{W}((cl_{1}, sh_{1}), (cl_{2}, sh_{2})) =^{def} (bin(cl_{1}, cl_{2}) ∪ bin(cl_{1}, sh_{2}) ∪ bin(sh_{1}, cl_{2}),
bin(sh_{1}, sh_{2})),
sbin^{W}((cl, sh)) =^{def} bin^{W}((cl, sh), (cl, sh))

= (sbin(cl) ∪ bin(cl, sh), sbin(sh)),

amgu^{W}(shw, x = t) =^{def} \overline{rel}^{W}(V_{xt}, shw)
∪^{W} bin^{W}(sbin^{W}(rel^{W}(V_{x}, shw)),
sbin^{W}(rel^{W}(V_{t}, shw))),

where V_{x} = {x}, V_{t} = vars(t), and V_{xt} = V_{x} ∪ V_{t}.

The next theorem, proven in [18], states the correctness of amgu^{W} and that normalization does not affect the correctness or precision of amgu^{W}.

Theorem 14 For each shw ∈ SH^{W} and each (x = t) ∈ Bind,

amgu(I(shw), x = t) ⊆_{ρ} I(amgu^{W}(shw, x = t));
amgu^{W}(shw, x = t) =_{ϱ} amgu^{W}(|shw|, x = t).

In general, ϱ is not a congruence for amgu^{W} and precision may be lost when the first component of shw is non-empty and the second component of shw contains redundant elements. Further work on this aspect is ongoing.

The computation of amgu^{W} can be optimized. To explain this, we need some extra notation. Let us define: shw = (cl, sh) ∈ SH^{W} and x = t ∈ Bind; V_{x} = {x}, V_{t} = vars(t), and V_{xt} = V_{x} ∪ V_{t}; shw_{x} = (cl_{x}, sh_{x}) = rel^{W}(V_{x}, shw) and shw_{t} = (cl_{t}, sh_{t}) = rel^{W}(V_{t}, shw). Suppose C_{x} = ⋃ cl_{x}, C_{t} = ⋃ cl_{t}, S_{x} = ⋃ sh_{x}, S_{t} = ⋃ sh_{t}, A_{xt} = bin(sbin(sh_{x}), sbin(sh_{t})), B_{xt} = bin(sh_{x}, sh_{t}), B_{x} = bin(cl_{x}, sh_{x}), and, finally, B_{t} = bin(cl_{t}, sh_{t}). Then let

shw_{rel}^{opt} =^{def} \begin{cases}(\{C_{x} ∪ C_{t} ∪ S_{x} ∪ S_{t}\}, ∅), & if cl_{x} ≠ ∅, cl_{t} ≠ ∅; \\ (\{C_{x} ∪ S_{t}\} ∪ B_{x} ∪ B_{xt}, A_{xt}), & if cl_{x} ≠ ∅, cl_{t} = ∅; \\ (\{C_{t} ∪ S_{x}\} ∪ B_{t} ∪ B_{xt}, A_{xt}), & if cl_{x} = ∅, cl_{t} ≠ ∅; \\ (∅, A_{xt}), & if cl_{x} = ∅, cl_{t} = ∅. \end{cases}

In [18], we prove the following optimization for the computation of amgu^{W}.

Theorem 15 Assuming the above notation,

amgu^{W}(shw, x = t)

=_{ϱ} \begin{cases}(\overline{rel}(V_{xt}, cl), \overline{rel}(V_{xt}, sh)) ∪^{W} shw_{rel}^{opt}, & if shw_{x} ≠ (∅, ∅), shw_{t} ≠ (∅, ∅); \\ \overline{rel}^{W}(V_{xt}, shw), & otherwise. \end{cases}

In Eq. (1), the basic amgu operation is defined using the SH^{ρ} domain. However, when we have freeness and linearity information it has been proven that we can improve the analysis with respect to precision and efficiency by avoiding one or both of the self-bin-unions occurring as components of the binary union operation. The question arises as to whether this improvement can be adapted for the amgu^{W} operation. That is, can we avoid the corresponding sbin^{W} operations under the same linearity and freeness conditions? The answer is yes, we can generalize Theorem 14 and show that this is sound. However, we may lose precision. Moreover, the optimization given by Theorem 15 only applies to the basic amgu^{W} operation given in Definition 13. When one or both of the self-bin-unions here is omitted due to available freeness and linearity information, then =_{ϱ} in the theorem becomes ⊑_{ϱ} and we may lose further precision. Further work on this subject is ongoing.

4 Widening Set-Sharing

We can now define a family of unary widenings over SH^{W}.

Definition 16 (Widening for SH^{W}.) A function ∇: SH^{W} → SH^{W} is a widening for SH^{W} if, for each shw ∈ SH^{W}, we have shw ⊑_{ϱ} ∇ shw.

The following result establishes the safety of such widening operators.

Theorem 17 For each shw ∈ SH^{W} and each (x = t) ∈ Bind we have

amgu^{W}(shw, x = t) ⊑_{ϱ} amgu^{W}(∇ shw, x = t).

The obvious corollary is that any analysis using these widenings, possibly a different widening at each step of the analysis, is correct. After widening we usually normalize the new domain to provide a smaller representation. Moreover, it is also shown in [18] that similar results hold for each of the component operators such as bin^{W} for amgu^{W}. Thus we can (and do) safely widen and normalize within the actual computation of amgu^{W}. The analyzer has the freedom of using whichever widening suits its current needs. Those needs can be dictated by a number of heuristics. Of course, really useful widenings are guarded by some applicability condition. The simplest conditions are those based on the cardinality of the sets in the SH^{W} description. For example, for each widening ∇ and for suitable choices of f: ℕ^{2} → ℕ and n ∈ ℕ, one can define

∇_{f,n}(cl, sh) =^{def} \begin{cases}∇(cl, sh), & if f(# cl, # sh) > n; \\ (cl, sh), & otherwise. \end{cases}

We order the widenings in the obvious way. If ∇_{1} and ∇_{2} are two widenings and, for all shw ∈ SH^{W}, ∇_{1}(shw) ⊑_{ϱ} ∇_{2}(shw), then let ∇_{1} ⊑_{ϱ} ∇_{2}. At the top end of the scale of widenings we have two panic widenings. They are defined by

∇^{p}(cl, sh) =^{def} (cl ∪ {⋃ sh}, ∅), ∇^{P} (cl, sh) =^{def} ({⋃ cl ∪ ⋃ sh}, ∅).

The panic widenings are present in the China implementation, with very strict guards, only to enforce the “never crash” motto: no real program we have access to makes them fire. At the other extreme we have very soft widenings.

Definition 18 (Cautious widening.) A widening ∇: SH^{W} → SH^{W} is called cautious if, for each shw ∈ SH^{W},

I(∇ shw) =_{ρ} I(shw).

Thus, a widening never introduces new pair-sharings nor new singletons in the description. However, information is lost as soon as the operations for the analysis given by Definition 13 are considered. For example, consider two elements of

SH^{W}: shw_{1} =^{def} (∅, {x, y, z, xy, xz, yz}) and shw_{2} =^{def} ({xyz}, ∅) so that we have

I(shw_{1}) =_{ρ} I(shw_{2}) but ϱ(shw_{1}) ≠ ϱ(shw_{2}). While sharing between y and z is not contemplated in rel^{W}({x}, shw_{1}) = (∅, {x, xy, xz}), the same does not hold for rel^{W}({x}, shw_{2}) = shw_{2}.

A useful cautious widenings is the gentle widening, defined as follows. Consider shw ∈ SH^{W}, and G be the graph (N, E) where N =^{def} { x | {x} ∈ I(shw) } and

E =^{def} { (x, y) | {x, y} ∈ I(shw), x, y ∈ N, x ≠ y }. Then

∇^{G} shw =^{def} ({C_{1}, …, C_{k}}, sh),

where C_{1}, …, C_{k} are all the maximal cliques of G. Note that, although the problem of enumerating all the maximal cliques of an undirected graph is NP-complete, this does not seem to be a problem for the graphs arising during the analysis of even the biggest real programs. For the experimentation we used the algorithm by Bron and Kerbosch [5], which is Algorithm 457 in the ACM collection, even though more efficient algorithms are present in the literature.

Of intermediate precision is the widening based on Fecht’s idea, which we call Fecht’s widening and defined as

∇^{F} (cl, sh) =^{def} (cl ∪ sh, ∅).

This widening is not cautious. However, it does not introduce new pairs. As it can introduce new singletons, it may destroy ground dependencies, and this is why this kind of widening is better coupled with Pos.

5 Experimental Evaluation

For the experimental evaluation of the Fecht’s widening ∇^{F}, precision is compared with respect to the non-redundant sharing domain SH^{ρ}. In fact, this approach is almost always as precise as the optimal one using SH^{ρ}.

For this and the following experiments, the widening was guarded by a size threshold of 100 on the second component (i.e., the normal sharing part). In other words, immediately before each abstract mgu operation the analyzer operated ρ-redundancy elimination, as usual. If after this the operand (cl, sh) was such that # sh > 100, then (cl, sh) was substituted by ∇^{F} (cl, sh). Let us call this guarded widening ∇_{100}^{F}. The results are reported in Table 2. Note that only the programs where the analysis with SH^{W} gives different results from the analysis with SH^{ρ} are reported in the table. Thus, for all the programs in the test-suite, the analysis with SH^{W} using the

Goal-Independent  Goal-Dependent
P+WSH+F+L P+NSH+F+L P+WSH+F+L P+NSH+F+L
Program NSP GV LV NSP GV LV NSP GV LV NSP GV LV
aqua c  11147 ⋆406 2757  ?  ?  ? 16364 ⋆1188 2028  ?  ?  ?
caslog  6553 474 1615 7027 474 1615 11338 1739 1062  ?  ?  ?
ochina  2193 285 1166 2193 285 1166 3958  802 760  ?  ?  ?
quot an  288  37 160 288 37 160  639  159 122 646 159 122

Table 2: Pos + SH^{W} + Free + Lin vs Pos + SH^{ρ} + Free + Lin using ∇_{100}^{F}: precision.

(rather drastic) widening ∇_{100}^{F} gives the same results obtainable (at a much higher cost) with SH^{ρ}, apart from those in Table 2. For aqua c we obtain termination in reasonable time, as with Fecht’s technique but with higher precision. The same holds for the GD analysis of caslog and ochina. However, while the GI analysis of ochina is “optimal” (meaning “as precise as SH^{ρ}”), this is not the case for caslog. Non-optimality happens also for the GD analysis of quot an.

Obviously, ∇_{100}^{F} is never less precise than Fecht’s domain. What is surprising, however, is that it is almost that efficient. The timings and the number of applications of the widening are reported in Table 3 for all the programs such that at least one timing was above 0.4 seconds. The first observation to be made is that the widening comes into play only a few times on the test-suite. On average, it is safe to say that on 99.9% of cases the sharing-sets remain of reasonable size (100 groups or less in this experiment). Table 3 says that this definition of “reasonable” makes sense: for those programs where widening does not take place the difference in performance between Fecht’s domain and our SH^{W} with the ∇_{100}^{F} widening is very limited. Analysis of aqua c shows that limiting precision may on occasions increase the cost (since less precision means more self-bin-unions to perform, thus even less precision, …).

The results on the precision of ∇_{100}^{F} are so good that we are left with a ridiculous test-suite for checking how much we can improve by using a more cautious widening. Our experimentation showed that the gentle widening ∇_{100}^{G} improves over ∇_{100}^{F} only on quot an. The same does, but at a lower price, a bigger widening ∇^{g} that is defined as ∇^{G} apart from the fact that singletons are disregarded. In other words, the undirected graph considered for ∇^{g}, given shw ∈ SH^{W}, is G =^{def} (N, E) such that

E =^{def} { (x, y) | {x, y} ∈ I(shw), x ≠ y } and N =^{def} { x | (x, y) ∈ E or (y, x) ∈ E }.

Now, suppose we perform sharing analysis without combining the sharing domain with Pos. Then it is important that the widening, as is the case with cautious ones, keeps track of singletons. Table 4 reports the results (fixpoint time and number of definitely not-sharing pairs) for SH^{W} with ∇_{100}^{F}, SH^{W} with ∇_{100}^{g}, and plain SH^{ρ}. The GD analysis of bryant is particularly eloquent example of the superiority of cautious widenings when Pos is not used.

Goal-Independent  Goal-Dependent
P+DSH+F+L P+WSH+F+L P+DSH+F+L P+WSH+F+L
Program  T  T  #W  T  T  #W
action  0.1  0.1  1  1.1  1.4  1
aircraft  0.2  0.2  0  0.7  0.7  0
aqua c  10.4  10.9  56  48.6  40.7  3
bmtp  0.8  0.9  6
bryant  0.1  0.1  0  0.6  1.4  1
caslog  2.0  2.5  17  17.7  19.2  22
chat80  0.9  1.0  2  4.3  4.9  6
chat parser  0.4  0.4  1  1.7  1.8  1
dpos an  0.2  0.2  0  0.5  0.8  1
eliza  0.1  0.1  0  0.2  0.4  1
lg sys  3.3  3.9  23
log interp  0.2  0.4  2  0.7  0.9  1
mixtus  0.9  0.9  4
ochina  1.2  1.4  11  7.7  8.3  4
parser dcg  0.2  0.1  0  0.7  0.6  0
peephole1  0.1  0.1  0  0.4  0.7  1
pets an  0.8  0.9  4  4.5  4.5  1
peval  0.2  0.3  3  0.4  0.5  1

plaiclp  0.7  0.7  3

press  0.1  0.1  0  0.4  0.7  0
quot an  0.3  0.4  0  1.3  1.7  1
read  0.1  0.1  0  0.3  0.6  1
reg  0.4  0.4  4  0.4  0.4  1
sdda  0.1  0.1  1  0.2  0.4  2
sim  0.2  0.3  2  0.7  0.8  2
simple  0.1  0.2  0  0.6  0.9  2
slice  0.6  0.7  2
spsys  0.6  0.7  5
trs  0.2  0.3  2  0.5  0.6  1
unify  0.1  0.1  0  0.5  0.7  0

Table 3: Pos + ↓ SH + Free + Lin vs Pos + SH^{W} + Free + Lin using ∇_{100}^{F}: timings (T) and number of (sharing) widenings (#W).

6 Conclusion

We believe we have made a significant step forward towards the solution of the problem of practical, precise, and efficient sharing analysis of (constraint) logic programs. We have studied a new representation for set-sharing that allows for the incorporation of a variety of widenings. Extensive experimentation has shown that one of these widenings, which is based on an idea of C. Fecht, provides seemingly hard to beat precision and performance, when combined with Pos. When this combination is not performed, we have also shown that “more cautious” widenings offer more precision at an acceptable extra-cost.

Goal-Independent  Goal-Dependent
SH^{W}, ∇_{100}^{F} SH^{W}, ∇_{100}^{g}  SH^{ρ}  SH^{W}, ∇_{100}^{F} SH^{W}, ∇_{100}^{g}  SH^{ρ}
Program T NSP T NSP  T NSP T NSP T NSP  T NSP
aqua c 4.1 10703 15.0 10899  ?  ? 27.6 15754 37.8 15754  ?  ?
bryant 0.2 1066 0.2 1066  0.2 1066 1.0 1033 1.0 1781  0.9 1781
caslog 2.1 6506 4.5 6539 744.4 7027 17.9 11054 21.8 11054  ?  ?
chat80 0.6 2536 1.1 2536  9.1 2536 4.4 3923 7.7 3926 285.7 5111
eliza 0.1 49 0.1 49 0.1 49 0.3 109 0.5 113 0.5 113
lg sys 2.7 7328 7.9 7334 725.1 7334
ochina 0.9 2187 2.6 2189 5.0 2193 5.9 3936 9.6 3936 ? ?
pets an 0.6 2525 1.3 2563 19.8 2569 3.7 4664 5.3 4664 1006.5 4710
quot an 0.3 288 0.4 288  0.3 288 1.4 639 3.2 646  3.1 646
simple 0.1 373 0.1 373  0.1 373 0.8 572 1.3 639  17.6 639
slice  0.6 426 0.9 428  0.8 428

Table 4: SH^{W} with ∇_{100}^{F} vs SH^{W} with ∇_{100}^{g} vs plain SH^{ρ}: timings and precision.

References

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

[2] R. Bagnara. Widening Pos: Simple, effective, and rarely needed. Unpublished short note, 1998.

[3] R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pairsharing. Theoretical Computer Science, 1999. To appear.

[4] R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDDbased implementations of Pos. In A. M. Haeberer, editor, Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST’98)”, volume 1548 of Lecture Notes in Computer Science, pages 471–485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.

[5] C. Bron and J. Kerbosch. Finding all cliques of an undirected graph. Communications of the ACM, 16(9):575–577, 1973.

[6] M. Bruynooghe, M. Codish, and A. Mulkers. Abstract unification for a composite domain deriving sharing and freeness properties of program variables. In F. S. de Boer and M. Gabbrielli, editors, Verification and Analysis of Logic Languages, Proceedings of the W2 Post-Conference Workshop, International Conference on Logic Programming, pages 213–230, Santa Margherita Ligure, Italy, 1994.

[7] M. Codish, H. Søndergaard, and P. J. Stuckey. Sharing and groundness dependencies in logic programs. Submitted for publication.

[8] A. Cortesi and G. Filé. Comparison and design of abstract domains for sharing analysis. In D. Saccà, editor, Proceedings of the “Eighth Italian Conference on Logic Programming (GULP’93)”, pages 251–265, Gizzeria, Italy, 1993. Mediterranean Press.

[9] A. Cortesi and G. Filé. Sharing is optimal. Journal of Logic Programming, 38(3):371–386, 1999.

[10] P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

[11] C. Fecht. An efficient and precise sharing domain for logic programs. In H. Kuchen and S. D. Swierstra, editors, Programming Languages: Implementations, Logics and Programs, Proceedings of the Eighth International Symposium, volume 1140 of Lecture Notes in Computer Science, pages 469–470, Aachen, Germany, 1996. Springer-Verlag, Berlin. Poster.

[12] C. Fecht. Efficient and precise sharing domains for logic programs. Technical Report A/04/96, Universität des Saarlandes, Fachbereich 14 Informatik, Saarbrücken, Germany, 1996.

[13] P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. In G. Levi, editor, Static Analysis: Proceedings of the 5th International Symposium, volume 1503 of Lecture Notes in Computer Science, pages 99–114, Pisa, Italy, 1998. Springer-Verlag, Berlin.

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

[15] A. Langen. Static Analysis for Independent And-Parallelism in Logic Programs. PhD thesis, Computer Science Department, University of Southern California, 1990. Printed as Report TR 91-05.

[16] K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming, 13(2&3):315–347, 1992.

[17] H. Søndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In Proceedings of the 1986 European Symposium on Programming, volume 213 of Lecture Notes in Computer Science, pages 327– 338. Springer-Verlag, Berlin, 1986.

[18] E. Zaffanella, R. Bagnara, and P. M. Hill. Widening Sharing. Submitted for

publication. Available at http://www.cs.unipr.it/~bagnara/, 1999.