▲ 俯瞰

TLA+ 記法ガイド

本スライドで使用するTLA+の演算子・構文

基本演算子

記法意味例
==定義（「〜とは」）Init == ... は「Initとは...のこと」
/\AND（論理積）A /\ B は「AかつB」
\/OR（論理和）A \/ B は「AまたはB」
=>含意（「ならば」）A => B は「AならばB」
~NOT（否定）~A は「Aでない」
\in集合の要素x \in S は「xはSの要素」
\notin集合の非要素x \notin S
\cup和集合S \cup T
\subseteq部分集合S \subseteq T
\A全称量化子（∀, for all）\A t \in Threads : P(t)
\E存在量化子（∃, exists）\E o \in Objects : ...

変数と状態遷移

記法意味例
VARIABLES x, y状態変数の宣言モデルの状態を構成する
x'次の状態でのxの値x' = x + 1 は「xを1増やす」
UNCHANGED <<x, y>>x, yは変化しないこのアクションでは変更なし
Init初期状態の定義全変数の初期値を指定
Next次状態関係（遷移）取りうるアクションの論理和
[][Next]_vars常にNextかstuttering仕様の時相論理式
WF_vars(Next)弱公平性（いつか実行される）活性のために必要

関数・レコード

記法意味例
[x \in S |-> e]関数の定義（S上でeを返す）[t \in Threads |-> 0] は全スレッド0で初期化
f[x]関数fのxでの値global_rc[o] はオブジェクトoのRC
[f EXCEPT ![x] = e]fのx番目だけeに変えた新関数[pc EXCEPT ![t] = "done"]
@EXCEPT内で「現在の値」[f EXCEPT ![x] = @ + 1] は+1
[a |-> 1, b |-> 2]レコード（構造体）r.a でフィールドアクセス

条件分岐・選択

記法意味例
IF P THEN A ELSE B条件式通常のif-then-else
CASE p1 -> e1 [] p2 -> e2パターンマッチp1が真ならe1、p2が真ならe2
LET x == e IN ...局所定義C++のauto x = e;に相当
CHOOSE x \in S : P(x)Pを満たすSの要素を1つ選ぶ非決定的選択

定数・型

記法意味例
CONSTANTSモデルパラメータThreads, Objects, MaxLocalRC
0..N0からNまでの整数集合0..MaxVal
Nat自然数集合型チェック用
BOOLEAN{TRUE, FALSE}型チェック用

CONSTANTS と .cfg ファイル

TLA+仕様のCONSTANTSは、モデルのパラメータを定義する。具体的な値は .cfgファイル（TLCの設定ファイル）で指定する。

仕様 (.tla)設定 (.cfg)意味
CONSTANTS Threads, ObjectsThreads = {t1, t2}
Objects = {o1, o2}		モデルチェック時の具体的な値を設定
CONSTANTS EnableCAS, EnableRecycleEnableCAS = TRUE
EnableRecycle = TRUE		機能のON/OFFフラグ

スレッド数・オブジェクト数を増やすと状態空間が指数的に増大する。 通常は2〜3スレッド、2オブジェクトで検証し、対称性（SYMMETRY）で縮約する。

StateConstraint と INVARIANT

記法場所意味
CONSTRAINT
StateConstraint		.cfgファイルこの条件を満たさない状態に到達したら、その先の探索を打ち切る（枝刈り）。状態空間を有限にするために使う。安全性の検証ではない。
INVARIANT
MemorySafety		.cfgファイル到達したすべての状態でこの条件が成り立つことを検証する。違反があればバグとして報告。

重要な違い: CONSTRAINTは「この範囲だけ調べる」（探索の制限）。 INVARIANTは「これが常に成り立つか？」（安全性の検証）。
例: global_rc[o] <= 5 をCONSTRAINTに書くと、global_rcが5を超える状態は探索されない（見逃す可能性）。 同じ式をINVARIANTに書くと、global_rcが5を超えたらエラーとして報告される。

