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 系 6 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 (9)tlaplus/test_*.c (9) |
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, 2:53) 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 (6) |
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 |
| 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)。動的仕様の最大は 921,351,233 (3L-dyn release superfine, 3h24m)。 いずれも CONSTRAINT なし完全 exhaustion。
タグ付きポインタ参照カウント、drain release、scoped_atomic_view RAII、10 不変条件、liveness 意図的違反。
bundle/unbundle + commit の基本解説。Gen 3 LLfree への導線。modular serial 系の歴史的記述。
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 検証。
5 topology + 非アトミック、本番 race 再現・修正、per-action fairness 初導入、Phase 4 reachability gate。
18 プログラム (cds_test_*.c 9 + test_*.c 9)、弱メモリモデル下の参照カウント安全性。スライド未作成（生データのみ）。
英語版: 同一構成の英語デッキが ../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」と古い値を記載。最新の最大は 1,154,807,632 (3L static confC)。
| 仕様 | 位置づけ |
|---|---|
BundleUnbundle.tla (3-level)BundleUnbundle_2level.tla | Gen 1/2 非 LL-free 版。LLfree (Gen 3) に置換済。modular serial / CONSTRAINT に依存。検証は pass するが baseline として保存。 |
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 | 非 LL-free path の TLA+-derived C11 テスト (legacy)。LLfree 版に置換。 |