Hard-link 系 TLA+ 検証 — 概要

5 つの topology + 非アトミックテストパターン + per-action fairness

5 つの topology + 非アトミック版

Self-collision (R-A-C) — bug repro + fix

BundleUnbundle_hardlink_self_collision.tla

Topology

バグサーフェス (本番 trace からの再現)

提案される修正 (TLA+ で確認)

// bundle() Phase 3 — pseudo-diff
for (child in subnodes) {
    if (local.subpackets[child] == nullptr) continue;  // ← NEW
    // existing CAS to BundledRef(this)
}

Hard-link 参照 (=「parent.sub[c] = Null は packet が他所にある印」) は Phase 3 で CAS-tag しない。修正後、bundle はパケットを消失させずに完了する。

検証結果

4-node — production race repro

BundleUnbundle_hardlink_4node.tla (gold standard)

Topology

race パターン

T2 が ❶ と ❷ の間で停止した瞬間、Root の Phase 4 が走ると C が どちらの親の sub[] にも届かない状態 (production race)。

修正 = C++ Phase 4 reachability gate

// transaction_impl.h Phase 4 (commits 87892b35, 92b15f62, 404fa137, b12e1895)
newpacket->m_missing = false;             // 先にクリア (mid-bundle 短絡を回避)
if (! newpacket->allSubReachable(...)) {
    newpacket->m_missing = true;          // 戻す
    return BundledStatus::DISTURBED;     // outer snapshot() retry
}

検証結果

External / External migration — cross-tree races

External (_hardlink_external.tla)

bundle(GN1) が GN1 を ~missing finalise する瞬間に GN2.sub[P2] = Null が GN1 から reverseLookup できない → SnapshotConsistency 違反。Phase 4 reachability gate が直接これを防ぐ。

External migration (_hardlink_external_migration.tla)

↑ 同じ topology だが、bundle が P2 を P1 の tree から GN2.sub[P2] に atomic に migrate する。bundle pipeline の各 step を peer thread が P1 上で race する状況を full モデル化。

Per-action fairness — KAME corpus 初導入

_hardlink_4node / _hardlink_external_migration

典型的な spec 書き方

\* 4-node:
Spec == Init /\ [][Next]_vars
        /\ WF_vars(NextStep)
        /\ \A t \in Threads : WF_vars(MigrateCToA(t))

\* external_migration: あらゆる progress step に WF を付与
Spec == Init /\ [][Next]_vars
        /\ WF_vars(NextStep)
        /\ \A t \in Threads :
            /\ WF_vars(BundlePhase1(t))
            /\ WF_vars(BundlePullP1(t))
            /\ WF_vars(BundleCASP2(t))
            /\ WF_vars(BundleUpdateGN1(t))
            /\ WF_vars(BundlePhase4(t))
            /\ WF_vars(BundlePhase5(t))

blanket WF_vars(NextStep) が弱すぎる理由

"older-wins" がこの fairness を吸収しないのはなぜか

非アトミックテストパターン

BundleUnbundle_hardlink_nonatomic.tla

動機

リモートブランチ claude/refactor-negotiate-scoped-f7de2 commit b23fa954 が 復元したテストパターン — 非 Tx p1->insert(p2) / release(p2) を Tx 操作と交互に走らせる — が master で本物の活性ギャップを露呈しているのか、 それともスケジューラアーティファクトか、を判定する。

モデル化

2 つの finalize variants (CONSTANT UseFixVariant)

検証結果 (全 4 構成)

Dynamic (sibling parents) + 他の topology との関係

BundleUnbundle_hardlink_dynamic.tla

Topology

カバー範囲

最も 基本的な hard-link 構造: 兄弟の 2 親が同じ子を共有する。 一方の親の bundle が他方の親の sub[] から DynChild1 を pull すべきタイミングで peer thread と race する migration race を網羅。

検証結果

State-space bounding policy (全 hardlink 共通)

共通の不変条件 + Phase 4 gate と他モデルへの影響

検証対象の不変条件 / property

Phase 4 reachability gate の C++ 側コミット履歴

non-hard-link モデルへの影響: なし

C++ 側 implementation の影響

まとめ + 参考資料

意義

参考資料

• kamestm/tests/VERIFICATION.md §5 — full results + per-cfg runs
• kamestm/tests/tlaplus/doc/verification_log.md — run log
• kamestm/tests/tlaplus/BundleUnbundle_hardlink_*.tla — spec 本体 (6 ファイル)
• slides_layer2_LLfree.html — base spec の説明 (LL-free Gen 3)