本モデルではStateConstraintを使用しない。 C++のスコープ破棄やモジュラー算術により状態空間を構造的に有限にし、 人為的な枝刈りなしで全到達可能状態を探索する。

{a, b, c}有限集合{"scan", "cas", "idle"}

読み方のコツ: TLA+のアクション（例: ReserveScanCAS(t)）は 「この条件が成り立つとき、変数をこう変える」という宣言。 /\で並んだ条件がすべて真のときに実行可能。 x'が次の状態、UNCHANGEDは変えないもの。

Layer 1: atomic_shared_ptr + commit primitives

TLA+モデル解説 — atomic_shared_ptr.tla

2層アーキテクチャ: KAME の TLA+ 検証は 2 層構成。 Layer 1 = atomic_shared_ptr（タグ付きポインタ）＋ commit-style プリミティブ (compareAndSet_impl_, scoped_atomic_view, drain release_tag_ref_)。 旧「stm_commit」層はモダン API に統合済（commit fd5b2522）。
Layer 2 = bundle/unbundle + LL-free negotiate。Layer 1 は safety only。 活性 (livelock-free) は Layer 2 の older-wins 機構が担保する（本スライド末尾参照）。

何をモデル化しているか

kamepoolalloc/atomic_smart_ptr.h の 全ボキャブラリを sequential consistency 下で網羅検証。 GenMC (RC11) と相補的に、全スレッドインターリーブを TLC で exhaustion する。

モデルの構成要素

要素TLA+での表現C++での対応
共有ポインタptr + local_rcm_ref (uintptr_t、上位=ptr, 下位=tag)
オブジェクトObjects (有限集合)Ref構造体
参照カウントglobal_rc[o]intrusive o->refcnt (atomic)
解放状態freed[o]delete呼び出し
スレッド状態pc[t], thr_*, scope_*[t]関数内のローカル変数 + scope オブジェクト

変数一覧 (現行 18 個)

VARIABLES
    ptr,            \* 共有ポインタ（Object or NULL）
    local_rc,       \* ローカル参照カウンタ（タグ）
    global_rc,      \* global_rc[o]: 各オブジェクトのグローバルRC
    freed,          \* freed[o]: 解放済みフラグ
    pc,             \* 各スレッドのプログラムカウンタ
    thr_op,         \* "load", "cas", "idle"
    thr_pref,       \* acquire_tag_ref_で読んだポインタ
    thr_rcnt,       \* acquire_tag_ref_で読んだローカルRC
    thr_old,        \* CAS: 期待する旧オブジェクト
    thr_new,        \* CAS: 新オブジェクト
    thr_holds,      \* local_shared_ptrで保持中のオブジェクト集合
    thr_rtr_ctx,    \* release_tag_ref_の戻り先 (load_done / cas_retry / scope_release 等)
    iterBudget,     \* per-thread 残りオペレーション数
    (* drain パラメタ — release_tag_ref_(pref, added_global_rcnt) *)
    thr_cas_rcnt,   \* 1回のCASで解放を試みるタグ数
    thr_added_grc,  \* caller が事前に追加した global rcnt 量
    thr_drained,    \* output: 実際に drain できたタグ数
    (* scoped_atomic_view RAII *)
    scope_state,    \* scope_state[t] ∈ {"none", "tagheld"}
    scope_pref      \* scope の m_pref

モデル簡略化の決定: (1) WEAK CAS の spurious failure は未モデル化（strong-CAS のスーパセットなので safety 上 sound、weak は GenMC で別途検証）。 (2) ABA-by-recycling は未モデル化（shared-pointer の oldr 所有契約で構造的に発生不可能）。 (3) scope の "empty" / "owned" は "none" に集約（観測同値）。

acquire_tag_ref_: アトミック読み取り + CAS

C++ソース: atomic_smart_ptr.h 行462-488

