Rust のエイリアシングモデル Stacked Borrows (MIRI の元) を噛み砕いて和訳したもの

この記事は, こちらの論文の内容を大雑把に和訳し解説するものです.

また, 限界開発鯖 Advent Calendar 2023 の空き枠を埋めるものとして急遽執筆しました.

Rust のエイリアシングモデルである Stacked Borrows の構成と, そのランタイムである MIRI についての理解が深まると思います.

スタック原理

Rust のボローチェッカーの功労は皆さんご存知だと思います. プログラムを静的に解析して, コードパスとして参照の作り方が問題ないかを検証しています. では何を検証しているのかと言うと, 次に定義するエイリアシングが起こっていないことを検証しています.

あるメモリを参照する名前があるときに, その領域を変更できる別の名前 (エイリアス) が存在することをエイリアシングという. これを起こしてはいけない.

しかし, これはポインタ型に対して何も検証されません. 当たり前ではありますが, 検証されるのは参照だけです. でもプログラムを順番に実行していけば, ポインタでもエイリアシングしてしまっていることを検知できそうです. そのために, ボローチェッカーが検証していることを整理します.

そのままだと大変なので, まずは簡単な状況として可変なリソースと可変参照しか存在しない言語を考えます. これなら, 以下のルールを検証すれば ok です.

1. ある参照および参照から派生した参照は, そのライフタイム (参照先のリソースが有効である期間) の間でのみ使用できる.
   1. リソースから参照を作成でき, リソースよりも先にその参照が使えなくなります.
   2. 参照から派生した参照を作成でき, 派生元よりも先にその派生した参照が使えなくなります.
2. ある参照が無効化されておらず使用できる間は, 参照を介することでのみ参照先のリソースを変更できる.
   1. すでに使えなくなった参照を使用すると未定義動作です.
   2. 参照を使用するときに, その参照から派生した参照を再帰的に無効化します.

このルールのことを スタック原理 と呼ぶことにします. 試しに, ここで次のプログラムを検査してみましょう.

let mut local = 0;
let mut x = &mut local;
let mut y = &mut *x; // x から派生した参照 y をつくります.
*x = 1; // x を使用して local を変更します. x を使用したので 2-2 より y は無効化されます.
*y = 2; // 無効化された参照 y を使用したので異常終了します.

今回は手動で検査しましたが, これを自動化していきます. そこで local に対する参照のスタックを構築して追いかけることにします. 簡単化と曖昧さ回避のため, この参照のスタックは ボロースタック と呼ぶことにします.

新しく作成した参照は, このボロースタックに積みます. 参照を無効化したら, ボロースタックから取り除きます. こうすれば, ボロースタックに載っていない参照は使用できないことが分かります. そして, 適格なプログラムであれば, プログラムを最後まで実行し終えるとスタックが空になって終了できます.

ボローチェッカーの操作モデル

このアイデアをモデル化します. 先ほどの例では同じメモリを指す 2 つの参照 x, y でしたが, より一般的な話にしていきます.

リソースから作成されたり派生したりした参照を区別するために, すべての参照に ポインタタグ (参照も内部的にはポインタですからね) を付けます. 新しい参照を作る度に, それに新しいポインタタグを割り当てることにします. そして, 参照を作らずにただコピーするだけなら, このポインタタグはそのままです. もちろん, 参照先のリソースを表すメモリ上の位置も格納します.

形式的には, これはメモリ上の位置 $l \in \text{Loc}$ とポインタタグ $t \in \mathbb N$ からなるポインタ値 $\text{Pointer}(l, t)$ として表されます. 実行するときは, 参照と生ポインタは同じものとして扱います.

さらに, それぞれの位置 $l \in \text{Loc}$ に対してそのリソースのボロースタックを格納します. 今後の議論でこのボロースタックに積むモノを拡張していくために, ボロースタックの要素のことを $\text{Item}$ と表します. この $\text{Item}$ には今のところ, $\text{Unique}(t)$ のみが該当します. これは, ポインタタグ $t \in \mathbb N$ に対応する参照たちが有効であることを示します.

メモリ上に実際に配置できるスカラー値は, 今のところポインタと整数だけにしておきます. メモリ上の位置には, それらのスカラーとボロースタックが常に対応することになります.

以上の性質を形式的に定義すると以下のようになります.

$$
\begin{align*}
t \in \text{Tag} & := \mathbb N \\
\text{Scalar} & := \text{Pointer}(l, t) \pod{l \in \text{Loc}, t \in \text{Tag}} \mid z \pod{z \in \mathbb Z} \\
\text{Item} & := \text{Unique}(t) \pod{t \in \text{Tag}} \\
\text{Mem} & := \text{Loc} \xrightarrow{\text{fin}} \text{Scalar} \times \text{Stack} \\
\text{Stack} & := \text{List}(\text{Item})
\end{align*}
$$

そしてタグとボロースタックについて, 操作セマンティクスを次のように定義します.

ルール (new-mutable-ref): 既存のポインタ値 $\text{Pointer}(l, t)$ (参照先) から (&mut expr によって) 新しいミュータブル参照を作成するときは常に, まずそのポインタ値を使用 (これは以下の use-1 を参照) しているとみなす. そして, 新しいタグ $t^\prime$ を選ぶ. 新しい参照は値 $\text{Pointer}(l, t^\prime)$ を取得し, $\text{Unique}(t^\prime)$ を $l$ にあるボロースタックにプッシュする.

ルール (use-1): ポインタ値 $\text{Pointer}(l, t)$ が使用されるときは, タグ $t$ を持つアイテムが $l$ のスタックになければならない. その上に他のタグがある場合はそれらをポップして, タグ $t$ を持つアイテムがそのスタックの一番上に来るようにする. もし $\text{Unique}(t)$ がスタックのどこにもない場合, このプログラムは未定義動作となる.

これらのルールはスタック原理を反映したものです. 先ほどのプログラムを, 今度はこれらのルールにしたがって数学的に処理してみます.

let mut local = 42; // 位置 l に格納, このタグは 0 とする
// 初期スタック: [Unique(0)]
let mut x = &mut local; // = Pointer(l, 1)
// local (0) を使用, スタックに x (1) のタグをプッシュ:
// [Unique(0), Unique(1)]. (new-mutable-ref)
let mut y = &mut *x; // = Pointer(l, 2)
// x (1) を使用, スタックに y (2) のタグをプッシュ:
// [Unique(0), Unique(1), Unique(2)]. (new-mutable-ref)
*x = 1;
// x (1) のタグを上に持ってくるために y (2) を除去.
// [Unique(0), Unique(1)]. (use-1)
*y = 2;
// y (2) がスタックに無いので未定義動作.

生ポインタへの対処

さて, Rust では expr as *mut T のようにすることで生ポインタを取得できるので, これにも対応していきます. 生ポインタどうしを区別することはできないので, タグなしを表すボトム記号 $\bot$ をタグの集合に添加することで対応します.

