White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Correctness, Precision and Efficiency in the Sharing Analysis of Real Logic Languages

Zaffanella, Enea (2001) Correctness, Precision and Efficiency in the Sharing Analysis of Real Logic Languages. PhD thesis, University of Leeds.


Download (2686Kb)


For programming languages based on logic, a knowledge of variable sharing is important; for instance, for their automatic parallelization and for many optimisations of the unification procedure, such as occurs-check reduction. Because of its usefulness, a considerable amount of research has been done on the design and development of techniques for the static analysis of variable sharing. Despite this fact, some of the most important issues related to the specification and implementation of a practical sharing analysis tool, such as the correctness, the precision and the efficiency of the analysis, have lacked satisfactory solutions. The thesis reports on our work in rectifying this situation and, thereby, enhancing the state-of-the-art on sharing analysis. Our contributions include: a correctness proof for the set-sharing domain of Jacobs and Langen that does not depend on the presence of the occurs-check in the concrete unification procedure; the definition of the simpler abstraction of set-sharing that is guaranteed to achieve the same precision on both variable independence and groundness; the specification, on this new domain of an abstract unification operator having polynomial complexity, as opposed to the exponential complexity of the abstract unification operator defined on set-sharing; the generalization of all the above results to a combined abstract domain including set-sharing, freeness and linearity information; an extensive experimental evaluation, including both the validation of the above results as well as the implementation and comparison of many other recent proposals for more precise sharing analysis domains; and the specification of a new representation for set-sharing which, by allowing for the definition of a family of widening operators, solves all the scalability problems of the analysis, while having a negligible impact on its precision.

Item Type: Thesis (PhD)
Additional Information: Supplied directly by the School of Computing, University of Leeds.
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.529166
Depositing User: Dr L G Proll
Date Deposited: 04 Mar 2011 17:18
Last Modified: 07 Mar 2014 11:23
URI: http://etheses.whiterose.ac.uk/id/eprint/1306

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)