Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-05T16:27:28.320Z Has data issue: false hasContentIssue false
  • English
  • Français

On the interaction between sharing and linearity

Published online by Cambridge University Press:  24 September 2009

GIANLUCA AMATO  and
FRANCESCA SCOZZARI
GIANLUCA AMATO
Affiliation:
Dipartimento di Science, Università “G. d'Annunzio” di Chieti–Pescara, Pescara, Italy (e-mail: [email protected], [email protected])
FRANCESCA SCOZZARI
Affiliation:
Dipartimento di Science, Università “G. d'Annunzio” di Chieti–Pescara, Pescara, Italy (e-mail: [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

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 ShLin2 abstract domain by Andy King. In the case of single-binding substitutions, we obtain optimal abstract unification algorithms for such domains.

Keywords

static analysisabstract interpretationsharinglinearityunification
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 10 , Issue 1 , January 2010 , pp. 49 - 112
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Amato, G. and Scozzari, F. 2002. Optimality in goal-dependent analysis of sharing. In Proc. of the Joint Conference on Declarative Programming (AGP'02), Moreno-Navarro, J. J. and Mariño-Carballo, J., Eds. Universidad Politécnica de Madrid, Madrid, 189–205.Google Scholar
Amato, G. and Scozzari, F. 2003. A general framework for variable aliasing: Towards optimal operators for sharing properties. In Logic Based Program Synthesis and Transformation 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17–20, 2002. Revised Selected Papers, Leuschel, M., Ed. Lecture Notes in Computer Science, vol. 2664. Springer, Berlin Heidelberg, 52–70.Google Scholar
Amato, G. and Scozzari, F. 2005. On Abstract Unification for Variable Aliasing, Technical Report TR-05-08. Dipartimento di Informatica, Università di Pisa.Google Scholar
Amato, G. and Scozzari, F. 2009. Optimality in goal-dependent analysis of sharing. Theory and Practice of Logic Programming 9, 5 (September), 617–689.CrossRefGoogle Scholar
Armstrong, T., Marriott, K., Schachte, P. and Søndergaard, H. 1994. Boolean functions for dependency analysis: Algebraic properties and efficient representation. In Static Analysis, 1st International Static Analysis Symposium, SAS'94 Namur, Belgium, September 28–30, 1994, Proc., Le Charlier, B., Ed. Lecture Notes in Computer Science, vol. 864. Springer, Berlin Heidelberg, 266–280.Google Scholar
Bagnara, R., Hill, P. M. and Zaffanella, E. 2002. Set-sharing is redundant for pair-sharing. Theoretical Computer Science 277, 1–2 (April), 3–46.CrossRefGoogle Scholar
Bagnara, R., Zaffanella, E. and Hill, P. M. 2005. Enhanced sharing analysis techniques: A comprehensive evaluation. Theory and Practice of Logic Programming 5, 1–2 (January), 1–43.CrossRefGoogle Scholar
Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M. V., López-García, P. and Puebla, G. 1997. The Ciao Prolog System: Reference Manual [online], Technical Report CLIP3/97. School of Computer Science, Technical University of Madrid (UPM). Accessed 14 July 2009. URL: http://www.ciaohome.org/Google Scholar
Bueno, F. and García de la Banda, M. J. 2004. Set-sharing is not always redundant for pair-sharing. In Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004, Proc., Kameyama, Y. and Stuckey, P. J., Eds. Lecture Notes in Computer Science, vol. 2998. Springer, Berlin Heidelberg, 117–131.Google Scholar
Codish, M., Dams, D. and Yardeni, E. 1991. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In Logic Programming, Proc. of the Eighth International Conference, Furukawa, K., Ed. MIT Press, Cambridge, MA, 79–93.Google Scholar
Codish, M., Lagoon, V. and Bueno, F. 2000. An algebraic approach to sharing analysis of logic programs. The Journal of Logic Programming 42, 2 (February), 110–149.CrossRefGoogle Scholar
Codish, M., Marriott, K. and Taboch, C. 2000. Improving program analyses by structure untupling. The Journal of Logic Programming 43, 3 (June), 251–263.CrossRefGoogle Scholar
Codish, M., Søndergaard, H. and Stuckey, P. J. 1999. Sharing and groundness dependencies in logic programs. ACM Transactions on Programming Languages and Systems 21, 5 (September), 948–976.CrossRefGoogle Scholar
Cortesi, A. and Filé, G. 1999. Sharing is optimal. The Journal of Logic Programming 38, 3 (March), 371–386.CrossRefGoogle Scholar
Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C. and Ranzato, F. 1997. Complementation in abstract interpretation. ACM Transactions on Programming Languages and Systems 19, 1 (January), 7–47.CrossRefGoogle Scholar
Cortesi, A., Filé, G. and Winsborough, W. W. 1998. The quotient of an abstract interpretation. Theoretical Computer Science 202, 1–2 (July), 163–192.CrossRefGoogle Scholar
Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In POPL '79: Proc. of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of programming languages. ACM Press, New York, 269–282.CrossRefGoogle Scholar
Cousot, P. and Cousot, R. 1992a. Abstract interpretation and applications to logic programs. The Journal of Logic Programming 13, 2–3 (July), 103–179.CrossRefGoogle Scholar
Cousot, P. and Cousot, R. 1992b. Abstract interpretation frameworks. Journal of Logic and Computation 2, 4 (August), 511–549.CrossRefGoogle Scholar
Cousot, P. and Cousot, R. 1992c. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation [Invited paper]. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP '92, Leuven, Belgium, August 26–28, 1992, Proc., Bruynooghe, M. and Wirsing, M., Eds. Lecture Notes in Computer Science, vol. 631. Springer, Berlin Heidelberg, 269–295.Google Scholar
Hans, W. and Winkler, S. 1992. Aliasing and Groundness Analysis of Logic Programs through Abstract Interpretation and Its Safety [online], Technical Report. 92–27. Technical University of Aachen (RWTH Aachen). Accessed 10 July 2009. URL: http://sunsite.informatik.rwth-aachen.de/Publications/AIBGoogle Scholar
Hermenegildo, M. V. and Rossi, F. 1995. Strict and nonstrict independent and-parallelism in logic programs: Correctness, efficiency, and compile-time conditions. The Journal of Logic Programming 22, 1 (January), 1–45.CrossRefGoogle Scholar
Hill, P. M., Zaffanella, E. and Bagnara, R. 2004. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Theory and Practice of Logic Programming 4, 3 (May), 289–323.CrossRefGoogle Scholar
Howe, J. M. and King, A. 2003. Three optimisations for sharing. Theory and Practice of Logic Programming 3, 2 (January), 243–257.CrossRefGoogle Scholar
Jacobs, D. and Langen, A. 1992. Static analysis of logic programs for independent AND parallelism. The Journal of Logic Programming 13, 2–3 (July), 291–314.CrossRefGoogle Scholar
Jones, N. D. and Søndergaard, H. 1987. A semantics-based framework for the abstract interpretation of Prolog. In Abstract Interpretation of Declarative Languages, Abramsky, S. and Hankin, C., Eds. Ellis Horwood, Chichester, UK, 123–142.Google Scholar
King, A. 1994. A synergistic analysis for sharing and groundness which traces linearity. In Programming Languages and Systems – ESOP '94, 5th European Symposium on Programming, Edinburg, U.K., April 11–13, 1994, Proc., Sannella, D., Ed. Lecture Notes in Computer Science, vol. 788. Springer, Berlin Heidelberg, 363–378.Google Scholar
King, A. 2000. Pair-sharing over rational trees. The Journal of Logic Programming 46, 1–2 (November–December), 139–155.CrossRefGoogle Scholar
Lagoon, V. and Stuckey, P. J. 2002. Precise pair-sharing analysis of logic programs. In PPDP '02: Proc. of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. ACM Press, New York, 99–108.CrossRefGoogle Scholar
Langen, A. 1990. Static Analysis for Independent And-Parallelism in Logic Programs, PhD thesis. University of Southern California, Los Angeles.Google Scholar
Levi, G. and Spoto, F. 2003. Pair-independence and freeness analysis through linear refinement. Information and Computation 182, 1 (April), 14–52.CrossRefGoogle Scholar
Mac Lane, S. 1988. Categories for the Working Mathematician, 2nd ed. Graduate Texts in Mathematics, vol. 5. Springer, Berlin Heidelberg.Google Scholar
Marriott, K., Søndergaard, H., and Jones, N. D. 1994. Denotational abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems 16, 3 (May), 607–648.CrossRefGoogle Scholar
Muthukumar, K. and Hermenegildo, M. V. 1992. Compile-time derivation of variable dependency using abstract interpretation. The Journal of Logic Programming 13, 2–3 (July), 315–347.CrossRefGoogle Scholar
Søndergaard, H. 1986. An application of abstract interpretation of logic programs: Occur check reduction. In ESOP '86, European Symposium on Programming, Saarbrcken, Federal Republic of Germany, March 17–19, 1986, Proc., Robinet, B. and Wilhelm, R., Eds. Lecture Notes in Computer Science, vol. 213. Springer, Berlin Heidelberg, 327–338.CrossRefGoogle Scholar
Sterling, L. and Shapiro, E. Y. 1994. The Art of Prolog: Advanced Programming Techniques, 2nd ed. MIT Press, Cambridge, MA.Google Scholar