freeze/2 个目标阻止了无法访问的变量

Question

我编写了以下小程序来确定当 X 变得无法访问时是否回收用于 freeze(X,Goal) 等目标的内存：

%:- 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)
   ).

让我们运行下面的查询...

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

...使用不同的 Prolog 处理器并查看内存消耗。 多么不同！

(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

当运行使用 ?- length(Zs,1000), big_freeze_test(1,10000,Zs). 进行更多迭代时，我进行了以下观察：

Ciao Prolog 在中止前报告 {ERROR: Memory allocation failed [in Realloc()]}。
sicstus-prolog and b-prolog分配越来越多，直到机器死机。
swi-prolog 在 3.554 秒内执行所有迭代。
yap 也执行所有迭代，但需要 36.910 秒。

任何想法为什么它适用于 SWI-Prolog 和 YAProlog，但不适用于其他的？

考虑到运行时间，为什么 SWI-Prolog 比 YAProlog 快一个数量级以上？

我的直觉倾向于 "attributed variables" 与 "garbage collection" 的互动。 SWI-Prolog 和 YAProlog 具有（共享？）与其他 Prolog 处理器不同的属性变量 API 和实现……而且，它可能是完全不同的东西。谢谢！

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

freeze/2 个目标阻止了无法访问的变量

freeze/2 goals blocking on variables that have become unreachable

prolog

prolog-coroutining