またボロースタックも, 生ポインタのようなのを追跡できる必要があります. そこで, $\text{Item}$ に $\text{SharedRW}$ を追加します. これは, 特定できない何らかの手段で読み書きできることを表すものです.

これらの事実を, 定義を次のように反映させます.

$$
\begin{align*}
t \in \text{Tag} & := \mathbb N \cup \{ \bot \} \\
\text{Item} & := \text{Unique}(t) \mid \text{SharedRW}
\end{align*}
$$

そして, これらに対応したつぎの操作セマンティクスも定義します.

ルール (new-mutable-raw-1): 可変参照からキャストによって生ポインタをいつでも作成できる. これはまず可変参照の値 $\text{Pointer}(l, t)$ を使用する (以下の use-2 を参照) ものと見なされて, それから新しい生ポインタ $\text{Pointer}(l, \bot)$ を得て $l$ のボロースタックに $\text{SharedRW}$ が積まれる.

ルール (use-2): ポインタの値 $\text{Pointer}(l, t)$ を使用するとき, $t$ が $\bot$ ならば $l$ のスタック内に $\text{SharedRW}$ が必要で, $\bot$ でないならば $\text{Unique}(t)$ が必要である. そのアイテムの上に他のアイテムがあるならば, それらを取り除く. そのアイテムがスタックのどこにも無い場合, スタック原理の違反を検知したことになる.

この use-2 は use-1 の上位互換です. これまでのタグ付きのポインタ値に対しても同じように動作します.

このルールを武器にして, 今度は次のプログラムを解析してみます.

fn main() {
    let mut local = 5; // 位置 l に格納, タグは 0
    // 初期スタック: [Unique(0)]
    let raw_pointer = &mut local as *mut i32; // = Pointer(l, ⊥)
    // 一時的な参照をスタックにプッシュ: [Unique(0), Unique(1)]
    // 生ポインタスタックにプッシュ: [Unique(0), Unique(1), SharedRW]
    let result = unsafe {
        example(
            &mut *raw_pointer, // = Pointer(l, 2)
            // 一時的な参照をスタックにプッシュ:
            // [Unique(0), Unique(1), SharedRW, Unique(2)]

            // ここでポインタを使うのでスタックから取り除く:
            // [Unique(0), Unique(1), SharedRW]
            &mut *raw_pointer, // = Pointer(l, 3)
            // 一時的な参照をスタックにプッシュ:
            // [Unique(0), Unique(1), SharedRW, Unique(3)]
        )
        // このまま example1 にジャンプ
    };
    println!("{result}");
}

fn example1(x: &mut i32, y: &mut i32) -> i32 {
    // x = Pointer(l, 2), y = Pointer(l, 3)
    // l のスタックは [Unique(0), Unique(1), SharedRW, Unique(3)]

    // x のタグに対応する Unique(2) がスタックに無いので, 未定義動作.
    *x = 42;
    *y = 13;
    *x
}

ここで大事なのは, このポインタ (参照や生ポインタ) の派生関係は木構造よりももっと単純になることです. 通常の GC ありの言語であれば, 参照の木構造を保持してそれを GC のクリーンアップに利用したりします. しかし, この手法ではスタックを用いて追跡するので, 常に派生元と派生先が 1 対 1 になります.

再タグ付けと, 可変参照の最適化のための証明のスケッチ

先ほどの example1 は, 2 つの引数のタグが異なっていたので簡単でした. しかし, もしこのタグ同じものを渡されたとしたら, これらを区別できず, 解析が困難になります. 同じタグを持つポインタは, unsafe な関数を使えば (transmute_copy などで) 作成可能です.

この問題は,引数のポインタのタグが呼び出し元によって与えられるために発生します. とはいえ, いくらタグを複製できるといっても, タグを好きなように偽造することはできません (この言語にそのような操作は存在しません). そこで, 同じタグであっても, それぞれが一意なタグになるようにタグを付け直してやればよいのです.

タグを付け直す命令として retag を追加します. これは, 参照に対して一意な新しいタグを与えるためのものです. これはコンパイラによって自動的に挿入され, 参照型である全ての引数は関数の実行開始時にこれを用いて再タグ付けされるものとします.

fn example1(x: &mut i32, y: &mut i32) -> i32 {
    retag x; // x = &mut *x; と等価
    retag y; // y = &mut *y; と等価
    *x = 42;
    *y = 13;
    *x
}

これで, 参照型の引数のタグが同じかもしれない問題は解消されます. &mut &mut i32 の参照外しで得られた参照や, 関数の戻り値として得られた参照も, それが出現する直後に retag すればよいことになります. 以降, 参照型のタグはそれぞれ相異なるとして議論を進めることにします.

さて, 最後の行の最適化――*x をリテラル 42 に置き換えてしまう行い――ができるどうか推論してみます. 最適化を行うので, 未定義動作は起こらないという前提で考えますと,

1. retag x; で $x = \text{Pointer}(l, t)$ になったとします. 他にこのタグ $t$ を持つポインタは存在しません.
2. このタグのアイテム $\text{Unique}(t)$ が $l$ のボロースタックのトップに位置するようにスタックから 0 個以上アイテムを取り除きます.
3. retag y; でまた $l$ のボロースタックからいくつか取り除かれるかもしれません. しかし, 次の行の *x = 42; が動作するにはボロースタックにアイテム $\text{Unique}(t)$ も残っていなければなりません. 未定義動作は起こらないとしたので, ここで $l$ のボロースタックからアイテムが取り除かれることはありません. したがって, *x = 42; を評価できて位置 $l$ に値 42 が格納されます.
4. *y = 13; も同様に, この操作は x に無関係と推論されます. 戻り値である *x は先ほど格納された 42 のままなので, この値を即値にする最適化は実行できると分かります.

ここで注目してほしいのは, "x と y がエイリアシングしない" という条件を明示していないにもかかわらず同等の性質が推論されていることです! この議論により, このような最適化パターン全体は "y のアクセスを x に言及しない 任意 のコードへ置き換える" パターンとして一般化できます.

fn example1(x: &mut i32, /* ほかの引数 */) -> i32 {
    retag x;
    // x を使わない任意のコード
    *x = 42;
    // x を使わない任意のコード
    *x
}

このパターンは x が "一意なポインタ" であることを示しています. なぜなら x を使わないコードは x が指すメモリ領域に影響しないからです.

特に, x を使わないコードが 未知の関数 の呼び出しである場合もこの最適化は適用できます. つまり, Stacked Borrows は典型的な C/C++ コンパイラでは考えられないようなことができます. 環境から渡された参照 x があって (すなわちポインタの値は環境が知っているという意味で エスケープ されていて) 外部関数 f(x) を呼び出すとき, f の引数に x を渡さない限りは f が x から読み書きしないと仮定できます. それだけでなく, この仮定はインライン化などを行わずとも, エイリアシング解析の 王道の 手続き的推論だけで支持できます.

