In the analysis of logic programs, abstract domains for detecting sharing and linearity information are widely used. Devising abstract unification algorithms for such domains has proved to be rather hard. At the moment, the available algorithms are correct but not optimal, i.e., they cannot fully exploit the information conveyed by the abstract domains. In this paper, we define a new (infinite) domain ShLin ! which can be thought of as a general framework from which other domains can be easily derived by abstraction. ShLin ! makes the interaction between sharing and linearity explicit. We provide a constructive characterization of the optimal abstract unification operator on ShLin ! and we lift it to two well-known abstractions of ShLin ! . Namely, to the classical Sharing × Lin abstract domain and to the more precise ShLin 2 abstract domain by Andy King. In the case of
In most of the work combining sharing and linearity, freeness information is included in the abstract domain. In fact, freeness may improve the precision of the aliasing component and it is also interesting by itself, for example in the parallelization of logic programs @cite_18 . In this comparison, we do not consider the freeness component.
@cite_18
1999281702
Abstract This paper presents some fundamental properties of independent and- parallelism and extends its applicability by enlarging the class of goals eligible for parallel execution. A simple model of (independent) and-parallel execution is proposed and issues of correctness and efficiency are discussed in the light of this model. Two conditions, “strict” and “nonstrict” independence, are defined and then proved sufficient to ensure correctness and efficiency of parallel execution: If goals which meet these conditions are executed in parallel, the solutions obtained are the same as those produced by standard sequential execution. Also, in the absence of failure, the parallel proof procedure does not generate any additional work (with respect to standard SLD resolution), while the actual execution time is reduced. Finally, in case of failure of any of the goals, no slowdown will occur. For strict independence, the results are shown to hold independently of whether the parallel goals execute in the same environment or in separate environments. In addition, a formal basis is given for the automatic compile-time generation of independent and-parallelism: Compiletime conditions to efficiently check goal independence at run time are proposed and proved sufficient. Also, rules are given for constructing simpler conditions if information regarding the binding context of the goals to be executed in parallel is available to the compiler.