freeze/2 目标阻止已变得无法访问的变量 [英] freeze/2 goals blocking on variables that have become unreachable
问题描述
我制作了以下小程序来确定内存是否用于 freeze(X,Goal) 在 X 变得不可达时被回收:
%:- use_module(library(freeze)).% Ciao Prolog 需要这个freeze_many([]，[]).freeze_many([_|Xs],[V|Vs]) :-冻结(V，抛出(错误(uninstantiation_error(V)，big_freeze_test/3)))，freeze_many(Xs,Vs).big_freeze_test(N0,N,Zs0) :-(N0＞N->真的;freeze_many(Zs0,Zs1),N1 是 N0+1，big_freeze_test(N1,N,Zs1)).让我们运行以下查询...
?- 统计，长度(Zs，1000)，big_freeze_test(1,500，Zs)，统计.... 使用不同的 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 和实现......而且，再一次，它可能是完全不同的东西.谢谢！
TL;DR: SWI 中的错误 没有了！
您正在创建 500,000 个随后无法达到的冻结目标.这些目标意味着什么?Prolog 系统不会分析目标的语义相关性(在实际执行之前).所以我们必须假设目标可能在语义上是相关的.由于目标已经脱节，它们可能具有的唯一语义效果是错误的，从而使下一个答案为错误.
所以考虑 freeze(_,false) 就足够了.
在语义上，谓词 p/0 和 q/0 是等价的:
p :-错误的.问:-冻结(_，假).然而，在程序上，第一个目标失败，而第二个目标成功.在这种情况下，区分解决方案和答案是关键.当 Prolog 成功时，它会产生一个答案 —最常见的是，这在 Prolog 中称为答案替换，没有约束，其中答案替换总是包含一个或无限多个解决方案1.在存在约束或粗略协同的情况下，答案现在可能包含冻结的目标或约束，必须考虑这些目标或约束才能了解实际描述了哪些解决方案.
在上述情况下，解决方案的数量是零.当一个系统现在垃圾收集那些冻结的目标时，它实际上改变了程序的含义.
在 SICStus 中显示如下:
<代码>|?- 问.序言:冻结(_A，用户:假)?;不
在 SWI 和 YAP 中，默认情况下不显示这些目标，因此很可能没有发现与此类似的错误.
<小时>PS:过去，有 a比较各种关于 GC 和约束的系统，其中 SICStus 是当时唯一通过所有测试的系统.与此同时，一些系统得到了改进.
我首先查看了 SICStus 数字:每次冻结 216 字节！那是 27 个单词，其中 13 个单词只是代表目标的术语.所以只需 14 个字的冻结.还不错.
PPS:冻结的目标是 throw/2，它应该是 throw/1
<支持>细则1:一些例子:答案替换 X = 1 只包含一个解决方案，而 X = [_A] 包含无限多个解决方案，例如 X = [a] 等等.在约束的上下文中，所有这些变得更加复杂.
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!
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 solutions1. 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 目标阻止已变得无法访问的变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