共有参照

ここまででは, 可変参照と生ポインタのみを考えていました. ここからはさらに, 共有参照も考えたいと思います. これを考えることで, 共有参照が読み取り専用であることを強制する方法や, メモリアクセスの順序を変更するようなプログラムの変形を正当化することにも役立ちます.

可変参照と同じ様に, 共有参照についてもスタック原理を考えられます. 参照のすべての使用 (およびその派生参照の作成) は, 参照が作られてからその次の書き換えまでの間に行わなければなりません. また, この共有参照は書き換えには利用できません. この作用について, 整数への共有参照を含んだ次の例を考えてみましょう.

let mut local = 42;
let x = &mut local;
let shared1 = &*x; // 2 つの共有参照を,
let shared2 = &*x; // 同じ可変参照 x から派生する.
let val = *x; // 3 つの参照すべてを,
let val = *shared1; // 交代交代に,
let val = *shared2; // 読み取りアクセスする.
*x += 17; // 再び x を使って, 書き込みアクセスする.
let val = *shared1; // x が変更されてから shared1 を使用したので未定義動作.

これを Stacked Borrows でモデル化するために, また新しい $\text{Item}$ を導入します.

$$
\text{Item} := \text{Unique}(t) \mid \text{SharedRO}(t) \mid \text{SharedRW}(t)
$$

$\text{SharedRO}(t)$ (共有読み取り専用, shared read only の略) は, $t$ タグの参照は, このスタックに関連付けられた位置から読み取りのみができることを示します. さらにここで, $\text{SharedRW}$ にもタグを付けられるようにしておきます. これで "$\text{Item}$ のタグ $t$" というものが必ず存在するようになりました.

今回の Stacked Borrows のルールは以下のようになります.

ルール (new-shared-ref-1): 新しい共有参照は &expr によってあるポインタの値 $\text{Pointer}(l, t)$ から作られる. これはまずそのポインタの値への 読み取りアクセス (下記のルール read-1 を参照) と見なされる. そして新しいタグ $t^\prime$ を選び, 共有参照の値として $\text{Pointer}(l, t^\prime)$ を用いる. 最後に $l$ のスタックに $\text{SharedRO}(t^\prime)$ を積む.

ルール (read-1): ポインタが $\text{Pointer}(l, t)$ という値でここから読み取るとき, タグが $t$ の $\text{Item}$ (すなわち $\text{Unique}(t), \text{SharedRO}(t), \text{SharedRW}(t)$ のいずれか) が $l$ のスタックに存在しなければならない. 読み取る際には, タグが $t$ である $\text{Item}$ の上にある $\text{Item}$ すべてが $\text{SharedRO}(\_)$ になるまで, スタックからアイテムを取り除く. タグが $t$ のアイテムが存在しない場合は未定義動作になる. (このルールは use-2 よりも優先される.)

つまり, $\text{SharedRO}(t)$ がスタックにあっても, タグが $t$ の参照は読み取りに使用することしかできません. 書き込むには $\text{Unique}(t)$ や $\text{SharedRW}(t)$ が必要となります.

read-1 の重要な点 (use-2 との重要な違い) は, $\text{Pointer}(l, t)$ を使った読み取りでタグが $t$ の $\text{Item}$ が一番上に来ないこともあります. これは, 2 つの共有参照が互いに邪魔すること無く読み取りに使用できるという事実を反映したものです. 対照的に, 書き込みアクセス (これは use-2 のルールが扱うもの) では, アクセスに使うポインタのタグを持つ $\text{Item}$ がスタックのトップに必要です.

ここから言えることは, このシステムが維持している重要な普遍性として, スタックに $\text{SharedRO}$ が存在する場合, それらはすべてスタックの先頭で隣り合います. 他の種類のアイテムをプッシュするような操作 (可変参照や生ポインタの作成) はすべて書き込みアクセスなので, その際に必要な $\text{Unique}$ や $\text{SharedRW}$ の上にある $\text{SharedRO}$ は消し飛ばされます. そのため, $\text{Unique}$ や $\text{SharedRW}$ が $\text{SharedRO}$ の上に置かれることは決してありません.

このルールをもって, 先ほどのサンプルは以下のように実行されます.

let mut local = 42; // 位置 l に格納し, タグは 0
let x = &mut local; // = Pointer(l, 1)
// x のタグをスタックにプッシュ: [Unique(0), Unique(1)]. (new-mutable-ref)
let shared1 = &*x; // = Pointer(l, 2)
let shared2 = &*x; // = Pointer(l, 3)
// 新しいタグをプッシュ: [Unique(0), Unique(1), SharedRO(2), SharedRO(3)]. (new-shared-ref-1)
let val = *x;
// x (1) より上のアイテムが全て SharedRO なので ok. (read-1)
let val = *shared1;
// shared1 (2) より上のアイテムが全て SharedRO なので ok. (read-1)
let val = *shared2;
// shared2 (3) はそのまま読み取れるので ok. (read-1)
*x += 17;
// トップが Unique(1) になるまで取り除く: [Unique(0), Unique(1)]. (use-2)
let val = *shared1;
// 未定義動作. shared1 のタグ 2 がスタックに載っていない. (read-1)

読み取り専用の共有参照を exploit する最適化のスケッチ

もう 1 つ最適化できそうなケースとして, 共有参照が読み取り専用であることを利用した最適化が有効な, 次のような関数を考えてみます.

fn example2(x: &i32, f: impl FnOne(&i32)) -> i32 {
    retag x;
    let val = *x / 3;
    f(x);
    // これを val を返すように最適化してほしい
    *x / 3
}

今回は, x を最初に読み取る処理と最適化対象の間に任意のコードが入る可能性をクロージャ f で表している. しかし, これは読み取り専用の参照で渡しているので f を実行しても x に影響しないはずですよね……?

さて, ここで (奇妙ではありますが) 意味論的には最適化してしまうとまずい反例を用意できます. 例えば, 共有参照のポインタから可変な生ポインタを作ってしまいます.

fn main() {
    let mut local = 6;
    let x = &local;
    let result = example2(x, |inner_x: &i32| {
        retag inner_x;
        let raw_pointer: *mut i32 = inner_x as *const i32 as *mut i32;
        unsafe { *raw_pointer = 15; }
    });
    println!("{result}");
}

しかし, Stacked Borrows の下ではこのプログラムが未定義動作となることを検知できてほしいです. では, 実際にどのような動きになるのか見てみましょう.

