freeze/2 goals blocking on variables that have become unreachable

Question

I made the following little program to determine if the memory used for goals like freeze(X,Goal) is reclaimed when X becomes 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)
   ).

Let's run the following query...

?- statistics, length(Zs,1000), big_freeze_test(1,500,Zs), statistics.

... with different Prolog processors and look at memory consumption. What a difference!

(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

When running more iterations with ?- length(Zs,1000), big_freeze_test(1,10000,Zs)., I made the following observations:

• Ciao Prolog reports {ERROR: Memory allocation failed [in Realloc()]} before aborting.

• sicstus-prolog and b-prolog allocate more and more until the machine freezes.

• swi-prolog performs all iterations in 3.554 seconds.
• yap also performs all iterations, but takes 36.910 seconds.

Any ideas why it works with SWI-Prolog and YAProlog, but not with the other ones?

Considering runtime, how come SWI-Prolog beats YAProlog by more than an order of magnitude?

My intuition is leaning towards the interaction of "attributed variables" with "garbage collection". SWI-Prolog and YAProlog have (share?) a different attributed variable API and implementation than the other Prolog processors ... and, then again, it could be something completely different. Thank you!

Answer 1

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.}