C++のm_ref.load()は単一アトミック操作であり、ポインタとローカルRCは 常に同じload値から導出される。TLA+でもこれを単一ステップでモデル化する。

(* アトミック読み取り: ptrとlocal_rcを同時に読む *)
ReserveScanRead(t) ==
    /\ pc[t] = "rs_read"
    /\ thr_pref' = [thr_pref EXCEPT ![t] = ptr]       \* ← ptrを読む
    /\ thr_rcnt' = [thr_rcnt EXCEPT ![t] = local_rc]  \* ← local_rcを読む（同時）
    /\ pc' = [pc EXCEPT ![t] = "rs_cas"]

(* CAS — ポインタとRCの両方が一致する場合のみ成功 *)
ReserveScanCAS(t) ==
    /\ pc[t] = "rs_cas"
    /\ thr_pref[t] /= NULL
    /\ \/ (* CAS成功: ptr AND local_rc の両方が一致 *)
          /\ ptr = thr_pref[t]
          /\ local_rc = thr_rcnt[t]
          /\ local_rc' = thr_rcnt[t] + 1  \* ピン留め！
       \/ (* CAS失敗: 読み取りに戻ってリトライ *)
          /\ ~(ptr = thr_pref[t] /\ local_rc = thr_rcnt[t])
          /\ pc' = [pc EXCEPT ![t] = "rs_read"]

ポイント: 読み取りからCASまでの間に他スレッドがptr/local_rcを変更しても、 CASがフルワード比較（ptr + local_rc の両方）するため、不整合は必ず検出される。

scan_: load_shared_() の3ステップ

C++ソース: 行494-503

(* Step 1: acquire_tag_ref_ → アトミック読み取り + CASでローカルRCを+1 [上のスライド参照] *)

(* Step 2: グローバルRCを+1 — relaxedで安全 *)
ScanIncGlobal(t) ==
    /\ pc[t] = "scan_inc"
    /\ global_rc' = [global_rc EXCEPT ![thr_pref[t]] = @ + 1]
    /\ pc' = [pc EXCEPT ![t] = "scan_leave"]

(* Step 3: release_tag_ref_ → ローカルRCを-1 *)
acquire_tag_ref_ → global_rc++ → release_tag_ref_

release_tag_ref_: フォールバック分岐

LeaveScanCAS(t) ==
    \/ (* CAS成功: ptrが変わっていない → ローカルRCを-1 *)
       /\ ptr = thr_pref[t] /\ local_rc = thr_rcnt[t]
       /\ local_rc' = thr_rcnt[t] - 1

    \/ (* CAS失敗, ptrが同じ → リトライ *)
       /\ ptr = thr_pref[t]
       /\ pc' = [pc EXCEPT ![t] = "ls_read"]

    \/ (* CAS失敗, ptrが変わった → フォールバック: global_rc-- *)
       /\ ptr /= thr_pref[t]
       /\ pc' = [pc EXCEPT ![t] = "ls_global"]

(* フォールバック: 入れ替えたスレッドがローカルRC分を転送済み *)
LeaveScanGlobal(t) ==
    /\ global_rc' = [global_rc EXCEPT ![o] = @ - 1]
    /\ IF global_rc[o] = 1
       THEN freed' = [freed EXCEPT ![o] = TRUE]  \* → 解放！

このフォールバックが不可欠: なしでは参照カウンタリーク or use-after-free。TLA+検証で確認。

compareAndSwap_: 6フェーズ

C++ソース: 行556-603

PhaseTLA+ Action動作
1CASPreInc新オブジェクトのglobal_rc++
2CASReserve→rs_*acquire_tag_ref_でピン留め
3CASCheckpref != oldrなら失敗を返す
4CASTransferローカルRC分をglobal_rcに転送
5CASSwapCAS (acq_rel): ポインタ入れ替え
6CASCleanup旧オブジェクトのglobal_rc--
(* Phase 4: ローカルRC分をグローバルに転送 *)
CASTransfer(t) ==
    /\ IF thr_pref[t] /= NULL /\ thr_rcnt[t] /= 1
       THEN global_rc' = [global_rc EXCEPT
                ![thr_pref[t]] = @ + thr_rcnt[t] - 1]

