freeze/2 goals blocking on variables that have become unreachable

%:- use_module(library(freeze)). % Ciao Prolog needs this freeze_many([],[]). freeze_many([_|Xs],[V|Vs]) :- freeze(V,throw(error(uninstantiation_error(V),big_freeze_test/3))), freeze_many(Xs,Vs). big_freeze_test(N0,N,Zs0) :- ( N0 > N -> true ; freeze_many(Zs0,Zs1), N1 is N0+1, big_freeze_test(N1,N,Zs1) ).

(AMD64) SICStus Prolog 4.3.2 : global stack in use = 108 MB (AMD64) B-Prolog 8.1 : stack+heap in use = 145 MB (i386) Ciao Prolog 1.14.2: global stack in use = 36 MB (~72 MB w/AMD64) (AMD64) SWI-Prolog 7.3.1 : global stack in use = 0.5 MB (AMD64) YAProlog 6.2.2 : global stack in use = 16 MB

TL;DR: ~~bug in SWI~~ no more!

You are creating 500,000 frozen goals which are subsequently unreachable. What do these goals mean? Prolog systems do not analyze a goal as to its semantic relevance (prior to actually executing it). So we have to assume that the goals may be semantically relevant. As the goals are already disconnected, the only semantic effect they might have is to be false and thus making the next answer false.

So it is sufficient to consider freeze(_,false) instead.

Semantically, the predicates p/0 and q/0 are equivalent:

p :-
   false.

q :-
   freeze(_,false).

Procedurally, however, the first goal fails whereas the second succeeds. It is in such situations key to distinguish between solutions and answers. When Prolog succeeds, it produces an answer — most commonly this is known as an answer substitution in Prolog without constraints, where answer substitutions always contain one or infinitely many solutions¹. In the presence of constraints or crude coroutining, an answer may now contain frozen goals or constraints that have to be taken into account to understand which solutions are actually described.

In the case above, the number of solutions is zero. When a system now garbage collects those frozen goals, it actually changes the meaning of the program.

In SICStus this is shown as follows:

| ?- q.
prolog:freeze(_A,user:false) ? ;
no

In SWI and YAP, those goals are not shown by default and thus chances are that bugs as this one have not been discovered.

PS: In the past, there has been a comparison between various systems concerning GC and constraints with SICStus being at that time the only one that passed all tests. In the meantime some systems improved.

I first looked at the SICStus numbers: 216 bytes per freeze! That's 27 words with 13 just for the term representing the goal. So simply 14 words for the freeze. Not so bad.

PPS: the frozen goal was throw/2, it should have been throw/1

^{Fine print
1: Some examples: An answer substitution X = 1 contains exactly one solution, and X = [_A] contains infinitely many solutions like X = [a] and many, many more. All this gets much more complex in the context of constraints.}

Recommended topics

Hot tags