fn main() {
    let mut local = 6; // 位置 l に格納, タグは 0
    let x = &local; // = Pointer(l, 1)
    // スタックは [Unique(0), SharedRO(1)]
    // example 2 にジャンプ
    let result = example2(x, |inner_x: &i32| {
        // スタックは [Unique(0), SharedRO(1), SharedRO(2)]
        retag inner_x; // = Pointer(l, 3)
        // 共有参照をスタックにプッシュ: [Unique(0), SharedRO(1), SharedRO(2), SharedRO(3)]
        let raw_pointer: *mut i32 = inner_x as *const i32 as *mut i32;
        // = Pointer(l, 3)
        unsafe { *raw_pointer = 15; }
        // タグが 3 の書き込み可能なアイテムがスタックにないので, 未定義動作. (use-2)
    });
    println!("{result}");
}

fn example2(x: &i32, f: impl FnOne(&i32)) -> i32 {
    // スタックは [Unique(0), SharedRO(1)]
    retag x; // x = Pointer(l, 2)
    // 共有参照をスタックにプッシュ: [Unique(0), SharedRO(1), SharedRO(2)]
    let val = *x / 3;
    // SharedRO(2) がスタックにあるのでそのまま読み取り. (read-1)
    // クロージャにジャンプ
    f(x);
    *x / 3
}

どうやら問題なさそうですね. ここで共有参照の場合も, 可変参照と同じように Stacked Borrows のルールから参照先が変更されない性質を導出できます. これにより, *x / 3 の代わりに val を返すような最適化が可能です.

より発展的な変形

ここまでで, unsafe なコードであっても, Stacked Borrows に準拠していて未定義動作は無視できるという仮定を利用した最適化を 2 つ見てきました. いずれも似たようなパターンであり,

1. ある参照を再タグ付けする.
2. 何らかの変更や観測 (可変参照への書き込みや共有参照からの読み取り) を行って未知のコードを実行する.
3. 元の参照を再使用する.

となっています. 再タグ付けによってその参照がスタックのトップに位置し, 最後の再使用によってその参照がスタックに残っていることが証明されます. この方法は未知のコードにおける命令の並べ替えにも有効です, 実際にこれまで検討した変換は, いずれもこのような並びに帰着できます. 例えば example1 では, 以下のような変換を基本的に行っていました (未知のコードは関数 g と f として抽象化してあります).

retag x;
g();
*x = 42;
f();
let x_val = *x;
return x_val;

↓

retag x;
g();
*x = 42;
let x_val = *x;
f();
return x_val;

これは, f() とその下の行を入れ替えただけです. しかしこれで *x = 42; と let x_val = *x; が隣り合ったので単純な最適化が可能となり, x_val には 42 が入ることが自明になります.

同様に, example2 では読み取り *x の行を, f(x) を越えて上に動かせばよいです. こうすれば, 2 つの読み取りが隣り合っているので, 重複を除去する正当化が簡単になります. example1 との違いは, これが共有参照の読み取りであることと, 未知のコード f が x にアクセスできることです.

しかし, 条件が揃えば未知のコードを越えて処理の順番を交換を移動できるというのは興味深いです. これは普通, 参照の有効期間を広げてしまうので難しくなります. 例えば, 以下の関数を考えてみましょう.

fn example2_down(x: &i32, f: impl FnOnce(&i32)) -> i32 {
    retag x;
    let val = *x;
    f(x);
    val // *x を代わりに返してもよいはずです.
}

この let val = *x; の読み取りを, f を越えて下に移動させたいです. そうすればレジスタの圧迫が防げます. というのも, f の呼び出しの前後で val を覚え続けなくてよくなるからです.

可変参照でも同様に, 参照が不要なコードを越えて読み取りを下に移動させることができます. ところが, 書き込みについては以下のような面白いケースもあります.

fn example3_down(x: &mut i32, f: impl FnOnce()) {
    retag x;
    *x = 42; // この書き込みは冗長で, 最適化で取り除けるはず.
    f();
    *x = 13;
}

ここで冗長な書き込みを取り除くには, x への書き込みを下へ移動させればよいです. すると, 同じ参照に対する書き込みが連続しますので, 最初の書き込みは除去できます. しかしここまでの論法では, f の実行後に x の参照先のリソースが変化する可能性を否定できません. このような最適化が妥当になる理由は後述します.

プロテクター

これまで紹介してきた Stacked Borrows では, まだあらゆる演算を下に移動させる最適化ができません. 以下に example2_down での反例を示します.

fn main() {
    let mut local = 42; // 位置 l に格納, タグは 0
    let raw_pointer = &mut local as *mut i32;
    let val = example2_down(
        unsafe { &*raw_pointer }, // = Pointer(l, 2)
        |x_inner| {
            retag x_inner;
            unsafe { *raw_pointer = 17; }
        },
    );
    println!("{val}");
}

fn example2_down(x: &i32, f: impl FnOnce(&i32)) -> i32 {
    retag x;
    let val = *x;
    f(x);
    val // *x を代わりに返してもよいはずです.
}

f として渡すクロージャでは, x として共有している raw_pointer へ書き込むことで x の格納値を変更する. クロージャでの書き込みの直前, $l$ のボロースタックは

$$
[\text{Unique}(0), \text{Unique}(1), \text{SharedRW}(\bot), \text{SharedRO}(2), \text{SharedRO}(3)]
$$

のようになっています. この状況ではスタックに $\text{SharedRW}(\bot)$ が存在するので生ポインタでの書き込みができます. 書き込み後はスタックからいくつか取り除かれて

$$
[\text{Unique}(0), \text{Unique}(1), \text{SharedRW}(\bot)]
$$

となります. しかし example2_down の中で x (タグ 3) が使用されることはないので, 問題なく動作できます. ところは先ほどのような可変参照に対する最適化を許容してしまうと, このプログラムは動作しなくなってしまいます.

この点において, rustc のボローチェッカーを再現できているとはいえません. Rust では, 引数の参照のライフタイムは関数のスコープ全体の有効期間と同等かそれ以上でなければないルール (outlive ルール) が存在します. Stacked Borrows でもこれを再現するために, プロテクター を導入します.

形式的には, ボロースタックのアイテムに任意の 呼び出し ID を付与する拡張を施します.

$$
\begin{align*}
\text{CallId} & := \mathbb N \\
c \in \text{CallId}^? & := \text{CallId} \cup \{ \bot \} \\
\text{Item} & := \text{Unique}(t, c) \mid \text{SharedRO}(t, c) \mid \text{SharedRW}(t, c)
\end{align*}
$$

すべての呼び出し ID は関数呼び出し (スタックフレーム相当のもの) を表します. また, これらのセマンティクスは, まだ戻っていない関数呼び出しに対応する呼び出し ID の集合を追跡するものとします. $\text{Unique}(t)$ は $\text{Unique}(t, \bot)$ の略記として使用し, 他の $\text{Item}$ についても同様の略記をします.

では, 新しくスタックに積まれた $\text{Item}$ がプロテクターを取得するのはどのようなときでしょうか? ここまでで, 参照が引数として渡されたり, ポインタを介して読み取ったり, 別の関数から返されたりするたびに, retag を行っていました. これと同じように, 引数の再タグ付けをする際に, 現在の関数呼び出しの呼び出し ID を付加して保護するようにします. こうすることで, 関数の実行中にその ID が付いている $\text{Item}$ を取り除かせないようにします. 構文的には, retag[fn] x と書くことで, x が関数の始まりで再タグ付けされ, そのアイテムが保護されることを示すことにします.

