Blog of Raivo Laanemets

Software development and personal stories.

Runtime determinism checker for SWI-Prolog

On 2015-11-08

Last weekend I built a runtime checker for deterministic predicates. Deterministic predicates should never fail and should produce only a single answer. In Prolog it's common to get answer "No" for buggy code without any more details. The issue is same in a web application where this is just logged as an error of a failing request handler. Most predicates dealing with database queries and view rendering are deterministic and it would be nice to get extra information when one of them fails.

Solution

My solution is to annotate deterministic predicates so that the runtime can automatically wrap them with a check. This is similar to the static mode checker in the Mercury language. However, I only check for det category and do it at runtime.

The major part of the checker (~50 lines of code) deals with the Prolog module system, everything else is almost trivial. Calls of annotated predicates get wrapped into an in-then-else.

somepred(Args),

is transformed into:

(   somepred(Args)
->  true
;   throw(error(goal_failed(...)))),

The call transformation is done through the standard expand_goal metaprogramming interface.

Example

The following example implements insertion sort. It has multiple deterministic predicates (for the input/output instantiation modes they are to be intended for). The last clause of insert/3 is intentionally broken for number lists.

:- use_module(library(rdet)).

:- rdet(insert_sort/2).
:- rdet(i_sort/3).
:- rdet(insert/3).

insert_sort(List, Sorted):-
    i_sort(List, [], Sorted).

i_sort([], Acc, Acc).
i_sort([H|T], Acc, Sorted):-
    insert(H,Acc,NAcc),
    i_sort(T,NAcc,Sorted).

insert(X,[Y|T],[Y|NT]):-
    X>Y,
    insert(X,T,NT).

insert(X,[Y|T],[X,Y|T]):-
    X=<Y.

insert(X,[a],[X]).

Running the example will throw an error. This will print the error on SWI console if you do not catch the error:

?- insert_sort([2,4,1,3], Sorted).
ERROR: Unhandled exception: Goal insert/3 failed in module user on line 11.

Overhead

I was expecting about 20%-50% overhead on the sorting example but found it to run much faster than the original version. Raw performance numbers (insert/3 fixed) on my computer:

with annotations commented out:

?- findall(X, between(1, 1000, X), Xs), time(insert_sort(Xs, Sorted)).
% 1,001,001 inferences, 0.386 CPU in 0.391 seconds (98% CPU, 2596612 Lips)
Xs = Sorted, Sorted = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] .

with annotations enabled:

?- findall(X, between(1, 1000, X), Xs), time(insert_sort(Xs, Sorted)).
% 1,001,002 inferences, 0.217 CPU in 0.218 seconds (100% CPU, 4613383 Lips)
Xs = Sorted, Sorted = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].

Which means that the annotated code runs 40%-50% faster. I believe that this is due to immediately pruning away choice points (annotated predicates discard all solutions besides the first one).

More information

More information can be found from the project repository on GitHub. To install the rdet pack, use pack_install(rdet) goal in SWI-Prolog version 7.x+

Static solution?

A static solution would have to support all of this:

  • Instantiatedness (unbound, ground, partial)
  • Type information (list vs. atom, higher order types)
  • Module system support
  • Supports goal_expansion and other extensions
  • Higher order calls (maplist/call/etc)
  • Static exceptions
  • Different determinism modes: det/semidet/nondet/comitted choice
  • Determinism dependence on all previous

And has all of this optional so that you can combine your code easily with 3rd party untyped/unmoded libraries. The Mercury language contains a static solution supporting most of these things. Currently Mercury lacks HTTP support and larger community which makes it a lot less practical platform than SWI-Prolog. The declarations required for static analysis can also make your program way more verbose.