(* Phase 5: CAS — フルワード比較 *)
CASSwap(t) ==
    \/ /\ ptr = thr_pref[t] /\ local_rc = thr_rcnt[t]  \* 一致
       /\ ptr' = thr_new[t]
       /\ local_rc' = 0
    \/ /\ ~(...)  \* CAS失敗 → Undo → release_tag_ref_ → リトライ

ABAとの関係: 呼び出し元はlocal_shared_ptrでoldrを保持 → global_rc > 0 → 解放されない → ABAは構造的に不可能。
ただしload_shared_()ではスレッドが参照を持たないため、TLA+ではABAリサイクルを sound over-approximationとしてモデル化。

swap: 無条件交換

CASとの違い: swapは旧ポインタを確認せず無条件に入れ替える。 PreIncフェーズ不要（所有権の交換であり追加ではない）。

プロトコル

StartSwap(t) ==
    /\ EnableSwap
    /\ pc[t] = "idle"
    /\ \E newObj \in Objects \cup {NULL} :
       /\ (newObj /= NULL => thr_holds[t][newObj] > 0)
       /\ thr_new' = [thr_new EXCEPT ![t] = newObj]
    /\ pc' = [pc EXCEPT ![t] = "cas_acquire"]  \* PreIncをスキップ
    /\ thr_op' = [thr_op EXCEPT ![t] = "swap"]

\* acquire_tag_ref_ 成功後:
\*   CASTransfer: global_rc[pref] += local_rc（タグ→グローバル転送）
\*   CASSwap: CAS ptr from pref to newObj, local_rc → 0
\*   CASCleanup不要（PreIncしていない）

Reset: local_shared_ptr::reset()

Reset(t) ==
    /\ pc[t] \in {"idle", "done"}
    /\ \E o \in Objects :
       /\ thr_holds[t][o] > 0
       /\ thr_holds' = [thr_holds EXCEPT ![t][o] = @ - 1]
       /\ global_rc' = [global_rc EXCEPT ![o] = @ - 1]
       \* decAndTest: global_rcが0に達したら解放
       /\ freed' = [freed EXCEPT ![o] =
            IF global_rc[o] = 1 THEN TRUE ELSE @]

swap vs load が重要な理由

swapperがポインタを入れ替えている最中にloaderが acquire_tag_ref_を実行中の場合、loaderのrelease_tag_ref_は ポインタ変更を検知しglobal_rcデクリメントにフォールバックする。 swapperのCASTransferが残存local_rcをglobal_rcに 転送することでバランスが取れる。このタグ→グローバル転送パスは atomic_shared_ptrの正しさの核心であり、 swap と load が並行実行されて初めて行使される。

scoped_atomic_view<T> RAII (新)

commit プリミティブ統合: 旧 stm_commit → 本層に吸収済（fd5b2522）

外部スコープの参照 (oldr) を 1 つの tag ref として握り続ける RAII 型。 内側の compareAndSet_impl_<scoped, ...> は acquire を省略 (scope が +1 を保証) し、 CAS 成功時に fetch_sub(2) で「m_ref の release + scope の tag share」を同時に吸収する。

状態遷移 (TagHeld の 2 状態モデル)

ScopeAcquire(t) ==                \* scoped_atomic_view ctor
    /\ scope_state[t] = "none"
    /\ \* acquire_tag_ref_ で tag を 1 つ握る
    /\ scope_state' = [scope_state EXCEPT ![t] = "tagheld"]
    /\ scope_pref' = [scope_pref EXCEPT ![t] = thr_pref[t]]

