Dynamic LL-free — オンライン insert / release

`BundleUnbundle_2level_LLfree_dynamic.tla` / `_3level_LLfree_dynamic.tla`

静的 LLfree (BundleUnbundle_2level_LLfree.tla) を拡張し、ランタイムでの子ノード挿入 (insert(online=true)) と解放 (release) を加える。木構造は固定ではなく、各イテレーションで動的に変化する。

priority gating (CanProceed / TagAfterFail / TagAfterSuccess / PreemptTag / ClearMyTags) は 2-level LLfree と同一 — slides_layer2_LLfree.html 参照。

木構造 (dynamic)

    Parent
     ├── DynChild1  (挿入/解放はランタイムで)
     └── DynChild2  (同上)

両子ノードは初期状態では未挿入 (own priority wrapper)。 Phase 1 で insert によって Parent に attach し、Phase 2 で commit + release を交互に実行。

Per-thread role 構成

役割 (CONSTANT)	動作
`InsertThreads`	`insert(online=true)` を実行 — 未挿入の子を選んで Parent に attach
`RootThreads`	`CommitParent` — Parent snapshot を取り、見つかった子の payload を全部 +1
`LeafThreads`	`CommitChild` — snapshot で discover した各子を 1 つずつ direct commit
`ReleaseThreads`	子を release (自分の commit が完了してから)

動的 discovery が要点: 子ノードは hardcode せず、snapshot で見つけたものをコミット対象にする。これにより「挿入直後の半構成状態でのコミット」「解放直前の最終コミット」など、動的フェーズ間の境界 race を網羅。

insert(online=true) と release のモデル化

InsertOnline アクション

InsertOnline(t) ==
    /\ t \in InsertThreads
    /\ pc[t] = "idle"
    /\ \E c \in UninsertedChildren :
        /\ \* ① 親の wrapper を読む
        /\ CanProceed(t, Parent)              \* ★ priority gate
        /\ \* ② 子のパケットを親の sub[c] に書き込んだ新 wrapper を CAS
        /\ LET newSubs == [Parent.sub EXCEPT ![c] = childPacket]
               newW == PriorityWrapper(MakePacket(Parent, payload, newSubs, FALSE), ser)
           IN linkage' = [linkage EXCEPT ![Parent] = newW,
                                       ![c] = BundledRefWrapper(Parent, ser)]
    /\ ClearMyTags(t)                       \* commit success と同じく tag 解放

Release アクション

Release(t) ==
    /\ t \in ReleaseThreads
    /\ \E c \in InsertedChildren :
        /\ \* 親の sub[c] を Null にし、子を own priority wrapper に戻す
        /\ CanProceed(t, Parent)
        /\ CanProceed(t, c)
        /\ ...
        /\ linkage' = [linkage EXCEPT ![Parent] = parentWithNullSlot,
                                   ![c] = PriorityWrapper(originalChildPkt, ser)]

insert と bundle/commit の干渉: 他スレッドが bundle(Parent) 中に insert(c) が走ると、 Phase 4 の m_missing=false finalise が Phase 4 reachability gate を発動して DISTURBED retry → bundling thread が見える「新しい子が増えた」状態で再収集。 priority gating により、insert 側が old/young の関係で待たされる/勝つ。

Static spec との差分 + 検証結果

差分まとめ

項目	static (`_LLfree.tla`)	dynamic (`_LLfree_dynamic.tla`)
子ノード集合	初期から固定 (Child1, Child2)	動的に挿入/解放 (DynChild1, DynChild2)
追加アクション	—	`InsertOnline` / `Release`
thread role	全 thread 同等	`InsertThreads` / `RootThreads` / `LeafThreads` / `ReleaseThreads` で構成
commit ターゲット	hardcode	snapshot で動的 discovery
不変条件	SnapshotConsistency 等 5 件	+ insert/release 整合性チェック

検証結果

cfg	Threads	States	Depth	Time	結果
2-level dynamic 2-thread superfine	2	(~M)	—	—	✅ Pass + liveness
2-level dynamic release superfine live	2	413,884,516	320	7:13	✅ Pass + liveness (ohtaka)
3-level dynamic 2-thread coarse	2	(M~)	—	—	✅ Pass + liveness
3-level dynamic 3-thread release	3	(大規模)	—	—	ohtaka 待ち

413M state の意義: 2-level dynamic で release を含む superfine の liveness 検証は 本仕様体系の最大規模 verification の一つ。動的 insert/release を含む全インターリーブで safety + liveness が成立することを exhaustion で確認。 priority gating + dynamic discovery + bounded variable domain の組み合わせで CONSTRAINT なし完走。

大規模 cfg 実行コマンド

# 2-level dynamic release superfine (ohtaka 推奨)
java -XX:+UseParallelGC -Xmx32g -cp tla2tools.jar tlc2.TLC \
  -workers auto -config BundleUnbundle_2level_LLfree_dynamic_3thr_B_live_mc.cfg \
  BundleUnbundle_2level_LLfree_dynamic.tla