ESH: Enhanced Sharing Analysis Techniques

[Page last updated on 2001/03/05 08:13:09.]

Choose a precision comparison
Choose a time comparison
View a (very) short description of the abstract domains considered

For each domain instance of a precision or time comparison, we provide three different formats:

Full: a detailed report of all the results obtained. The tables contain a row for each program in the benchmark suite.
Diff: a detailed report of all the analysis differences. The tables contain a row for each program that produced different results when analyzed with the two domains considered. For time comparisons, analyses times are considered equal whenever their difference is under a given threshold (0.1 seconds).
Summ: a summary of the analyses results, where the benchmark suite is partitioned into several precision/performance classes and the cardinality of each class is shown.

The precision comparisons

Comparison	Goal Independent		Goal Dependent
Comparison	w/o struct. info.	with struct. info.	w/o struct. info.	with struct. info.
SFL vs Pos x SFL	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Pattern(Pos x SFL)	Full \| Diff \| Summ		Full \| Diff \| Summ
Pos x SFL vs Star-union order	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Free-Lin order	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Reverse order	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Enhanced Pos	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Ground or free	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Enhanced linearity	Not meaningful	Full \| Diff \| Summ	Not meaningful	Full \| Diff \| Summ
Pos x SFL vs Enhanced freeness	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ

The analysis time comparisons

Comparison	Goal Independent		Goal Dependent
Comparison	w/o struct. info.	with struct. info.	w/o struct. info.	with struct. info.
SFL vs Pos x SFL	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Pattern(Pos x SFL)	Full \| Diff \| Summ		Full \| Diff \| Summ
Pos x SFL vs Star-union order	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Free-Lin order	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Reverse order	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Enhanced Pos	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Ground or free	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ
Pos x SFL vs Enhanced linearity	Not meaningful	Full \| Diff \| Summ	Not meaningful	Full \| Diff \| Summ
Pos x SFL vs Enhanced freeness	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ	Full \| Diff \| Summ

The domains considered

Domain	Description
SFL	The (almost) standard combination of possible sharing (S) with definite freeness (F) and linearity (L) information. We use the reduced set-sharing domain PSD, which has the same precision of the classical set-sharing domain of Jacobs&Langen (SH), as far as we observe variable independence and groundness information. The abstract execution of the grounding bindings is anticipated. The non-grounding bindings are then executed in the textual (left-to-right) order.
Pos x SFL	A combination of the domain SFL with the domain Pos (the positive Boolean functions) for tracking groundness dependencies. In this combination, the set of ground variables computed by Pos is used in the abstract operators of SFL to remove redundant sharing groups, to improve linearity information and to detect and anticipate more grounding bindings.
Pattern(Pos x SFL)	The integration of the domain Pos x SFL with the explicit structural information encoded by the Pattern(.) construction. In order to compare the comparison with the base domain Pos x SFL, the computed structural information is thrown away at the end of the analysis.
Star-union order	The domain Pos x SFL where the non-grounding bindings requiring star-unions are delayed.
Free-Lin order	The domain Pos x SFL where the non-grounding bindings that maximizes freeness and linearity information are executed first.
Reverse order	The domain Pos x SFL where the non-grounding bindings are executed right-to-left.
Enhanced Pos	An improved combination of SFL with Pos, where at each step the reduced product of the Pos component and the set-sharing component (S) is computed.
Ground or free	The combination of the domain Pos x SFL with a new component representing the set of variables that are either ground or free.
Enhanced linearity	The usual domain Pos x SFL with an improved version of the abstract mgu operator, better exploiting the interaction between definite linearity, possible sharing and explicit structural information.
Enhanced freeness	The usual domain Pos x SFL with an improved version of the abstract mgu operator, better exploiting the interaction between definite freeness and possible sharing information.