以下に, プロテクターの新しいルールを示します.

ルール (retag-fn): retag[fn] の一部として (new-mutable-ref や new-shared-ref-1 で) 新しいアイテムをある位置のボロースタックにプッシュするとき, その $\text{Item}$ のプロテクターとして現在の関数呼び出しの呼び出し ID をセットする.

ルール (protector): アイテムが (use-2 や read-1 によって) 取り除かれるたびに, プロテクター $(c, \bot)$ を持つアイテムが存在するかどうかチェックする. もし存在していてその呼び出し ID が実行中の (まだ戻っていない) 関数呼び出しに対応するならば, そのプロテクターはアクティブであると呼ぶ. アクティブなプロテクターの除去は未定義動作となる.

example2_down のコードを少し書き換えて, x の再タグ付けに先ほどのルールを適用できるようにしてみました.

fn example2_down(x: &i32, f: impl FnOnce(&i32)) -> i32 {
    retag[fn] x;
    let val = *x;
    f(x);
    val // *x を代わりに返してもよいはずだ.
}

さて, このルールに則って先ほどの反例を考えてみると, クロージャの実行開始時点での $l$ のボロースタックは以下のようになります.

$$
[\text{Unique}(0), \text{Unique}(1), \text{SharedRW}(\bot), \text{SharedRO}(2), \text{SharedRO}(3, c)]
$$

ここで, $c$ とは example2_down の呼び出し ID です. この場合に書き込みをしようとすると, プロテクターのルールによって阻害されます. 生ポインタで書き込むには $\text{SharedRW}(\bot)$ より上にあるアイテムを取り除かなければなりませんが, このルールにより未定義動作となることがわかります.

可変参照への書き込みの最適化の証明のスケッチ

さて, プロテクターを用いることで先の反例に対処できました. 実際に, プロテクターは以下のようにして変形の検証ができるようになります.

1. retag[fn] で x は $\text{Pointer}(l, t)$ の値を持つとします. 位置 $l$ のボロースタックのトップの $\text{Item}$ は $\text{SharedRO}(t, c)$ です. ここで, $c$ は example2_down の呼び出し ID です. $l$ に格納されているスカラー値を $s$ として記憶しておきます.
2. f の実行中に $l$ への書き込みアクセスがあれば, スタックから全ての $\text{SharedRO}$ が取り除かれてしまいます. さらに $\text{SharedRO}(t, c)$ の $c$ はアクティブなプロテクターなのでこれを取り除くことができません. したがって, 位置 $l$ に対する書き込みは発生しないと考えてよいです.
3. 結果として, f から処理が戻ったとき, $l$ には $s$ がまだ格納されています. これにより先の変形が正当化されます.

内部可変性のサポート

Stacked Borrows は, 未知のコードに対して共有参照や可変参照の使用を上下に移動させるような変形をサポートしていることを見てきました. これにより, コンパイラはエイリアシング解析で参照型を利用するために必要な自由度が得られます. しかし, まだこれだけではルールにそぐわない Rust の実態が存在します.

例えば, Rust には Cell という Copy な型の値を格納できるコンテナ型が用意されています. これはスレッド安全でなくなる代わりに, その共有参照でも内部の値を変更できます.

fn cells(x: &Cell<i32>, y: &Cell<i32>) -> i32 {
    x.set(13):
    y.set(42);
    x.get() // x と y が同じかそうでないかで, 13 を返すか 42 を返すかが変化する.
}

&Cell<i32> は本質的に C の int* が安全になったものです. これはいつでも参照先のリソースを読み書きできます. Cell のような型でのアクセスは Rust の安全性のルールが壊されるように見えるかもしれませんが, Cell はそれを防ぐようになっています. 内部的には, UnsafeCell というコンパイラに特別扱いされる型を使用して, それに安全装置を付けています. Cell ではそのデータのコピーによる書き込みと読み取りしかできず, 中の値の参照を直接取得できません. これにより可変なデータの共有に関する問題が解消され, &Cell<i32> のライフタイムのみを気にすればよくなっています.

Stacked Borrows ではこの情報を利用し, UnsafeCell の内部メモリを共有参照の読み出しに関する制限から除外します. UnsafeCell の内部の値の追跡については, 既に導入した $\text{SharedRW}$ を用います. これは生ポインタなどと同じ挙動なので妥当です.

一般には, 共有参照が 部分的な 内部可変性を持ちうるという点が問題を複雑にします. これまで, 参照は 1 つの場所を指して 1 つのスタックにのみ影響するものでした. しかし, &(i32, Cell<i32>) のような型では内部可変性のある (UnsafeCell を使用している) 部分とそうでない部分が混在しています. この場合, 1 つ目の要素へのアクセスでは共有参照のルールを適用し, 2 つ目の要素へのアクセスでは可変参照のルールを適用する, という出し分けの必要があります.

したがって, 部分的な内部可変性を持つ共有参照を作成する場合, 参照が被覆するあらゆる位置に対して同じように変形できるとは限りません. まず, 新しいタグ $t$ を選び, その参照が指すメモリ領域内の UnsafeCell を参照が被覆するメモリの型に基づいて探す必要があります. UnsafeCell の外にあるすべての位置については, これまでと同様に処理を進めて, read-1 によって新しい読み取り専用を表す $\text{SharedRO}(t, c)$ をスタックに乗せます (共有参照の作成は読み取りアクセスでした). UnsafeCell 内の位置については, 代わりに読み書きを表す $\text{SharedRW}(t, c)$ をスタックに積むことで, 可変生ポインタと同じものを提供します.

参照の作成がいつもアクセスだけになるとは限りません. これまでと違うのは, UnsafeCell の共有参照の作成は読み取りアクセス扱いではなく, 新しい $\text{Item}$ をスタックのトップに追加しません. 代わりに, 内部可変性のポインタ $\text{Pointer}(l, t)$ から新しい共有参照を作るときは, その $\text{Item}$ のすぐ上に $\text{SharedRW}$ を追加するだけで, $\text{Item}$ を取り除きません.

ルール (new-shared-ref-2): ある既存のポインタ値 $\text{Pointer}(l, t)$ から新しい共有参照を作成するとき, ある新しいタグ $t^\prime$ を選び, 共有参照の値として $\text{Pointer}(l, t^\prime)$ を作る. この参照が被覆する位置のうち, UnsafeCell 内部のすべての位置についてボロースタックにあるタグが $t$ のアイテムを探し, それぞれのすぐ上に $\text{SharedRW}(t^\prime)$ を追加する. そのようなアイテムが 1 つも見つからない場合は未定義動作となる. 残りの UnsafeCell 内部でない位置については, タグ $t$ のアイテムに対する読み取りアクセスを行い, $\text{SharedRO}(t^\prime)$ をスタックのトップにプッシュする.

