TLA+ 記法（Layer 1参照）

TLA+の基本記法は Layer 1スライドの冒頭 (slides_layer1.html) を参照。
本スライドで新たに登場する記法:

記法意味
MakePacket(node, payload, sub, miss)レコード構築関数。[payload |-> ..., sub |-> ..., missing |-> ..., node |-> ...] を返す。
PriorityWrapper(packet, ser)PacketWrapperレコード。hasPriority=TRUE。
BundledRefWrapper(parentNode, ser)bundleされた状態のwrapper。hasPriority=FALSE, bundledBy=parentNode。
[n \in AllNodes |-> IF ... THEN ... ELSE ...]条件付き関数定義。ノードごとに異なる初期値を設定。
r.fieldレコードのフィールドアクセス。例: w.hasPriority, w.packet.sub[c]
% MaxSerialモジュラー算術。シリアルがMaxSerialで周回し、状態空間を構造的に有限にする。StateConstraintは使用しない。
ModGT(a, b)モジュラー大小比較。LET diff == (a - b + MaxSerial) % MaxSerial IN diff > 0 /\ diff < MaxSerial \div 2。C++の符号付き差分比較に対応。

このモデルの特徴: 変数localはレコードの入れ子構造（local[t].wrapper.packet.sub[c]等）。 C++の構造体のネストに対応する。TLA+では[local EXCEPT ![t].wrapper = w]でネストしたフィールドを更新。

Layer 2: Bundle/Unbundle + Commit

TLA+モデル解説 — BundleUnbundle_2level.tla / BundleUnbundle_3level.tla

最も複雑なモデル。 2レベル・3レベル木での4フェーズbundle、多段unbundle、 および楽観的commitを統合検証する。旧「Layer 1 (stm_commit)」の単一ノードCASコミットは、 本層の CommitTryCAS 直接パスに統合された（2層アーキテクチャ化）。

モデルは3段階の忠実度で切替可能（coarse / fine / superfine — 次スライド参照）。

木構造（固定）

Grand ── Parent ──┬── Child1
                         └── Child2

データ構造

(* Packet: ペイロード + 子パケット + missingフラグ *)
MakePacket(node, payload, sub, miss) ==
    [payload |-> payload, sub |-> sub, missing |-> miss, node |-> node]

(* PacketWrapper: priority（独立）or bundled（親に吸収） *)
PriorityWrapper(packet, ser) ==
    [packet |-> packet, hasPriority |-> TRUE, bundledBy |-> Null, serial |-> ser]

BundledRefWrapper(parentNode, ser) ==
    [packet |-> Null, hasPriority |-> FALSE, bundledBy |-> parentNode, serial |-> ser]

変数 (7個)

VARIABLES
    serial,        \* per-thread シリアルカウンタ
    globalSerial,  \* 最新グローバルシリアル
    linkage,       \* linkage[n]: 各ノードのPacketWrapper
    pc, op, target, local  \* per-thread 状態

3段階の忠実度モデル (coarse / fine / superfine)

本層のTLA+仕様は同じ不変条件を異なる粒度で検証できる。 粒度の選択は .cfg ファイルの定数フラグで切替。 細かいほど状態数が増えるが、C++実装への忠実度が上がる。

モード特徴用途
coarse単一アトミックステップでフェーズをまとめる（最速）。
一部のインターリーブを見逃す可能性はあるが、高水準な不変条件は検証可能。		大規模モデル（3レベル、3スレッド等）のスモークテスト
fine子ノードごとに個別のCASと失敗パスを分離。
Phase3のロールバックは省略（C++実装が行わないため）。		標準的な網羅検証
superfineC++に忠実な5つの最適化パスを有効化:
#1 pre-bundle シリアルCAS、#2 inner bundle のフェーズ分割、
#4 Phase3 の DISTURBED チェック、#5 root-first unbundle 順序、
#6 同一子リトライ（same-child retry）		C++実装との厳密な突き合わせ

TLA+モデル化の際に生じたバグの発見例: BundlePhase3 の allDone 判定が ~hasPriority のみをチェックしており、別スレッドがbundleした子も「完了」と誤判定していた。 BundledRefWrapper(node, ser) との一致で判定するようモデルを修正。 C++実装では全子に対してCASを実行し「既にbundled済みならスキップ」という最適化がないため、 この問題は発生しない。TLA+モデル固有のバグであった。

Bundle: 4フェーズCASプロトコル

Phase 1: Collect — 子パケットを収集

