Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

制約伝播

リージョン推論の主な作業は制約伝播であり、 これは propagate_constraints 関数で行われます。NLL で使用される制約には 3 種類あり、これらの制約を一度に 1 種類ずつ「重ねる」ことで propagate_constraints がどのように動作するかを説明します(それぞれは互いにかなり独立しています)。

  • 生存性に由来する、生存性制約(R live at E)。
  • サブタイピングに由来する、outlives 制約(R1: R2)。
  • impl Trait に由来する、メンバー制約member R_m of [R_c...])。

この章では、生存性制約と outlives 制約の両方を扱いながら、制約伝播の「核心」を説明します。

記法と高水準の概念

概念的には、リージョン推論は「不動点」計算です。これは、 何らかの制約の集合 {C} を与えられ、各リージョン R を要素の集合 {E} にマッピングする値の集合 Values: R -> {E} を計算します (リージョン要素に関する追加の注記はこちらを参照してください)。

  • 最初は、各リージョンは空集合にマッピングされるため、すべてのリージョン R について Values(R) = {} です。
  • 次に、不動点に到達するまで制約を繰り返し処理します。
    • 各制約 C について:
      • 制約を満たすために必要に応じて Values を更新します

簡単な例として、生存性制約 R live at E がある場合、 その制約を満たすために Values(R) = Values(R) union {E} を適用できます。 同様に、outlives 制約 R1: R2 がある場合は、 Values(R1) = Values(R1) union Values(R2) を適用できます。 (メンバー制約はより複雑で、このセクションで説明します。)

ただし実際には、もう少し賢い方法を取っています。制約をループ内で適用する代わりに、 制約を解析し、それらを適用する正しい順序を見つけ出すことで、 最終結果を得るために各制約を 1 回だけ適用すればよいようにできます。

同様に、実装では Values 集合は scc_values フィールドに格納されますが、 それらはリージョンではなく強連結成分(SCC)によってインデックス付けされます。 SCC は、多くの冗長な格納と計算を避けるための最適化です。 これらについては outlives 制約のセクションで説明します。

生存性制約

生存性制約は、リージョン R を含む型を持つ何らかの変数が、あるポイント P で生存している場合に発生します。 これは単に、R の値がポイント P を含んでいなければならないことを意味します。 生存性制約は MIR 型チェッカーによって計算されます。

生存性制約 R live at E は、EValues(R) のメンバーである場合に満たされます。 したがって、そのような制約を Values に「適用」するには、 Values(R) = Values(R) union {E} を計算するだけで済みます。

生存性の値は型チェックで計算され、作成時に liveness_constraints 引数でリージョン推論へ渡されます。 ただし、これらは R live at E のような個々の制約として表現されるわけではありません。 代わりに、リージョン変数ごとに(疎な)ビットセット(型は LivenessValues)を格納します。 この方法では、各生存性制約に対して 1 ビットだけが必要です。

言及しておく価値のある点が 1 つあります。すべてのライフタイムパラメーターは、常に関数本体全体にわたって生存しているとみなされます。 これは、それらが呼び出し元の実行の一部に対応しており、その実行には明らかにこの関数で費やされる時間が含まれるためです。 呼び出し元は、私たちが戻るのを待っているからです。

Outlives 制約

outlives 制約 'a: 'b は、'a の値が 'b の値の上位集合でなければならないことを示します。 つまり、outlives 制約 R1: R2 は、Values(R1)Values(R2) の上位集合である場合に満たされます。したがって、そのような制約を Values に「適用」するには、Values(R1) = Values(R1) union Values(R2) を計算するだけで済みます。

ここから得られる 1 つの観察は、R1: R2R2: R1 がある場合、 R1 = R2 が真でなければならないということです。同様に、次がある場合:

R1: R2
R2: R3
R3: R4
R4: R1

すると R1 = R2 = R3 = R4 が成り立ちます。後述するように、私たちはこれを利用して処理を大幅に高速化しています。

コードでは、outlives 制約の集合は、作成時に型 OutlivesConstraintSet のパラメーターとしてリージョン推論コンテキストへ渡されます。 この制約集合は、基本的には単に 'a: 'b 制約のリストです。