内部可変性を持つ共有参照と可変生ポインタのルールを一貫させる (結局どちらも $\text{SharedRW}$ を使っている) ために, 後者はアクセス扱いとならないように調整します.

ルール (new-mutable-raw-2): ある可変参照 (&mut T) からキャスト (expr as *mut T) によって可変生ポインタの値 $\text{Pointer}(l, t)$ を作成するときは, ボロースタックでタグが $t$ のアイテムを探し, それぞれのアイテムのすぐ上に $\text{SharedRW}(\bot)$ を追加する. (そのようなアイテムが 1 つも見つからない場合は未定義動作です.) そして, ポインタの値は $\text{Pointer}(l, \bot)$ となる.

このルールでは, 例えば同じ可変参照から内部可変性を持つ共有参照を大量に作成すると, スタック内で多くの $\text{SharedRW}$ が隣り合うことになります. スタック上の隣接する $\text{SharedRO}$ を, スタックからお互いを取り除くことなく使用できる グループ と考えると少し扱いやすいです. そして, 隣接する $\text{SharedRW}$ のグループが使用されてもそのグループ内のアイテムは取り除かれることなく残り続けるように, アクセスのルールも調整する必要がある.

これを書き下すと, 以下のようになります (ついでにプロテクターとも連携します).

ルール (write-1): ポインタ値 $\text{Pointer}(\_ , t)$ を使用した任意の書き込みアクセスにおいて, アクセスによって影響を受けるそれぞれの位置 $l$ に対して次を行う. トップのアイテムが $\text{Unique}(t, \_ )$ である または トップのアイテムが含まれるグループに $\text{SharedRW}(t, \_ )$ が存在するようになるまで, スタックからアイテムを取り除く (これによって, $\text{SharedRW}(t, \_ )$ がスタック内にあれば, その上には同じグループの $\text{SharedRW}$ が乗ることしかありえません). スタックから全てのアイテムを取り除いてしまったか, アクティブなプロテクターを持つアイテムを取り除いてしまった場合は, 未定義動作となる.

読み取りアクセスであっても, タグ付きの $\text{SharedRW}$ アイテムがあることを考慮する必要があります. しかし, $\text{SharedRW}$ のグループに隣接する他のグループの $\text{SharedRW}$ や $\text{SharedRO}$ を無効化せずに読み取りしたいです (これは write-1 の書き込みのルールと似ています).

しかし, アクセスを正当化してくれるアイテムの上に $\text{Unique}$ アイテムが残っていないことを確認する必要があります. これを実現するテクニックとして, スタックからアイテムを取り除くのではなく, そのままにして $\text{Unique}$ に対して “無効化” の印を付けることにします. こうすれば, スタック上でそのアクセスしたい位置に関するアイテムの上にある $\text{SharedRW}$ アイテムの有効性を維持できます.

つまるところ, 新しい $\text{Item}$ として以下を導入します.

$$
\text{Item} := \text{Unique}(t, c) \mid \text{SharedRO}(t, c) \mid \text{SharedRW}(t, c) \mid \text{Disabled}
$$

そして読み取りのルールを以下のように変更します.

ルール (read-2): ポインタ値 $\text{Pointer}(\_ , t)$ を用いた読み取りアクセスにおいて, そのアクセスが影響するそれぞれの位置 $l$ について次のことを行う. スタックのタグ $t$ を持つ最もトップに近いアイテムを探し, それより上にある $\text{Unique}(\_ , \_ )$ をすべて $\text{Disabled}$ に置き換える. もしその中にアクティブなプロテクターを持つ $\text{Unique}$ があれば, そのプログラムは未定義動作となる.

read-2 にこのようなひねりを加えているのは, 実際の Rust で試していると以下のようなパターンによく遭遇したからです. $\text{Disabled}$ がなければ, このパターンは未定義動作になってしまいます.

fn make_raw(y: &mut i32) -> *mut i32 {
    // y = Pointer(l, t2)
    retag[fn] y; // = Pointer(l, t3)
     // スタック: [..., Unique(t1), Unique(t2), Unique(t3)]
    y as *mut i32 // さらにスタックに SharedRW(⊥) をプッシュ
}

fn bad_pattern(x: &mut i32) {
    retag[fn] x; // = Pointer(l, t1)
    let raw_ptr = make_raw(x); // ラベル t2 の一時的な参照が作られます.
    // スタック: [..., Unique(t1), Unique(t2), Unique(t3), SharedRW(⊥)]
    let val1 = *x;
    // スタック: [..., Unique(t1)]
    // スタックに SharedRW(⊥) が無いので未定義動作, とはなってほしくないです. 問題ないはずなので.
    let vale2 = unsafe { *raw_ptr };
}

これで最終調整は完了しました. ここで, この理論全体を俯瞰して形式的に整理するとしましょう.

形式的定義

高水準な構造

高水準な構造としては, Stacked Borrows はラベル付きの遷移システムとして定義されます. ラベルはイベント (ここで最重要なのは読み書きのアクセスと再タグ付け) として, 状態は以下のレコードによって表されます.

$$
\begin{align*}
\sigma \in \text{SState} & := \begin{cases}
\text{stacks} & : \text{Stacks}, \\
\text{calls} & : \text{List}(\text{CallId}), \\
\text{nextptr} & : \text{PtrId}, \\
\text{nextcall} & : \text{CallId}, \\
\end{cases} \\
\xi \in \text{Stacks} & := \text{Loc} \xrightarrow{\text{fin}} \text{Stack}
\end{align*}
$$

また, 残りの関連する定義については以下のようになります.

残りの定義

ドメイン:

$$
\begin{align*}
\text{PtrId} & := \mathbb N \\
t \in \text{Tag} & := \text{PtrId}^? \\
c \in \text{CallId} & := \mathbb N \\
\iota \in \text{Item} & := \text{Permission} \times \text{Tag} \times \text{CallId}^? \\
p \in \text{Permission} & := \text{Unique} \mid \text{SharedRW} \mid \text{SharedRO} \mid \text{Disabled} \\
S \in \text{Stack} & := \text{List}(\text{Item})
\end{align*}
$$

イベント:

$$
\begin{align*}
\text{AccessType} & := \text{AccessRead} \mid \text{AccessWrite} \\
\text{RetagKind} & := \text{Default} \mid \text{Raw} \mid \text{FnEntry} \\
\epsilon \in Event & := \begin{cases}
\text{EAccess}(a, \text{Pointer}(l, t), \tau) \pod{a \in AccessType, \iota \in Type} \\
\text{ERetag}(\text{Pointer}(l, t_{old}), t_{new}, \tau, k, k^\prime) \pod{k \in PtrKind, k^\prime \in RetagKind} \\
\text{EAlloc}(\text{Pointer}(l, t), \tau) \\
\text{EDealloc}(\text{Pointer}(l, t), \tau) \\
\text{EInitCall}(c) \\
\text{EEndCall(c)}
\end{cases} \\
m \in \text{Mutability} & := \text{Mutable} \mid \text{Immutable} \\
\text{PtrKind} & := \text{Ref}(m) \mid \text{Raw}(m) \text{Box}
\end{align*}
$$

