冻结/2个目标，阻止无法访问的变量 [英] freeze/2 goals blocking on variables that have become unreachable

问题描述

我编写了以下小程序来确定用于X无法访问时，将回收="nofollow"> freeze(X,Goal) :

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.

...使用不同的Prolog处理器，并查看内存消耗. 有什么不同！

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

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

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

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

sicstus-prolog 和 b-prolog 分配直到机器死机为止.

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

有什么想法为什么可以与SWI-Prolog和YAProlog一起使用，但不能与其他想法一起使用?

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

考虑到运行时，SWI-Prolog与YAProlog的竞争程度如何超过一个数量级?

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

我的直觉倾向于归因变量"与垃圾回收"之间的相互作用.与其他Prolog处理器相比，SWI-Prolog和YAProlog具有(共享?)不同的属性变量API和实现...然后，这又可能是完全不同的. 谢谢！

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!

推荐答案

TL; DR:

TL;DR: bug in SWI no more!

您正在创建500,000个冻结目标，这些目标随后将无法实现.这些目标是什么意思? Prolog系统没有分析目标的语义相关性(在实际执行之前).因此，我们必须假设目标可能在语义上是相关的.由于目标已经脱节，所以它们可能唯一的语义影响就是错误，从而使下一个答案错误.

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.

因此，只需考虑使用freeze(_,false)就足够了.

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

在语义上，谓词p/0和q/0是等效的:

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

p :-
   false.

q :-
   freeze(_,false).

在程序上，第一个目标失败，而第二个目标成功.在这种情况下，区分解决方案和答案是关键. Prolog成功后，将产生一个答案—.最普遍的做法是在Prolog中将其称为答案替换，没有任何限制，其中答案替换始终包含一个或无限多个解决方案 ¹ .现在，在存在约束或粗略的相关性的情况下，答案可能包含冻结的目标或约束，必须理解这些目标或约束才能理解实际描述的解决方案.

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.

在SICStus中，如下所示:

In SICStus this is shown as follows:

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

在SWI和YAP中，默认情况下不会显示这些目标，因此很可能尚未发现该目标的错误.

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:过去，有 a各种有关GC和约束的系统之间的比较，当时SICStus是唯一通过所有测试的系统.同时，一些系统得到了改进.

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.

我首先查看了SICStus编号:每个冻结216个字节！这是27个单词，其中13个仅代表目标.因此，只需冻结14个字即可.还不错.

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:冻结的目标是throw/2，应该是throw/1

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

^{精美打印 1:一些示例:答案替换X = 1仅包含一个解决方案，而X = [_A]包含无限多个解决方案，例如X = [a]和更多很多其他解决方案.在约束的情况下，所有这变得更加复杂.}

^{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个目标，阻止无法访问的变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！