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

TLA+モデル解説 — atomic_shared_ptr.tla (340行)

2層アーキテクチャにおける本層の位置づけ: 本スライドはかつて「Layer 0」と呼ばれていたが（ファイル名は slides_layer1.html に移動済み）、 論文の2層モデル（Layer 1: atomic_shared_ptr / Layer 2: bundle/unbundle + commit）に合わせてLayer 1に改称。 内容は変更なし。

何をモデル化しているか

kame/atomic_smart_ptr.h の参照カウントプロトコル全体。
C++のロックフリー atomic_shared_ptr を TLA+ で網羅的に検証する。

モデルの構成要素

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

変数一覧 (12個)

VARIABLES
    ptr,            \* ポインタ（Object or NULL）
    local_rc,       \* ローカル参照カウンタ（下位3ビット相当）
    global_rc,      \* global_rc[o]: 各オブジェクトのグローバルRC
    freed,          \* freed[o]: 解放済みフラグ
    pc,             \* 各スレッドのプログラムカウンタ（22状態）
    thr_op,         \* "scan", "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_ls_ctx      \* release_tag_ref_の戻り先

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 が並行実行されて初めて行使される。

ABAリサイクル

Recycle(t) ==
    /\ EnableRecycle             \* フラグで有効/無効を制御
    /\ pc[t] \in {"idle", "done"}
    /\ \E o \in Objects :
       /\ freed[o] = TRUE       \* 解放済みオブジェクトを
       /\ global_rc[o] = 0
       /\ freed' = [freed EXCEPT ![o] = FALSE]   \* 再生!
       /\ global_rc' = [global_rc EXCEPT ![o] = 1]
       /\ thr_holds' = [thr_holds EXCEPT ![t] = @ \cup {o}]

Sound over-approximation: 全操作でリサイクルを許可（実際はcompareAndSwap_では不可能）。 過剰近似の下で安全性が証明されれば、実際のプログラムでも安全。

経緯: 著者は安全性を自明と判断。AIが過剰近似としてモデル化を提案、著者が同意。

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

#不変条件意味
1MemorySafetyピン留め中のオブジェクトは解放されない
2NoUseAfterFreethr_holdsに含まれるオブジェクトは解放されない
3GlobalRCNonNeg生存オブジェクトのglobal_rc ≥ 0
4FreedImpliesZeroRC解放済みならglobal_rc = 0
5InstalledNotFreedptrが指すオブジェクトは解放されない
6LocalRCBoundedlocal_rc ≤ スレッド数
7TypeOK型不変条件
MemorySafety ==
    \A t \in Threads :
        (pc[t] \in {"scan_inc", "scan_leave",
                     "ls_read", "ls_cas", "ls_global",
                     "cas_check", ..., "cas_cleanup"}
         /\ thr_pref[t] /= NULL)
        => freed[thr_pref[t]] = FALSE

検証結果（StateConstraintなし）

構成スレッド状態数時間結果
scan only340,9341秒✅ Pass
scan+CAS (ABAなし)23,549,30412秒✅ Pass (完全)
full (CAS+ABA)28,719,36728秒✅ Pass (完全)
swap+load (ABAなし)2——ohtaka実行中
swap+CAS+ABA26.6×10⁹+18h+部分探索、違反なし (I/O律速)

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

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

変数の対応

TLA+ 変数C++ (atomic_smart_ptr.h)生成C11 (test_atomic_shared_ptr.c)
ptr + local_rcm_ref (uintptr_t)
上位=ptr, 下位=tag		_Atomic(uintptr_t) g_ref
get_ptr() / get_tag()
global_rc[o]o->refcnt (intrusive atomic)_Atomic(uintptr_t) obj_refcnt[NUM_OBJECTS]
freed[o]delete呼び出しint obj_freed[NUM_OBJECTS]
thr_pref[t]Ref* pref (local)uintptr_t pref (local)
thr_rcnt[t]Refcnt rcnt (local)unsigned rcnt (local)
thr_holds[t][o]local_shared_ptrの生存数thread-local hold index

アクションの対応

TLA+ アクションC++ 関数生成C11 関数memory_order
AcquireTagRefRead
+ AcquireTagRefCAS		acquire_tag_ref_()acquire_tag_ref()relaxed → acq_rel
LoadSharedIncGlobalload_shared_()内load_shared()内
fetch_add(refcnt, 1)		relaxed
ReleaseTagRefCAS
/ ReleaseTagRefGlobal		release_tag_ref_()release_tag_ref()acq_rel / acq_rel
CASPreInc → CASSwap
→ CASCleanup		compareAndSwap_()compare_and_swap()relaxed / acq_rel
StartSwap → CASTransfer
→ CASSwap		swap()swap_exchange()acq_rel
Resetlocal_shared_ptr::reset()local_reset()acq_rel (decAndTest)

検証の三角形:
C++実装（著者が書いた）← 著者が独立に照合 → TLA+仕様
TLA+ → 生成C11（C++を参照せず、独立セッションで生成）→ GenMC検証（RC11）
この三角形が閉じることで、TLA+モデルの忠実性が確認可能。