選択した遷移:

• os-access:
  $$
  \frac{\text{MemAccessed}(\sigma.\text{stacks}, \sigma.\text{calls}, a, \text{Pointer}(l, t), |\tau|) = \xi^\prime \quad \sigma^\prime = \sigma \mathbb{\text{ with }} [\text{stacks} := \xi^\prime]}{\sigma \xrightarrow{\text{EAccess}(a, \text{Pointer}(l, t), \tau)} \sigma^\prime}
  $$
• os-retag:
  $$
  \frac{\text{Retag}(\sigma.\text{stacks}, \sigma.\text{nextptr}, \sigma.\text{calls}, \text{Pointer}(l, t_{old}), \tau, k, k^\prime) = (t_{new}, \xi^\prime, n^\prime) \quad \sigma^\prime = \sigma \mathbb{\text{ with }} [\text{stacks} := \xi^\prime, \text{nextpr} := n^\prime]}{\sigma \xrightarrow{\text{ERetag}(\text{Pointer}(l, t_{old}), t_{new}, \tau, k, k^\prime)} \sigma^\prime}
  $$

ここで, $\text{stacks}$ はそれぞれの位置のスタックを追跡し, $\text{calls}$ はアクティブな呼び出し ID の現在のリスト (プロテクターの実装の必要) を追跡し, $\text{nextptr}$ と $\text{nextcall}$ は新しいポインタ ID とコール ID の生成に利用します.

このアプローチにより, Stacked Borrows を言語の他から切り離せます. この言語の操作セマンティクスは, 単に $\text{SState}$ を含むもので, 関連するイベントが発生するたびにその状態に対して適切に遷移するものです. したがって, 前節と異なりそれぞれの位置のスタックは $\text{SState}$ の $\text{stacks}$ フィールドで追跡します.

また, 想定されるイベントと重要な遷移を定義してあります. これらのイベントには, 全てのメモリアクセス (読み取り, 書き込み, メモリ確保, メモリ解放), 関数呼び出しの開始と終了 (プロテクターを動かす際の呼び出し ID の追跡関係), そしてもちろん再タグ付けがあります. これらのイベントの引数のほとんどは, 外から Stacked Borrows のサブシステムに入る情報そのものであるという点で "入力引数" です. 呼び出しイベントの呼び出し ID $c$ と再タグ付けイベントの新しいタグ $t_{new}$ のみが出力引数であり, Stacked Borrows から外へ返される情報を表しています.

それぞれのイベントが Stacked Borrows の状態 $\sigma$ に及ぼす影響は, 前の状態が与えられたときに次の状態を計算する関数によって記述されます. ここでは, レコードの単一のフィールドを更新する表記として $\sigma \mathbb{\text{ with }} [\text{field} := e]$ を用いています (後述するように, これは有限な部分辞書配列の要素を更新する場合にも使用します). Stacked Borrows の非常にアルゴリズムチックな性質を考慮すると, リレーショナルな方式よりもこのような計算方式のほうが適していそうです.

次に, 非形式的にしか取り上げなかったイベントの形式的な定義を述べます.

メモリアクセス

次の図式では, $\text{EAccess}$ イベントの発生を定義する関数として $\text{MemAccessed}$ を実装することで read-2 と write-1 を形式化します. この関数の定義は単純で, アクセスによって影響を受ける全ての位置を反復処理し, ヘルパー関数 $\text{Access}$ を呼び出して新しいスタックを計算します. 影響を受ける位置の集合を決定するには, アクセスのサイズを知らなければなりません. これは, イベントの一部である型 $\tau$ に基づいて計算されます. $\text{Access}$ は部分関数であり, アクセスが不正であることを表すための戻り値として $\bot$ を用います. この場合, $\mathbb{\text{with}}$ 演算子によって失敗が伝播され, $\text{MemAccessed}$ も $\bot$ を返し, 遷移システムは停止します.

読み取りと書き込みの両方について, $\text{Access}$ は $\text{Grants}$ 関数で定義された "認可アイテム" を見つけることから始まります. $\text{Grants}(p, a)$ は与えられた権限 $p$ のアイテムがメモリアクセスの正当化に使用できるかを決定するもので, $a$ はこれが読み取りか書き込みかを示します. 書き込みの場合は, $\text{Unique}$ と $\text{SharedRW}$ のみが (write-1 のように) 許可され, 読み取りの場合は加えて $\text{SharedRO}$ も許可されます (read-2 のように $\text{Disabled}$ では許可されません). アクセスは, $\text{FindGranting}$ を使用してスタック $S$ を上から下まで検索し, 与えられたタグ $t$ に一致する最上位のアイテムを見つけ, 現在のアクセスを許可します. 暗黙のうちに, 再帰の基本ケースであるリストが空の場合は $\bot$ を返します (パターンのいずれにもマッチしないため). これは, 目的のアクセスを許可するアイテムが存在しない場合にのみ起こります.

/// p がタイプ a のアクセスの正当化に使用できるかを定義する.
fn grants(p: Permission, a: AccessType) -> bool {
    p != Permission::Disabled &&
        (a == AccessType::AccessRead || p != Permission::SharedRO)
}

/// S 内で t へのアクセス a を認可できる一番上のアイテムを探す.
fn find_granting(s: &Stack, a: AccessType, t: Option<Tag>) -> Option<(ItemId, Permission)> {
    let (rest, top) = s.split_last()?;
    if top.tag == grants(top.perm, a) {
        Some((rest, top.perm))
    } else {
        find_granting(rest, a, t)
    }
}

/// i の上にあるアイテムのうち、p で正当化される書き込みと両立しないような一番下のアイテムを求める.
fn find_first_write_incompat(s: &Stack, i: ItemId, p: Permission) -> Option<ItemId> {
    match p {
        // Unique への書き込みはそれより大きい Id のものと両立しない.
        Permission::Unique => Some(i + 1),
        // SharedRW への書き込みは隣接する SharedRW のみと両立する.
        Permission::SharedRW => {
            if i + 1 < s.len() && s[i + 1].perm == p {
                find_first_write_incompat(s, i + 1, p)
            } else {
                Some(i + 1)
            }
        },
        _ => None,
    }
}