BundlePhase1(t) ==
    /\ LET childPkts == [c \in children |->
           IF childWs[c].hasPriority /\ ~childWs[c].packet.missing
           THEN childWs[c].packet     \* 子が完全 → 取得
           ELSE IF childWs[c].bundledBy = node
           THEN parentW.packet.sub[c]  \* 既にbundled → 既存を使用
           ELSE Null]                  \* 取得不可 → リスタート
       IN
       IF allCollected
       THEN pc' → "bundle_phase2"
       ELSE pc' → "snap_check"  \* リスタート

Phase 2: CAS親 — 新PacketWrapper (missing=TRUE)

BundlePhase2(t) ==
    /\ LET newPkt == MakePacket(node, payload, subs, TRUE)
           newW   == PriorityWrapper(newPkt, ser)
       IN
       IF linkage[node] = oldW    \* CAS: 変わっていなければ
       THEN linkage' = [linkage EXCEPT ![node] = newW]

Phase 3: CAS子 — BundledRefWrapperに置換

BundlePhase3(t) ==
    /\ IF allMatch   \* 全子が期待値と一致
       THEN linkage' = [n \in AllNodes |->
           IF n \in children
           THEN BundledRefWrapper(node, ser)  \* 子 → 親への逆参照
           ELSE linkage[n]]

Phase 4: Finalize — missing=FALSE

BundlePhase4(t) ==
    /\ LET finalPkt == MakePacket(node, payload, sub, FALSE)  \* ← FALSE!
       IN
       IF linkage[node] = oldW
       THEN linkage' = [linkage EXCEPT ![node] = finalW]
            \* → 整合的スナップショットが可能に

Unbundle: コミット時の解体

なぜ必要か

bundleされた子ノードにコミットするには、まず祖先のbundleチェーンを解体する必要がある。 コミット対象の子から bundledBy を辿って根側の祖先を特定し、各祖先の missing を TRUE に立ててから子を priority に戻す。

Step 1: UnbundleWalk — 祖先リスト構築

UnbundleWalk(t) ==
    \* コミット対象の子から bundledBy チェーンを上向きに辿り、
    \* CAS すべき祖先ノード群 casTargets を構築する
    \* (child → parent → (3レベルでは) grand)
    /\ local' = [local EXCEPT ![t].casTargets = chain]
    \* superfine #5: 3レベルではリストを root-first で構築
    \* (C++順に合わせ、root→leaf順でCASする)

Step 2: UnbundleCASAncestors / UnbundleCASLoop — 祖先の missing=TRUE 化

UnbundleCASAncestors(t)   \* 2レベル版 (BundleUnbundle_2level.tla)
UnbundleCASLoop(t)         \* 3レベル版 (BundleUnbundle.tla)
    \* casTargets の各祖先について、wrapper を新しい wrapper に CAS。
    \* missing=TRUE にするだけで、子スロット sub[c] はそのまま保持する
    \* (Phase3 のロールバックや後続の復旧に必要なため Null 化しない)
    /\ LET newPkt == MakePacket(anc, anc.payload, anc.sub, TRUE)
           newW   == PriorityWrapper(newPkt, ser)
       IN linkage' = [linkage EXCEPT ![anc] = newW]
    \* coarse: 全祖先を1ステップで / fine: 1ノードずつ

Step 3: UnbundleCASChild — 子を priority に復元

UnbundleCASChild(t) ==
    \* コミット対象の子を BundledRefWrapper から PriorityWrapper に復元。
    \* 新しい(コミット後の)payload を載せた新 packet を格納する。
    /\ LET newChildW == PriorityWrapper(newpacket, ser)
       IN linkage' = [linkage EXCEPT ![node] = newChildW]

Unbundle 流れ（多段共通）:
① UnbundleWalk で祖先リスト casTargets を構築 → ② 各祖先を missing=TRUE に CAS（子スロットは保持） → ③ コミット対象子を Priority+新payload に CAS。
重要: 祖先の sub[c] スロットは Null 化しない。missing=TRUE フラグだけで「この部分木は一時的にスナップショット不可」を表し、Phase3 ロールバック時の参照元として残す。

superfine #5（3レベル時のみ）: casTargets を root-first 順（grand → parent → child 方向）で 構築し、祖先のCASも root-first で実行する。C++実装の走査順と一致させることで、 他スレッドの bundle/unbundle との競合ケースを忠実に再現する。

Commit: 直接コミットと親/祖父スコープコミット

2種類のコミット

本モデルのコミットは 2系統 ある:

CommitParent (2レベル) / CommitGrand (3レベル)

