KAME のロックフリー Software-Transactional-Memory コアは、抽象プロトコルから実行バイナリまでの隙間を埋める 3 手法で検証されている。
最下層で GenMC がタグ付きポインタ atomic_shared_ptr 参照カウントを C/C++ RC11 弱メモリモデル下で網羅的にモデル検査
(18 プログラム、最大 ~117 万実行) し、全 memory_order 注釈が use-after-free / double-free / leak に対し安全であることを証明する。
その上で TLA+/TLC が全スレッドインターリーブを網羅探索する: Layer 1 は atomic_shared_ptr + commit プリミティブを
数千万状態 (2 スレッドで 6,653 万) でメモリ安全と証明し、裸のプリミティブが livelock-free でないことを意図的に示す。
Layer 2 は 2/3 レベル木の多段 bundle/unbundle STM プロトコルを、静的・動的の両方で safety かつ livelock-free と証明し、
Lamport クロック優先度調停で 11.5 億状態超まで検証する。さらに hard-link 系 7 topology/パターン変種が
本番 race「30/30 abort」を 再現・修正する。最後に C++ ストレステスト 7 本 (~2,700 万反復、4-8 スレッド)
が実装を実機で走らせ、抽象モデルでは捉えられないコンパイラ・レイアウト・タイミング依存バグを検出する。
結論: プロトコルは数学的に保証され、実装は経験的に堅牢化されており、両者の間に隙間はない。
本俯瞰スライドは各層の詳細デッキへのハブです。下のスライドのリンクから個別デッキへ移動できます。
正本データ: kamestm/tests/VERIFICATION.md /
doc/verification_log.md /
doc/proof_semantics.md。
| 層 | 仕様 / テスト | ツール | 検証対象 | 最大検証規模 | 結果 | デッキ |
|---|---|---|---|---|---|---|
| L0 | cds_test_*.c (10)tlaplus/test_*.c (15; 6 は hardlink) |
GenMC v0.17 (RC11) |
タグ付きポインタ参照カウント、memory_order 安全性 (弱メモリ) | multi_cas: 464,164 完了 + 705,296 blocked (~270s) | 全 Pass | —（VERIFICATION.md §1） |
| L1 | atomic_shared_ptr.tla |
TLC | atomic_shared_ptr + commit プリミティブ (drain release, scoped_atomic_view)、10 safety 不変条件 | 66,537,058 / depth 84 / 1h30m (2t full) | Pass liveness 意図的 FAIL |
slides_layer1.html |
| L2 | BundleUnbundle_2level_LLfree.tla |
TLC | 2-level bundle/unbundle + LL-free priority gating | 137,333,348 (3t confC live, 2h 57min) 127,586,599 (MaxCommits=2, 4:40) |
Pass + liveness | slides_layer2_LLfree.html |
| L2 | BundleUnbundle_2level_LLfree_dynamic.tla |
TLC | ↑ + オンライン insert/release | 413,884,516 (release superfine live, 7:13) | Pass + liveness | slides_layer2_LLfree_dynamic.html |
| L2 | BundleUnbundle_3level_LLfree.tla |
TLC | 3-level 木、再帰的 inner bundle、多段 unbundle walk | 1,154,807,632 (3t confC safety, 4:09) 640,894,951 (confC live, 15:25) |
Pass (+ liveness on live cfg) | slides_layer2_LLfree_3level.html |
| L2 | BundleUnbundle_3level_LLfree_dynamic.tla |
TLC | 3-level + オンライン insert/release | 921,351,233 (release superfine, 3h24m, safety) 6.8M (coarse 2t live) |
Pass | slides_layer2_LLfree_dynamic.html |
| HL | BundleUnbundle_hardlink_*.tla (7; 条件付き nested_external 含む) |
TLC | 2-親/1-子 hard-link 6 topology、Phase 4 reachability gate、per-action fairness | self_collision FAIL→114、4node FAIL→531、external_migration 3t 1,202 | Pass + liveness (修正後) |
slides_hardlink.html |
| PF | パラメータ化正当性 ( doc/parameterized_cutoff.md) |
TLC + 手証明 | 有界 TLC を ∀ へ持ち上げ: 木軸=構造カットオフ定理、スレッド軸=σ-飽和、活性=∀N ranking | cutoff H=3/N=2、σ=6 が T=2≡T=3 で飽和（superfine 137M 全状態で確認） | 木: 定理 / スレッド: 予想 / 活性: ∀N | slides_parameterized.html |
| RT | C++ 7 tests (tests/) |
C++ 実機 | 実装の高競合ストレス: lifecycle balance、snapshot 整合性、starvation-freedom 経験的 | negotiation 6t (2 slow + 4 fast × 5M)、~27M iter 合計 | 全 Pass | —（VERIFICATION.md §6） |
最大規模ハイライト: 全検証中の最大状態空間は 1,154,807,632 状態 (3-level static confC, safety-only, ohtaka 4:09)。safety+liveness 込みの最大は 640,894,951 (3-level confC live, 15:25)。（これらは spec バージョン依存のピーク値；生の状態数は spec 進化で変動し、現行 spec は confC ≈ 540,782,047 に再基準化 — バージョン跨ぎ比較は無意味、VERIFICATION.md §3–§4 参照。）動的仕様の最大は 921,351,233 (3L-dyn release superfine, 3h24m)。 いずれも CONSTRAINT なし完全 exhaustion。
タグ付きポインタ参照カウント、drain release、scoped_atomic_view RAII、10 不変条件、liveness 意図的違反。
STM の中核プロトコル仕様。bundle/unbundle + commit の木構造・段階の基本解説。
priority-TID negotiate、CanProceed / TagAfterFail / PreemptTag / ClearMyTags、CONSTRAINT なし構造的 LL-free 証明。
slides_layer2_LLfree_3level.html →
Grand→Parent→Child、再帰的 inner bundle (InnerPhase2/3/4)、多段 unbundle walk。
slides_layer2_LLfree_dynamic.html →
オンライン insert(online=true) / release、thread role 構成、413M state 検証。
有界 TLC を「∀ 木形・全スレッド」へ持ち上げる議論。構造カットオフ定理（catamorphism）、σ-飽和（T=2≡T=3）、oldest-tag ranking による ∀N 活性、spec-version provenance。
5 topology + 非アトミック、本番 race 再現・修正、per-action fairness 初導入、Phase 4 reachability gate。
25 プログラム (cds_test_*.c 10 + test_*.c 15; 後者の 6 は hardlink プロトコルテスト)、弱メモリモデル下の参照カウント安全性。スライド未作成（生データのみ）。
英語版: 同一構成の英語デッキが ../doc/ にあります（slides_layer1_en.html,
slides_layer2_en.html, slides_layer2_LLfree.html,
slides_layer2_LLfree_3level_en.html, slides_layer2_LLfree_dynamic_en.html,
slides_hardlink_en.html）。英語俯瞰図: ../doc/slides_overview_en.html。
| 性質 | C++ ストレス | GenMC (L0) | TLA+ (L1/L2) |
|---|---|---|---|
| メモリ順序の正しさ | 確率的 (timing 依存) | 網羅 (RC11) | N/A (逐次一貫) |
| プロトコル論理 (refcount/drain/scope) | 確率的 | assertion ベース | 網羅 (L1) |
| STM commit 整合性 | gn2 ≤ gn3 不変条件 | N/A | 網羅 (L1+L2) |
| bundle/unbundle プロトコル | STM テスト経由 (暗黙) | N/A | 網羅 (L2、最大 1.15B states) |
| livelock-freedom | 非対称ストレス | N/A | 網羅 (L2; L1 は反例) |
| fairness / starvation | transaction_negotiation_test | N/A | hard-link で per-action WF モデル化 |
| 実コンパイラ/実機バグ | Yes (実バイナリ) | No (抽象) | No (抽象) |
※ VERIFICATION.md §6 の相補性表は「622M states」と古い値を記載。spec バージョン跨ぎのピークは 1,154,807,632 (3L static confC, spec 8d6026e3) — 現行 spec は confC ≈ 540,782,047 (924b6e63) に再基準化。生の状態数は spec バージョン依存。
| 仕様 | 位置づけ |
|---|---|
BundleUnbundle.tla (3-level)BundleUnbundle_2level.tla | アーカイブされたベースライン仕様 (参考用)。機能は現行 LLfree スイートでカバー済。検証は pass するが日常実行しない。 |
MC.tla / MC_2level.tla / MC_3level.tla | 旧スタイルの model-checker config モジュール。現在は *_mc.cfg を直接使用。 |
test_stm_commit.c / test_bundle_2level.c / test_bundle_3level.c | アーカイブされた TLA+-derived C11 テスト (参考用)。機能は現行 LLfree スイートでカバー済。 |