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：使用中的全局堆栈 = 108 MB (AMD64) B-Prolog 8.1：使用中的堆栈+堆 = 145 MB (i386) Ciao Prolog 1.14.2：使用中的全局堆栈 = 36 MB（~72 MB w/AMD64） (AMD64) SWI-Prolog 7.3.1：使用中的全局堆栈 = 0.5 MB (AMD64) YAProlog 6.2.2：使用中的全局堆栈 = 16 MB

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

• Ciao Prolog 在中止前报告{ERROR: Memory allocation failed [in Realloc()]}。

• sicstus-prolog 和 b-prolog 分配越来越多，直到机器死机。

• swi-prolog 在 3.554 秒内执行所有迭代。
• yap 也执行所有迭代，但需要 36.910 秒。

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

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

我的直觉倾向于“属性变量”与“垃圾收集”的相互作用。 SWI-Prolog 和 YAProlog 具有（共享？）与其他 Prolog 处理器不同的属性变量 API 和实现......而且，再一次，它可能是完全不同的东西。 谢谢！

Answer 1

TL;DR：bug in SWI 没有了！

您正在创建 500,000 个随后无法达到的冻结目标。这些目标意味着什么？ Prolog 系统不分析目标的语义相关性（在实际执行之前）。所以我们必须假设目标可能在语义上是相关的。由于目标已经脱节，它们可能具有的唯一语义效果是错误的，从而使下一个答案为错误。

所以考虑freeze(_,false) 就足够了。

在语义上，谓词p/0 和q/0 是等价的：

p :-
   false.

q :-
   freeze(_,false).

然而，在程序上，第一个目标失败，而第二个目标成功。在这种情况下，区分解决方案和答案是关键。当 Prolog 成功时，它会产生一个答案——这在 Prolog 中通常称为 答案替换，没有约束，其中答案替换总是包含一个或无限多个解决方案¹。在存在约束或粗略的协程的情况下，答案现在可能包含冻结的目标或约束，必须考虑这些目标或约束才能了解实际描述了哪些解决方案。

在上述情况下，解决方案的数量是零。当系统现在垃圾收集那些冻结的目标时，它实际上改变了程序的含义。

在 SICStus 中显示如下：

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

在 SWI 和 YAP 中，默认情况下不显示这些目标，因此很可能没有发现与此类似的错误。

---

PS：过去，在各种系统之间存在a comparison，涉及 GC 和约束，当时 SICStus 是唯一通过所有测试的系统。与此同时，一些系统得到了改进。

我首先查看了 SICStus 数字：每次冻结 216 字节！那是 27 个单词，其中 13 个单词只是代表目标的术语。所以只需 14 个单词就可以冻结。还不错。

PPS：冻结的目标是throw/2，应该是throw/1

---

^{细则 1：一些例子：答案替换 X = 1 只包含一个解决方案，X = [_A] 包含无限多个解决方案，例如 X = [a] 等等。所有这些gets much more complex 都在约束的上下文中。}