CommitParent(t)   \* 2レベル: Parent スコープで +1 を全 Child payload に伝播
CommitGrand(t)    \* 3レベル: Grand スコープで +1 を全 Grandchild payload に伝播
    \* Parent/Grand の wrapper に対する単発CAS。sub[c] 内の各 payload を
    \* (p + 1) % MaxPayload に更新し、スコープ全体を 1 アクションで確定する。
    \* bundle 状態の部分木でも、その内部 payload が連動して +1 されることを検査する。

直接コミットのパイプライン (CommitRead → CommitTryCAS → CommitDone)

CommitRead(t) ==
    \* CAS 直前に最新の linkage[node] を読み直す
    /\ local' = [local EXCEPT ![t].wrapper = linkage[target[t]]]

CommitTryCAS(t) ==
    IF linkage[node] = oldW
    THEN linkage' = [linkage EXCEPT ![node] = newW]   \* CAS成功 → commit_done
    ELSE IF linkage[node].hasPriority
    THEN
        IF linkage[node].packet.payload = oldW.packet.payload
        THEN \* ★ 単一ノード最適化: payload 同一なら新しい子を採用して再試行 ★
             local' = [local EXCEPT ![t].wrapper = linkage[node], ...]
        ELSE \* 真の競合 → fail
    ELSE
        \* bundleされた → unbundle_walk へ遷移
        pc' → "unbundle_walk"

CommitDone(t) ==
    \* コミット完了処理: iterBudget を -1、childQueue から次の子を取り出す
    \* キューが空なら idle へ戻り、iterBudget=0 なら終了状態へ
    /\ iterBudget' = [iterBudget EXCEPT ![t] = @ - 1]

ライフサイクル変数と終端条件

iterBudget / childQueue / MaxCommits: 各スレッドは MaxCommits 回のイテレーションを実行する。各イテレーションは 「1回の親/祖父スコープコミット（CommitParent/CommitGrand）＋ 各子への直接コミット（CommitRead/TryCAS/Done）1回ずつ」 から構成される。childQueue[t] はそのイテレーション内で未コミットの子リスト、 iterBudget[t] は残りイテレーション数。

TerminalPayloadCheck: 全スレッドが iterBudget=0 かつ idle になった終端状態で、 各直接子の payload が (2 × MaxCommits × |Threads|) % MaxPayload と一致することを検査。 深いコミット(+1) と直接コミット(+1) の両系統が正しく反映されたことを保証する。

単一ノード最適化: CAS 失敗時に linkage[node].hasPriority が保たれていて payload が自分の期待値と同じなら、子スロットだけが他スレッドに差し替わったとみなし、 新しい子パケットを採用して CAS を再試行する。無駄な abort を減らす。

検証された不変条件 (5件)

\* 1. missing=FALSEなら全子パケットが存在
SnapshotConsistency ==
    \A n \in InnerNodes :
        (w.hasPriority /\ ~w.packet.missing) =>
            (\A c \in ChildrenOf(n) : w.packet.sub[c] /= Null)

\* 2. 非ルートノードはpriority OR bundledBy≠Null
NoPriorityLoss ==
    \A n \in AllNodes \ {Grand} :
        w.hasPriority \/ w.bundledBy /= Null

\* 3. bundledByチェーンが有効（2ホップ以内にpriorityに到達）
BundleChainValid ==
    \A n \in AllNodes \ {Grand} :
        (~w.hasPriority /\ w.bundledBy /= Null) =>
            pw.hasPriority \/ pw.bundledBy /= Null

\* 4. bundledByは常に構造上の親を指す
BundledByCorrect ==
    \A n \in AllNodes \ {Grand} :
        ~w.hasPriority => w.bundledBy = ParentOf(n)

\* 5. ルートは常にpriority
GrandAlwaysPriority ==
    linkage[Grand].hasPriority

検証結果（StateConstraintなし、モジュラー算術）

モデル粒度スレッドMaxCommits状態数時間結果
2レベルcoarse21906K12秒✅ Pass（完全）
2レベルcoarse25~3.2M—✅ Pass（完全）
3レベルcoarse21110K3秒✅ Pass（完全）
3レベルcoarse25~8.5M—✅ Pass（完全）
3レベルall-fine211.2M22秒✅ Pass（完全）
2/3レベルfine/superfine (deep)2〜35——ohtaka待ち
モジュラー算術でシリアルを有限化。StateConstraintは使用しない。production構成は MaxSerial=512（2レベル）/ 1024（3レベル）。

