freeze/2 goals blocking on variables that have bec

问题:

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!

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

回答2:

Reclaiming frozen goals is not valid in certain settings. For example in CC this would not be allowed, since a program has at least 3 outcomes:

There is a paper by Evan Tick explaining CC:

A program successfully terminates when, starting from an initial user query (a conjunct of atoms), after some number of reduction steps, no goals remain to be executed, nor are suspended. Alternatively, the program deadlocks if only suspended goals remain. A third result is program failure, which is defined more formally below.

THE DEEVOLUTION OF CONCURRENT LOGIC PROGRAMMING LANGUAGES
Evan Tick - 1995
https://core.ac.uk/download/pdf/82787481.pdf

Here is an example that illustrates the problem. freeze/2 is more primitive than CLP(FD). So CLP(FD) can do the following sometimes:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.21)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- [user].
test(A,B) :- A #< X, X #< B.

?- test(1,2).
false

?- test(1,3).
true

But now if I do the same with freeze I loose all information, since SWI-Prolog reclaimes the frozen goals:

?- [user].
test2(A,B) :- freeze(X,(integer(X),A<X)), freeze(X,(integer(X),X<B)).

?- test2(1,2).
true.

?- test2(1,3).
true.

Maybe some finer control about the garbage collection behaviour is needed.

Edit 1: The suggestion for finer control in SWI-Prolog is to wrap with call_residue_vars/2. I don't know whether this is the most clever solution, but at least it is a solution:

?- call_residue_vars(test2(1,2),L).
L = [_5538],
freeze(_5538,  (integer(_5538), 1<_5538)),
freeze(_5538,  (integer(_5538), _5538<2)).

?- call_residue_vars(test2(1,3),L).
L = [_5544],
freeze(_5544,  (integer(_5544), 1<_5544)),
freeze(_5544,  (integer(_5544), _5544<3)).