/// タグ t に a タイプのアクセスをした後の新しいスタックを計算する.
/// これは c が追跡するアクティブコールに依存する.
fn access(a: AccessType, s: &Stack, t: Option<Tag>, c: &HashSet<CallId>) -> Option<Stack> {
    match a {
        AccessType::AccessRead => {
            let (i, _) = find_granting(s, a, t)?;
            // プロテクターがかかっている場合はエラーになる.
            let protected = S[i + 1..].any(|item| c.contains(item.protector));
            if protected {
                None
            } else {
                // i より上の Unique をすべて Disabled にする.
                let new_stack: Stack = s[i + 1..].iter().cloned().map(|item| {
                    if item.perm == Permission::Unique {
                        Item {
                            perm: Permission::Disabled,
                            ..item
                        }
                    } else {
                        item
                    }
                }).collect();
                Some(new_stack)
            }
        },
        AccessType::AccessWrite => {
            let (i, p) = find_granting(s, a, t)?;
            let j = find_first_write_incompat(s, i, p)?;
            // プロテクターがかかっている場合はエラーになる.
            let protected = S[j..s.len()].any(|item| c.contains(item.protector));
            if protected {
                None
            } else {
                // j 以上の位置のアイテムを取り除く.
                Some(S[..j].to_vec())
            }
        }
        _ => None,
    }
}

/// それぞれの場所の点ごとに, 読み取りと書き込みのアクセスはリフトされる.
fn mem_accessed(
    stacks: &Stacks,
    c: &HashSet<CallId>,
    a: AccessType,
    Pointer(l, t): Pointer,
    n: usize,
) -> Option<HashMap<Loc, Stack>> {
    let mut cloned = stacks.clone();
    for loc in l..l + n {
        cloned[loc] = access(a, &cloned[loc], t, c);
    }
    Some(cloned)
}

続いて再タグ付けのセマンティクスも実装する.

/// 新しいアイテム new_item を挿入した後, 古いタグから派生した新しいスタックを計算する.
/// また, アクティブな呼び出しのリスト c（access で使用) にも依存する.
fn grant_tag(s: &Stack, told: Option<Tag>, new_item: Item, c: &HashSet<CallId>) -> Option<Stack> {
    // この操作に対応する access を決定する.
    let a = if grants(new_item.perm, AccessType::AccessWrite) {
        AccessType::AccessWrite
    } else {
        AccessType::AccessRead
    };
    // 古いタグに一致するアイテムを探す.
    let (i, p) = find_granting(s, a, told)?;
    if new_item.perm == Permission::SharedRW {
        // SharedRW をその認可した位置に挿入する
        let j = find_first_write_incompat(s, i, p)?;
        insert_at(s, new_item, j)
    } else {
        // さもなくば, アクセスを行ってアイテムをトップにする.
        let s = access(a, s, told, c)?;
        insert_at(s, new_item, s.len())
        // ポインタの型 k、ポインタ元の型 τ に対して, Pointer(l, told) が指すメモリを再借用する.
        // τ.prot は, アイテムが保護されるべきかどうかを示す.
    }
}

fn reborrow(
    stacks: &Stacks,
    c: &HashSet<CallId>,
    Pointer(l, t_old): Pointer,
    tau: Type,
    k: PtrKind,
    t_new: Option<Tag>,
    prot: Option<CallId>,
) -> Option<Stacks> {
    let mut cloned = stacks.clone();
    // それぞれの位置について, 新しい認可を決定し対応するアイテムを追加する.
    for (loc, fr) in frozen_iter(l, tau) {
        let p_new = new_perm(k, fr);
        let new_item = (p_new, t_new, prot);
        stacks[loc] = grant_tag(&stacks[loc], t_old, new_item, c)?;
    }
    Some(cloned)
}

再タグ付け

Stacked Borrows は参照が作成されたり (new-mutable-ref や new-shared-ref-2), 生ポインタにキャストされたり (new-mutable-raw-2) するたびに, いくつかの追加処理を行いました. そして再タグ付けはこれらの操作からなる糖衣構文でした. しかし実際の Rust において &mut を生ポインタとして引数に渡すとき, これは再借用をしているのではなく単にタグの付け直しをしていると考えるのが, いくつかの特殊なコードの状況でも自然です. そのため retag[raw] という構文を導入することで, 可変参照から生ポインタへの再タグ付けを表現することにします.

そこで, 再タグ付けを掘り下げます. 中核となるヘルパー関数である reborrow を見てみましょう. 再借用は古いポインタのタグ t_old と位置 l, ポインタが指す型 tau, 新しいポインタのタグ t_new とポインタの種類 k, そして prot (新しいアイテムがプロテクトされる任意の呼び出し ID) を引数として受け取ります. ポインタの種類 k は新しいポインタが参照, 生ポインタ, Box のいずれかであるかを決定するものです.

借用はポインタが被覆するそれぞれの位置 $l^\prime$ について以下のように進行します (この位置のリストは frozen_iter によって計算されます).

1. $l^\prime$ に対して, $t_{new}$ に付与しようとする許可 $p_{new}$ を計算する (new_perm によって計算する).
   • x が可変参照 (&mut T) であれば, $p_{new} := \text{Unique}$.
   • x が可変生ポインタ (*mut T) であれば, $p_{new} := \text{SharedRW}$.
   • x が共有参照 (&T) または不変生ポインタ (*const T) である場合, $l^\prime$ の存在を確認する. frozen (確実に UnsafeCell の外にある) かどうかを, 型 tau に基づいて frozen_iter で決定する. frozen な位置であれば $p_{new} := \text{SharedRO}$ を, さもなくば $p_{new} := \text{SharedRW}$.
2. 追加したい新規アイテムは, new_item = (p_new, t_new, prot) である. 実際にこれをスタックに追加するために, grant_tag にかける.
3. この操作に対応するアクセス a は, p_new が書き込みの許可ならば書き込みアクセスに, さもなくば読み取りアクセスになる.
4. s.stacks[loc] で t_old のタグを持つこのアクセスに対して認可アイテムを探す.
5. p_new == Permission::SharedRW かどうかを確認する.
   • もしそうなら, 認可するアイテムのすぐ上に新しいアイテム new_item を追加する.
   • そうでないなら, loc に対して (a によって決定された) 読み取りあるいは書き込みアクセスを t_old で実行する. そして, 新しいアイテム new_item をスタックの一番上にプッシュする.

これで, 再タグ付けはこれらの引数を決定すればよくなりました. ポインタの種類 k と再タグ付けの種類 (通常の retag, retag[fn], retag[raw] のいずれか) が与えられたとき, 新しいタグ t_new とプロテクター prot は次のように計算されます. 生ポインタは retag[raw] だと, プロテクターなしに新しいタグ $\bot$ を得ます (それ以外ならば無視されます). Box ポインタは新しいタグを得ますが, プロテクターは付きません. 参照は retag[fn] だと新しいタグとプロテクターを得ます.

まとめ

以上により, スタック原理を元にした抽象機械 Stacked Borrows の数学的定義が得られました. これを実装することで, C のようなポインタ型しかない言語であってもボローチェッカーのような検査を行うことができます.