検証の意味: 2スレッドが同時にsnapshot/commit/bundle/unbundleを任意の組み合わせで 実行するすべてのインターリーブで、5つの不変条件が保持される。coarseは単一ステップで最速、 fineは子ごとにCAS分離、superfineはC++最適化パスを忠実に再現する。

TLA+で発見したバグ: BundlePhase3のfine粒度において、allDone判定が ~hasPriorityのみをチェックしており、別スレッドがbundleした子も「完了」と 誤判定していた。修正後は自スレッドの BundledRefWrapper(node, ser) と 一致するかで判定する（C++実装は「既にbundled済みならスキップ」という最適化を持たず、 全子にCASするため元々この問題は発生しない）。

2層アーキテクチャの全体像

層何を抽象化何を検証状態数
Layer 1—（ハードウェア直接）参照カウント、ABA、メモリ安全性8.7M（2スレッド完全）
Layer 2atomic_shared_ptrを正しいCASレジスタにBundle/Unbundle + 楽観的commit、サブツリー整合性906K〜8.5M（coarse/fine完全、superfine待ち）

2層に整理した経緯: 旧「Layer 1 (stm_commit)」の単一ノードCASコミットは、 Layer 2 の CommitTryCAS 直接パス（単一ノードCASコミット）に自然に統合できるため、 独立層としては不要と判断。bundle/unbundleと楽観的commitを同じ仕様内で検証することで、 干渉パターンの網羅性が向上した。
Layer 1は完全探索済み、Layer 2はcoarse/fine完全探索済み、superfine/深いfineはohtaka実行待ち。

C++ ↔ TLA+ ↔ 生成C11 対応表

変数の対応

TLA+ 変数C++ (transaction_impl.h)生成C11 (test_bundle_3level.c)
linkage[n]atomic_shared_ptr<PacketWrapper> n->m_link_Atomic(uint64_t) linkage[4]
64bitパック（Wrapper構造体）
linkage[n].hasPriorityPacketWrapper::hasPriority()Wrapper.has_priority (bit field)
linkage[n].bundledByPacketWrapper::bundledBy()Wrapper.bundled_by
linkage[n].packet.payloadPacket::payload()Wrapper.payload
linkage[n].packet.sub[c]Packet::subpackets()[i]Wrapper.sub_child1/2
serial[t]SerialGenerator (Lamport clock)uint8_t thread_ser (local)
ModGT(a,b)符号なし減算→符号付き再解釈mod_gt(a,b): (a-b+MAX)%MAX < MAX/2

アクションの対応

TLA+ アクションC++ コード生成C11 関数
SnapRead + SnapCheck
（3レベルでは SnapCheck のみ）		snapshot()
transaction_impl.h:842-870		snapshot_grand()
load_wrapper() → priority/missing判定
BundlePhase1〜4bundle()
transaction_impl.h:1077-1171		snapshot_grand()内
collect → CAS親 → CAS子 → finalize
InnerPhase2/3/4
（3レベルのみ）		bundle() の内側 bundle 部分
transaction_impl.h:1100-1171		snapshot_grand()内
Grand bundle 時の Parent 側 inner bundle（superfine ではフェーズ分割、fine では BundlePhase1 に畳み込む）
CommitParent（2レベル）
CommitGrand（3レベル）		commit() の親/祖父スコープ版
transaction_impl.h:1245-1270		commit_parent() / commit_grand()
内側の全 child payload を +1 する「深い」コミット
CommitReadcommit() の CAS 直前リロード
transaction_impl.h:1245-1260		commit_child()内
CAS 試行直前の load_wrapper
CommitTryCAScommit()
transaction_impl.h:1245-1270		commit_child()
直接CAS + single-node optimization
CommitDonecommit() 完了処理
transaction_impl.h:1265-1275		commit_child() の末尾
iterBudget を減算し、次の子または idle へ遷移
UnbundleWalksnapshotSupernode()
transaction_impl.h:696-755		commit_child()内
bundledBy チェーンを辿って casTargets を構築（superfine #5 は root-first）
UnbundleCASAncestors（2レベル）
UnbundleCASLoop（3レベル）		transaction_impl.h:1367-1379commit_child()内
各祖先に対して cas_wrapper(anc, ... missing=TRUE)。子スロット sub は Null 化せず保持
UnbundleCASChildtransaction_impl.h:1383-1389commit_child()内
child → priority復元（新 payload 載せ）

Layer 2の特徴: 生成C11では全ノードのlinkageを64bitにパックし、 1回のatomic_compare_exchangeで全フィールドをアトミックに更新。 TLA+の「1アクション = 1ステップ」に忠実。