Inferring non-suspension conditions for logic programs with dynamic scheduling

Genaim, Samir and King, Andy (2008) Inferring non-suspension conditions for logic programs with dynamic scheduling. ACM Transactions on Computational Logic, 9 (3). pp. 182-196. ISSN 1529-3785. (Full text available)

PDF
Download (414kB)
[img]
Preview
Official URL
http://dx.doi.org/10.1145/1352582.1352585

Abstract

A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of subgoal selection. The order of subgoal selection is often controlled with delay declarations that specify that a subgoal is to suspend until some condition on its arguments is satisfied. Reasoning about delay declarations is notoriously difficult for the programmer and it is not unusual for a program and a goal to reduce to a state that contains a subgoal that suspends indefinitely. Suspending subgoals are usually unintended and often indicate an error in the logic or the control. A number of abstract interpretation schemes have therefore been proposed for checking that a given program and goal cannot reduce to such a state. This article considers a reversal of this problem, advocating an analysis that for a given program infers a class of goals that do not lead to suspension. This article shows that this more general approach can have computational, implementational and user-interface advantages. In terms of user-interface, this approach leads to a lightweight point-and-click mode of operation in which, after directing the analyser at a file, the user merely has to inspect the results inferred by the analysis. In terms of implementation, the analysis can be straightforwardly realized as two simple fixpoint computations. In terms of computation, by modeling n! different schedulings of n subgoals with a single Boolean function, it is possible to reason about the suspension behavior of large programs. In particular, the analysis is fast enough to be applied repeatedly within the program development cycle. The article also demonstrates that the method is precise enough to locate bugs in existing programs.

Item Type: Article
Uncontrolled keywords: languages; theory; verification; abstract interpretation; concurrency; logic programming; debugging
Subjects: A General Works
Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Faculties > Science Technology and Medical Studies > School of Computing
Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Depositing User: Suzanne Duffy
Date Deposited: 04 Mar 2009 14:23
Last Modified: 25 Jun 2014 13:03
Resource URI: http://kar.kent.ac.uk/id/eprint/15105 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year