3-level LL-free (Gen 3) — 2-level からの差分

`BundleUnbundle_3level_LLfree.tla`

本スライドは slides_layer2_LLfree.html (2-level LL-free) の続編。 2-level spec の privilege-TID 機構をそのまま継承し、木の深さを 1 段増やす: Grand → Parent → {Child1, Child2}。

priority gating の動作 (CanProceed / TagAfterFail / TagAfterSuccess / PreemptTag / ClearMyTags) と EventuallyAllDone による liveness 検証は完全に同じ — 2-level スライド参照。

木構造

    Grand
     └── Parent
         ├── Child1
         └── Child2

2-level からの追加カバレッジ

項目	2-level	3-level (本仕様)
commit root	`CommitParent`	`CommitGrand` (Grand スコープで全 grandchild payload を +1)
recursive bundle	(なし)	`InnerPhase2`/`3`/`4`: `snapshot(Grand)` が Parent を内側で bundle する
unbundle walk	1 ホップ (`UnbundleCASAncestors`)	2 ホップ (`UnbundleCASLoop`): Child → Parent → Grand
chain navigation	(自明)	`WalkUpChain` / `SnapshotForUnbundle` が `bundledBy` を上向きに辿る
新規不変条件	—	`BundleChainValid` / `BundledByCorrect` / `GrandAlwaysPriority`

Recursive inner bundle

`InnerPhase2` / `InnerPhase3` / `InnerPhase4`

snapshot(Grand) で Parent が missing=TRUE に出会うと、 その中で Parent の bundle を起動する (recursive bundle)。 4-phase プロトコル本体は外側と同一だが、状態空間の forking を抑えるため inner は別アクション (InnerPhase2/3/4) としてモデル化する。

InnerPhase の構造 (superfine では Phase 分割; fine では `BundlePhase1` に畳む)

InnerPhase2(t) ==
    \* Parent の missing=TRUE wrapper を CAS で立てる
    /\ CanProceed(t, Parent)         \* ★ priority gate
    /\ LET newW == PriorityWrapper(MakePacket(Parent, _, _, TRUE), ser)
       IN linkage' = [linkage EXCEPT ![Parent] = newW]

InnerPhase3(t) ==
    \* 全 Child を BundledRefWrapper(Parent, ser) に CAS
    /\ \A c \in {Child1, Child2} : CanProceed(t, c)
    /\ ...

InnerPhase4(t) ==
    \* Parent の missing=FALSE を最終 CAS で立てる
    /\ CanProceed(t, Parent)
    /\ ...

InnerPhase restart の歴史: 仕様開発中に発見・修正された subtle なバグ群 (コミット履歴より):

1d9820bc: InnerPhase3 restart で stale subpackets が lost increment を引き起こす
8d6026e3: InnerPhase4 restart で outer bundle state を clear し忘れる
73bcef3a: InnerPhase2 restart の修正

いずれも C++ 側の対応 path は元々正しく、TLA+ モデル化過程で見つかったモデル固有の bug。 TLA+ 化が C++ より細かい粒度で動作を追ったことの副産物。

Multi-level unbundle walk

`UnbundleWalk` + `UnbundleCASLoop` + `UnbundleCASChild`

Child が 2 段深く bundle されている (Child → Parent → Grand) 状態で commit(Child) を実行する場合、Child を priority に復元する前に bundledBy chain 上の祖先 2 つを全て missing=TRUE にする必要がある。

Step 1: UnbundleWalk — chain 構築

UnbundleWalk(t) ==
    \* 子から bundledBy を辿って祖先 chain を構築
    \* casTargets = <<Grand, Parent>>  (root-first)
    /\ local' = [local EXCEPT ![t].casTargets = chain]
    \* superfine #5: 3-level では root-first 順 (C++ 走査順と一致)

Step 2: UnbundleCASLoop — 祖先を順に missing=TRUE に

UnbundleCASLoop(t) ==
    \* casTargets の各祖先について、wrapper を新しい missing=TRUE PriorityWrapper に CAS
    \* sub[c] は保持 (Phase 3 ロールバックや復旧のため Null 化しない)
    /\ CanProceed(t, anc)
    /\ LET newW == PriorityWrapper(MakePacket(anc, _, anc.sub, TRUE), ser)
       IN linkage' = [linkage EXCEPT ![anc] = newW]
    \* coarse: 全祖先を 1 ステップで; fine: 1 ノードずつ

Step 3: UnbundleCASChild — Child を priority + 新 payload で復元

UnbundleCASChild(t) ==
    /\ LET newChildW == PriorityWrapper(newpacket, ser)
       IN linkage' = [linkage EXCEPT ![node] = newChildW]

追加された不変条件

不変条件	意味
`BundleChainValid`	bundled ノードの `bundledBy` 先は priority か、それ自身が bundled
`BundledByCorrect`	`bundledBy` は常に構造上の親を指す
`GrandAlwaysPriority`	Root (Grand) は常に priority を持つ

検証結果 + 関連 spec

3-level LL-free 検証結果

cfg	Threads	States	Depth	Time	結果
1-thread superfine	1	(small)	—	<1s	✅ Pass (sanity)
2-thread coarse	2	1,497,098	98	1:35	✅ Pass + liveness
2-thread superfine	2	14,109,731	148	19:13	✅ Pass + liveness
3-thread superfine confC (all-root)	3	640,894,951	88	15:25	✅ Pass + liveness (ohtaka)

意味: 3 段の木で 3 スレッドが同時に snapshot / commit / bundle / unbundle を実行する全インターリーブで safety + liveness が成立。LL-free priority 機構が depth-2 の bundle/unbundle 連鎖でも構造的に有限化を保証している。詳細: kamestm/tests/VERIFICATION.md §4。

大規模 cfg の実行

# 1-thread sanity (< 1 s)
java -XX:+UseParallelGC -Xmx8g -cp tla2tools.jar tlc2.TLC \
  -workers auto -config BundleUnbundle_3level_LLfree_1thr_superfine_mc.cfg \
  BundleUnbundle_3level_LLfree.tla

# 2-thread coarse with liveness (~2 min)
java -XX:+UseParallelGC -Xmx14g -cp tla2tools.jar tlc2.TLC \
  -workers auto -config BundleUnbundle_3level_LLfree_coarse_mc.cfg \
  BundleUnbundle_3level_LLfree.tla

3-thread superfine 等の大規模構成は ohtaka が必須。doc/ohtaka_handoff.md 参照。