ScopeCASConsume(t) ==          \* compareAndSet_impl_<scoped> 成功
    /\ scope_state[t] = "tagheld"
    /\ \* step4 = +T (full add), CAS 成功で fetch_sub(2) → tag 1 + ref 1 を同時消費
    /\ local_rc' = local_rc - 2
    /\ scope_state' = [scope_state EXCEPT ![t] = "none"]

ScopeDestruct(t) ==            \* scoped_atomic_view dtor
    /\ scope_state[t] = "tagheld"
    /\ \* release_tag_ref_(scope_pref, 1) を呼ぶ
    /\ thr_cas_rcnt' = 1
    /\ pc' = [pc EXCEPT ![t] = "rtr_read"]

Drain release_tag_ref_ パターン

\* release_tag_ref_(pref, T) — 1 回の CAS で min(local_rc, T) 個のタグを抜く
ReleaseTagRefCAS(t) ==
    /\ pc[t] = "rtr_cas"
    /\ \/ \* CAS 成功: ptr/local_rc が読み取り値と一致
          /\ ptr = thr_pref[t] /\ local_rc = thr_rcnt[t]
          /\ LET drained == Min(thr_rcnt[t], thr_cas_rcnt[t]) IN
             /\ local_rc' = thr_rcnt[t] - drained
             /\ thr_drained' = drained
       \/ \* CAS 失敗 → リトライ or fallback global path
          /\ ~(ptr = thr_pref[t] /\ local_rc = thr_rcnt[t])

\* drain 完了後: 余剰の global rcnt を fetch_sub で打ち消す
ReleaseTagRefExcess(t) ==
    /\ LET excess == thr_added_grc[t] - thr_drained[t] IN
       global_rc' = [global_rc EXCEPT ![pref] = @ - excess]

意義: drain release は load_shared_ の bulk transfer パスを成立させる中核。 従来は 1 tag ずつ release していたのを「caller が refcnt.fetch_add(rcnt) で先に global を確保 → release_tag_ref_(pref, rcnt) で複数 tag を 1 CAS で drain」という設計に。 競合スレッドの tag IOU を奪取することで m_ref contention を refcnt へ移し、 スループットが大幅向上 (commit d93fc7de, +23%)。

ABA は scope 外: 旧版にあった Recycle アクションと EnableRecycle フラグは 削除済 (686460d5)。shared-pointer 所有契約 (oldr->refcnt ≥ 1) で oldr は生存保証されるため、ABA-by-recycling はタグ付きポインタプロトコルの 構造的問題ではない。明示的に scope 外とした。

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

#不変条件意味
1TypeOK型不変条件
2MemorySafetytag/ref を握っているオブジェクトは解放されない
3NoUseAfterFreelocal_shared_ptr が握るオブジェクトは解放されない
4GlobalRCNonNeg生存オブジェクトの global_rc ≥ 0
5FreedImpliesZeroRC解放済みなら global_rc = 0
6InstalledNotFreedptr が指すオブジェクトは解放されない
7LocalRCBoundedlocal_rc ≤ 2 × |Threads| (各スレッド scope tag 1 + in-flight acquire 1)
8QuiescentCheck全スレッド idle 時に freed[o] = (global_rc[o] = 0)
9TerminalCheckiterBudget=0 + 全 ref/scope 解放後、ptr は rc=1、他は freed
10ScopeConsistentscope_state と scope_pref 整合; tagheld なら scope_pref not freed
ScopeConsistent ==
    \A t \in Threads :
        \/ scope_state[t] = "none" /\ scope_pref[t] = NULL
        \/ scope_state[t] = "tagheld"
           /\ scope_pref[t] /= NULL
           /\ freed[scope_pref[t]] = FALSE

活性 (liveness): 意図的に違反

