6

次のような小さなプログラムを作成して、到達不能になったときに目標に使用されたメモリfreeze(X,Goal)が回収されるかどうかを判断しました。X

%:- 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 (AMD64 では ~72 MB)
(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()]}中止する前に報告します。

  • とは、マシンがフリーズするまで割り当てを増やします。

  • は、すべての反復を3.554秒で実行します。
  • もすべての反復を実行しますが、36.910秒かかります。

SWI-Prolog と YAProlog では機能するが、他のものでは機能しない理由はありますか?

実行時間を考えると、SWI-Prolog が YAProlog よりも 1 桁以上優れているのはなぜですか?

私の直感は、「属性変数」と「ガベージ コレクション」の相互作用に傾いています。SWI-Prolog と YAProlog は、他の Prolog プロセッサとは異なる属性付き変数 API と実装を (共有?) 持っています。ありがとうございました！

4

1 に答える 1

3

TL;DR: SWI のバグはもうありません!

後で到達できない 500,000 個の凍結された目標を作成しています。これらの目標は何を意味するのでしょうか? Prolog システムは、(実際に実行する前に) その意味的関連性に関してゴールを分析しません。したがって、目標が意味的に関連している可能性があると想定する必要があります。ゴールはすでに切り離されているため、唯一のセマンティック効果は false であるため、次の答えが false になります。

freeze(_,false)したがって、代わりに検討するだけで十分です。

意味的には、述語p/0とq/0は同等です。

p :-
   false.

q :-
   freeze(_,false).

ただし、手続き的には、最初の目標は失敗しますが、2 番目の目標は成功します。このような状況では、解決策と回答を区別することが重要です。Prolog が成功すると、答えが生成されます。最も一般的には、これはProlog で制約のない答えの置換として知られています。この場合、答えの置換には常に 1 つまたは無限に多くの解が含まれます1。制約または大雑把なコルーチンが存在する場合、回答には、どのソリューションが実際に記述されているかを理解するために考慮しなければならない、凍結された目標または制約が含まれる場合があります。

上記の場合、解の数は0です。システムがこれらの凍結された目標をガベージコレクションすると、プログラムの意味が実際に変わります。

SICStus では、これは次のように示されます。

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

SWI と YAP では、これらのゴールはデフォルトでは表示されないため、このようなバグが発見されていない可能性があります。

PS: 過去に、 GC と制約に関するさまざまなシステム間の比較が行われましたが、その時点ですべてのテストに合格したのは SICStus だけでした。その間、いくつかのシステムが改善されました。

私は最初に SICStus の数値を見ました: フリーズあたり 216 バイトです! これは、目標を表す用語だけで 13 語を含む 27 語です。つまり、フリーズには 14 ワードしかありません。そんなに悪くない。

PPS: 凍結された目標は でしたthrow/2。throw/1

細字 1: いくつかの例: 回答の置換X = 1には、厳密に 1 つのソリューションがX = [_A]含まれ、無限に多くのソリューションが含まれX = [a]ます。制約のコンテキストでは、これらすべてがより複雑になります。

于 2015-06-28T13:06:44.700 に答える