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

`BundleUnbundle_2level_LLfree_dynamic.tla` / `_3level_LLfree_dynamic.tla`

LLfree の Layer 2 仕様にランタイムでの子ノード挿入 (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 のモデル化

insert(online=true) — 5 ステップの CAS パイプライン（単一アクションではない）

\* insert は 5 アクションに分割され、TLC が「途中まで構築された insert」の
\* 全 interleaving を探索できる（対象: \E c : ~inserted[c]）。
InsertStart → InsertCASParent → InsertReadChild →
InsertCASChild(t):  linkage'[c] = InsertedRef(Parent, ser, cpkt)   \* パケット保持 ref
InsertFinal(t):     linkage'[Parent] = PriorityWrapper(
                       MakePacket(Parent, _, newSub, TRUE), ser)   \* 別 CAS、missing=TRUE
                     \* 成功時: inserted'[c]=TRUE, ClearMyTags(t)

release — 4 ステップの CAS パイプライン

ReleaseStart → ReleaseCASParent → ReleaseReadChild → ReleaseCASChild
    \* 親スロット CAS と子スロット CAS は別アクション；
    \* 2 つの CanProceed gate (Parent / c) は別ステップに存在。

insert と bundle/commit の干渉: 他スレッドが bundle(Parent) 中に insert(c) が走ると、 Phase-4 の CAS が freshness チェックに失敗（親 linkage が変化）して retry → bundling thread が見える「新しい子が増えた」状態で再収集。（dynamic spec に reachability gate は無い — それは hardlink 専用。） priority gating により、insert 側が old/young の関係で待たされる/勝つ。

static モードとの対比 + 検証結果

static / dynamic モードの対比

項目	static (`_LLfree.tla`)	dynamic (`_LLfree_dynamic.tla`)
子ノード集合	初期から固定 (Child1, Child2)	動的に挿入/解放 (DynChild1, DynChild2)
追加アクション	—	`Insert`（5 ステップ）/ `Release`（4 ステップ）パイプライン
thread role	Root / Leaf ロール（`RootThreads` / `LeafThreads`）	+ Insert / Release ロール（`InsertThreads` / `ReleaseThreads`）
commit ターゲット	hardcode	snapshot で動的 discovery
不変条件	SnapshotConsistency 等 5 件	+ insert/release 整合性チェック

検証結果

cfg	Threads	States	Depth	Time	結果
2-level dynamic 2-thread superfine (release なし)	2	(~M)	—	—	✅ Pass (safety); liveness は下の release 実行で
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_release_superfine_live_mc.cfg \
  BundleUnbundle_2level_LLfree_dynamic.tla