新しいトレイトソルバーにおけるキャッシュ
トレイトソルバーの結果をキャッシュすることは、パフォーマンスのために必要です。
それが健全であることを確認しなければなりません。キャッシュは
SearchGraph によって処理されます。
グローバルキャッシュ
中核において、キャッシュはかなり単純です。ゴールを評価するとき、 それがグローバルキャッシュにあるかを確認します。ある場合は、そのエントリを再利用します。ない場合は、 ゴールを計算し、その結果をキャッシュに格納します。
インクリメンタルコンパイルを扱うため、ゴールの計算は
DepGraph::with_anon_task の内部で行われます。これは、この計算内で使用されたすべてのクエリに依存する新しい DepNode を作成します。
その後、グローバルキャッシュにアクセスするときに、この
DepNode を読み取り、使用されたすべてのクエリへの依存関係エッジを手動で追加します: ソース。
オーバーフローへの対処
新しいトレイトソルバーで再帰制限に達することは致命的ではなく、代わりに単に 曖昧性を返します: ソース。そのため、再帰制限に達したかどうかは、 コンパイル失敗を引き起こすことなく結果を変化させる可能性があります。つまり、 キャッシュ結果にアクセスするときには、残りの利用可能な深さを考慮しなければなりません。
これは、キャッシュエントリにより多くの情報を格納することで行います。評価が
再帰制限に達しなかったゴールについては、単にその到達深さを格納します: ソース。
これらの結果は、現在の available_depth がその
reached_depth より大きい限り、自由に使用できます: ソース。その後、
グローバルキャッシュエントリを使用したかどうかが観測可能にならないように、
現在のゴールの到達深さを更新します: ソース。
再帰制限に達するゴールについては、現在のところ、利用可能な深さがエントリの深さと 正確に一致する 場合にのみキャッシュ結果を使用します。そのため、各ゴールのキャッシュエントリには、 残りの深さごとに別個の結果が含まれます: ソース。1
サイクルの処理
トレイトソルバーはサイクルをサポートしなければなりません。これらのサイクルは、
参加するゴールに応じて帰納的または共帰納的です。詳細については
chapter on coinduction を参照してください。サイクルヘッドとサイクルルートを区別します。スタックエントリは、
再帰的にアクセスされた場合にサイクルヘッドです。ルート は、いずれかのサイクルに
関与しているスタック上で最も深いゴールです。次の依存関係ツリーでは、A と B はどちらも
サイクルヘッドですが、ルートは A だけです。
graph TB
A --> B
B --> C
C --> B
C --> A
サイクル参加者の結果は、まだスタック上にあるゴールの結果に依存します。
しかし、現在その結果を計算しているところなので、その結果はまだ不明です。これは、
不動点に達するまでサイクルヘッドを評価することで処理されます。最初のイテレーションでは、
サイクルが共帰納的かどうかに応じて、制約なしの成功またはオーバーフローのいずれかを
返します: ソース。サイクルのヘッドを評価した後、
その provisional_result がこのイテレーションの結果と等しいかどうかを確認します。等しい場合、
このサイクルの評価は完了しており、その結果を返します。等しくない場合は、暫定結果を更新し、
ゴールを再評価します: ソース。最初のイテレーションの後は、
サイクルが共帰納的か帰納的かは問題ではありません。常に暫定結果を使用します。
サイクルルートのみをキャッシュする
サイクルルートの評価が完了するまで、どのサイクル参加者の結果もグローバルキャッシュに移動することはできません。 しかし、サイクルを完全に評価した後であっても、ルート自体を除く すべての参加者の結果を破棄せざるを得ません。
すべてのグローバルキャッシュエントリのクエリ依存関係を追跡します。これにより、
サイクル参加者のキャッシュは自明ではなくなります。サイクルルートの DepNode を単純に再利用することはできません。2
サイクル A -> B -> A がある場合、A の DepNode には A -> B からの依存関係が含まれます。
このエントリを B に再利用すると、ソースが変更された場合に壊れる可能性があります。B -> A の
エッジはもはや存在しないかもしれず、A は完全に削除されているかもしれません。これは容易に
ICE につながる可能性があります。
しかし、サイクルの結果はどのゴールがルートであるかによって変化する可能性があるため、さらに悪いです: 例。これにより、キャッシュをさらに弱める必要があります。 そのルートを含むサイクルの参加者であったスタックエントリが存在する場合、 サイクルルートのキャッシュエントリを使用してはなりません。これは、指定されたルートのすべてのサイクル参加者を そのグローバルキャッシュエントリに格納し、それがスタックの要素を含まないことを確認することで行います: ソース。
暫定キャッシュ
TODO: これを書く :3
- 暫定結果のスタック依存性
- エッジケース: 暫定キャッシュが挙動に影響する
-
これは過度に制限的です。すべてのネストされたゴールが、ある利用可能な深さ
nで オーバーフロー応答を返す場合、それらの結果はnより小さい任意の深さで同じであるべきです。 この最適化は将来実装できます。 ↩ -
関連する Zulip thread の要約 ↩