EventuallyAllDone == <>AllDone は Layer 1 で fail する。 TLC は 2 スレッドが相互 CAS retry に入る lasso を発見 (cas_retry → cas_acquire → atr_cas → ...)。 内部 CAS リトライは iterBudget を消費しないため、 adversarial scheduler が無限ループを維持できる。これは想定どおり: 活性は Layer 2 の priority older-wins (LL-free negotiate) 機構が担保する。

検証結果 (CONSTRAINT なし、SYMMETRY 適用)

cfgスレッドMaxOps含むオペ状態数Depth時間結果
1thr_mc.cfg13load+CAS+swap+scope4,01433<1s✅ Pass (完全)
small_mc.cfg22load+CAS+scope613,9906912s✅ Pass (完全)
all_mc.cfg23load+CAS+swap+scope (full)66,537,058841h 30min✅ Pass (完全)
3thr_cas_mc.cfg32load+CAS+scope———ローカル実行中
live_mc.cfg22<>AllDone liveness(lasso)—40s❌ Fail (想定どおり)

詳細: kamestm/tests/VERIFICATION.md §2

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

著者による C++ ↔ TLA+ 照合、および TLA+ → 生成 C11 変換の確認用（続編 → Layer 2 LLfree スライド / slides_layer2_LLfree.html）

変数の対応

TLA+ 変数C++ (atomic_smart_ptr.h)生成 C11 / GenMC test
ptr + local_rcm_ref (uintptr_t、上位=ptr, 下位=tag)_Atomic(uintptr_t) g_ref
global_rc[o]o->refcnt (intrusive atomic)_Atomic(uintptr_t) obj_refcnt[]
freed[o]delete 呼び出しint obj_freed[]
thr_pref[t] / thr_rcnt[t]Ref* pref / Refcnt rcnt (local)local 変数
thr_holds[t][o]local_shared_ptr の生存数thread-local hold index
thr_cas_rcnt / thr_added_grc / thr_drainedrelease_tag_ref_(pref, added_global_rcnt) の cas_rcnt 引数cds_test_multi_cas_excess.c
scope_state[t] / scope_pref[t]scoped_atomic_view<T> の m_pref + statecds_test_scoped_weak.c

アクションの対応

TLA+ アクションC++ 関数 (atomic_smart_ptr.h)memory_order
AcquireTagRefRead + AcquireTagRefCASacquire_tag_ref_() (行 1058-1108)relaxed → acq_rel
LoadSharedBulkAdd (新)load_shared_() bulk transfer
refcnt.fetch_add(rcnt) + drain (行 1116-1128)		relaxed
ReleaseTagRefCAS + ReleaseTagRefExcessrelease_tag_ref_(pref, T) drain (行 1158-1206)
min(local_rc, T) tag を 1 CAS で抜く + 余剰 fetch_sub		acq_rel
CASPreInc → CASSwap → CASCleanupcompareAndSwap_() 6 phases (legacy, 行 550-650)relaxed / acq_rel
compareAndSet_impl_ パス統一テンプレ compareAndSet_impl_<OldrT, NewrT, false, RETAIN_NEWR> (行 1240-1450)
Set / Swap を 1 つの実装に統合		relaxed / acq_rel
compareAndSet_impl_<SCOPED> パスscope hold で acquire 不要; step4 = +T (full add); 成功時 fetch_sub(2)acq_rel
ScopeAcquire → ScopeCASConsume / ScopeDestructscoped_atomic_view ctor / CAS / dtor (行 598-845)acq_rel
Resetlocal_shared_ptr::reset() fetch_sub(1) + delete check (行 433-444)acq_rel

検証の三角形:
C++ 実装（著者が書いた）← 著者が独立に照合 → TLA+ 仕様 (sequential consistency)
TLA+ → 生成 C11 (tests/tlaplus/test_*.c) → GenMC 検証（RC11 memory order）
さらに著者が独立に書いた C++-derived テスト (tests/cds_atomic_shared_ptr/cds_test_*.c) も GenMC で検証。
三角形 + 独立テストの両輪で TLA+ モデルの忠実性が確認される。