Proving deadlock freedom of logic programs with dynamic scheduling
In increasingly many logic programming systems, the Prolog left to right selection rule has been replaced with dynamic selection rules, that select an atom of a query among those satisfying suitable conditions. These conditions describe the form of the arguments of every program predicate, by means of a so-called delay declaration. Dynamic selection rules introduce the possibility of deadlock, an abnormal form of termination that occurs if the query is non-empty and it contains no `selectable' atoms. In this paper, we introduce a simple compositional assertional method for proving deadlock freedom. The method is based on the notion of suspension cover, a static description of the possible dynamic schedulings of the body atoms of a clause, according to a given delay declaration. In the method, we assume that monotonic assertions are used for specifying the conditions of the delay declaration. Apart sections are devoted to two more practical instances of the method, that use types and modes, respectively.
|Logic Programming (acm D.1.6), Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)|
|Logic programming (msc 68N17), Complexity classes (hierarchies, relations among complexity classes, etc.) (msc 68Q15), Theory of computing (msc 68Qxx), Specification and verification (program logics, model checking, etc.) (msc 68Q60)|
|Department of Computer Science [CS]|
Marchiori, E, & Teusink, F. J. M. (1996). Proving deadlock freedom of logic programs with dynamic scheduling. Department of Computer Science [CS]. CWI.