Suspension analyses for concurrent logic programs

ABSTRACT

Concurrent logic languages specify reactive systems which consist of collections of communicating processes. The presence of unintended suspended computations is a common programming error which is difficult to detect using standard debugging and testing techniques. We develop a number of analyses, based on abstract interpretation, which succeed if a program is definitely suspension free. If an analysis fails, the program may, or may not, be suspension free. Examples demonstrate that the analyses are practically useful. They are conceptually simple and easy to justify because they are based directly on the transition system semantics of concurrent logic programs. A naive analysis must consider all scheduling policies. However, it is proven that for our analyses it suffices to consider only one scheduling policy, allowing for efficient implementation.

REFERENCES

• 1: BARBUTI, R., AND MARTELLI, M. 1990. Recognizing non-floundering logic programs and goals. Int. J. Found. Comput. Sci., 1, 2, 151-163.
• 2: A. Bossi , N. Cocco , M. Fabris, Proving termination of logic programs by exploiting term properties, Proceedings of the international joint conference on theory and practice of software development on Advances in distributed computing (ADC) and colloquium on combining paradigms for software development (CCPSD): Vol. 2, p.153-180, April 1991, Brighton, United Kingdom
• 3: CODISH, M., DAMS, D., AND EYAL, Y. 1991. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis, in Proceedings of the 8th International Conference on Logic Programming. MIT Press, Cambridge, Mass., 79-93.
• 4: CODISH, M., FAI~SCHI, M., AND MARRIOTT, K. 1991. Suspension analysis for concurrent logic programs. In Proceedings of the 8th International Conference on Logic Programming. MIT Press, Cambridge, Mass., 331-345.
• 5: Michael Codish , Moreno Falaschi , Kim Marriott , William H. Winsborough, Efficient Analysis of Concurrent Constraint Logic Programs, Proceedings of the 20th International Colloquium on Automata, Languages and Programming, p.633-644, July 05-09, 1993
• 6: Christian Codognet , Philippe Codognet , Marc-Michel Corsini, Abstract interpretation for concurrent logic languages, Proceedings of the 1990 North American conference on Logic programming, p.215-232, January 1990, Austin, Texas, United States
• 7: CORSINI, M., AND FIL~, G. 1989. A complete framework for the abstract interpretation of logic programs: Theory and application. Tech. Rep., Univ. di Padova, Italy.
• 8: Patrick Cousot , Radhia Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.269-295, August 26-28, 1992
• 9: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 10: Philip W. Dart, On derived dependencies and connected databases, Journal of Logic Programming, v.11 n.2, p.163-188, Aug. 1991 [doi>10.1016/0743-1066(91)90017-J]
• 11: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 12: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 13: Kim Marriott , Harald Søndergaard, Analysis of constraint logic programs, Proceedings of the 1990 North American conference on Logic programming, p.531-547, January 1990, Austin, Texas, United States
• 14: MARRIOTT, K., AND S~NDERGAARD, H. 1989. Semantics-based dataflow analysis of logic programs. In Information Processing 89. North-Holland, Amsterdam.
• 15: Kim Marriott , Harald Søndergaard , Philip Dart, A characterization of non-floundering logic programs, Proceedings of the 1990 North American conference on Logic programming, p.661-680, January 1990, Austin, Texas, United States
• 16: NAISH, L. 1984. Heterogeneous SLD resolution. J. Logic Program. 1, 4.
• 17: Lutz Plümer, Termination proofs for logic programs, Springer-Verlag New York, Inc., New York, NY, 1990
• 18: SATO, T., AND TAMAKI, H. 1984. Enumeration of success patterns in logic programs. Theor. Comput. Sci. 34, 227-240.
• 19: Ehud Shapiro, The family of concurrent logic programming languages, ACM Computing Surveys (CSUR), v.21 n.3, p.413-510, Sep. 1989 [doi>10.1145/72551.72555]
• 20: STATMAN, R. 1985. Logical relations and the typed lambda calculus. Inf. Contr. 65, 85-97.
• 21: E. Yardeni , S. Kliger , K. Kahn , E. Shapiro, The languages FCP(:) and FCP(:,?), New Generation Computing, v.7 n.2-3, p.89-107, 1990 [doi>10.1007/BF03037201]
• 22: K. A. Yelick , J. L. Zachary, Moded type systems for logic programming, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.116-124, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75287]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Concurrent, distributed, and parallel languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Logics of programs
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Languages

Keywords:
abstract interpretation, concurrent logic programming, program analysis