outlives 制約グラフと SCC

outlives 制約をより効率的に扱うために、それらはグラフの形式に変換されます。 このグラフのノードはリージョン変数('a, 'b)であり、各制約 'a: 'b は 辺 'a -> 'b を導入します。この変換は、推論コンテキストを作成する RegionInferenceContext::new 関数で行われます。

グラフ表現を使用すると、サイクルを探すことで、等しくなければならないリージョンを検出できます。 つまり、次のような制約がある場合

'a: 'b
'b: 'c
'c: 'd
'd: 'a

これは、要素 'a...'d を含むグラフ内のサイクルに対応します。

したがって、リージョン値を伝播する際に最初に行うことの 1 つは、 制約グラフ内の強連結成分(SCC)を計算することです。 結果は constraint_sccs フィールドに格納されます。 その後、constraint_sccs.scc(r) を呼び出すことで、 リージョン r が属している SCC を簡単に見つけることができます。

SCC に基づいて扱うことで、より効率的にできます。単一の SCC の一部であるリージョンの集合 'a...'d がある場合、それらの値を個別に計算または格納する必要はありません。 それらはすべて等しくなければならないため、SCC に対して 1 つの値だけを格納すればよいのです。

リージョン推論コードを見てみると、多くのフィールドが SCC に基づいて定義されていることがわかります。 たとえば、scc_values フィールドは各 SCC の値を格納します。 したがって、特定のリージョン 'a の値を取得するには、まずそのリージョンが属する SCC を見つけ、 次にその SCC の値を見つけます。

SCC を計算するとき、各 SCC のメンバーであるリージョンがどれかを特定するだけでなく、それらの間のエッジも特定します。たとえば、次の outlives 制約の集合を考えてみましょう。

'a: 'b
'b: 'a

'a: 'c

'c: 'd
'd: 'c

ここには 2 つの SCC があります。S0 は 'a'b を含み、S1 は 'c'd を含みます。しかし、これらの SCC は独立していません。'a: 'c があるため、 S0: S1 も成り立つことになります。つまり、S0 の値は S1 の値の スーパーセットでなければなりません。重要な点の 1 つは、この SCC のグラフが常に DAG であることです。つまり、循環を持つことはありません。これは、すべての循環が SCC 自体を形成するために取り除かれているためです。

生存性制約を SCC に適用する

型チェッカーから渡される生存性制約は、リージョンの観点で表現されています。つまり、 Liveness: R -> {E} のようなマップがあります。しかし、最終結果は SCC の観点で表現したいので、単に和集合を取ることで、これらの生存性制約を非常に簡単に統合できます。

for each region R:
  let S be the SCC that contains R
  Values(S) = Values(S) union Liveness(R)

リージョン推論器では、このステップは RegionInferenceContext::new で行われます。

outlives 制約を適用する

SCC の DAG を計算したら、それを使って計算全体を構造化します。2 つの SCC の間にエッジ S1 -> S2 がある場合、 Values(S1) >= Values(S2) が成り立たなければならないことを意味します。したがって、S1 の値を計算するには、まず各後続ノード S2 の値を計算します。その後、それらの値すべての和集合を単純に取ります。準イテレーター風の記法を使うと、次のようになります。

Values(S1) =
  s1.successors()
    .map(|s2| Values(s2))
    .union()

コードでは、この処理は propagate_constraints 関数で始まります。この関数はすべての SCC を反復処理します。各 SCC S1 について、その後続ノードの値を先に計算することで、その値を計算します。SCC は DAG を形成するため、循環について心配する必要はありません。ただし、特定の SCC をすでに処理したかどうかを追跡するための集合を保持しておく必要はあります。各後続ノード S2 について、S2 の値を計算したら、それらの要素を S1 の値に union できます。(ただし、この処理では、高ランクプレースホルダーを適切に扱うよう注意する必要があります)。S1 の値には、生存性制約がすでに含まれていることに注意してください。これは、それらが RegionInferenceContext::new で追加されているためです。

この処理が完了すると、すべての生存性制約と outlives 制約を考慮した S1 の「最小値」が得られます。しかし、処理を完了するには、メンバー制約も考慮しなければなりません。これについては後のセクションで説明します。