Layer 2: LL-free 仕様

STM bundle/unbundle プロトコルの livelock-free 化 — 形式証明つき

記法と中核要素

BundleUnbundle_2level_LLfree.tla は privileged-TID negotiate 機構を備えた 2-level 仕様。 livelock-freeness を TLC で 形式的に 検証可能にすることが目的。 bundle/unbundle のツリー構造・プロトコル詳細は slides_layer2.html も参照。

新規追加 — variables, operators, actions, properties

有限性まわりの構成

Overview: 仕様と検証結果

LLfree は CONSTRAINT なしで完全 exhaustion できることが livelock-free 性の構造的証明となる。ツリー構造・プロトコル本体に priority 機構 (priorityTag) を載せた構成を確認する。

ツリー構造

2-level tree。bundle/unbundle protocol 本体・4-phase / commit pipeline / coarse-fine-superfine 三段構成に加え、LLfree は livelock-free 性を保証する gating 層を持つ。

モジュールヘッダ (引用)

\* Variant of BundleUnbundle_2level that mirrors KAME's livelock-free
\* negotiate mechanism explicitly so TLC's exhaustive search reaches a
\* finite state space without modular-serial wraparound.
\*
\* Key differences from the base 2level spec:
\*   - Lamport serial (TID encoded in lower digit, counter in upper).
\*     No globalSerial — C++ has none. No MaxSerial constant.
\*   - New variable priorityTag[n]: per-node (Null | <<iter, tid>>) tag.
\*   - Set by a thread when its CAS fails at a "negotiate point";
\*     others see the tag and only proceed if it's Null or matches mine.
\*   - Older transactions (smaller iter, then smaller tid) win.
\*   - Tag cleared at Transaction boundaries via ClearMyTags —
\*     mirroring C++ drop_tags_n_privilege() (per-linkage default).

TLC verification の結果

superfine 構成でも完走

BundleUnbundle_2level_LLfree_superfine_mc.cfg (Phase 1 prestamp CAS + Phase 3 DISTURBED 検出) でも同様に完走。C++ の最も忠実なミラーが動作することを示す。

priorityTag 変数と補助オペレータ

LLfree が導入する唯一の新変数 priorityTag[n] と、それを操作する補助オペレータ。 これらは C++ の per-linkage Linkage::m_transaction_started_time / tag_as_contender() を per-iteration 粒度でミラーする （iter は work-done カウンタで C++ の µs スタンプそのものではない＝健全な粗視化であり順序同型ではない）。

変数宣言と Init

VARIABLES
    serial, linkage, pc, op, target, local,
    iterBudget, childQueue,
    priorityTag   \* [Nodes -> Null | <>]

\* globalSerial は廃止 (C++ に対応物なし)。serial は Lamport 方式。
vars == <<serial, linkage, pc, op, target, local,
         iterBudget, childQueue, priorityTag>>

\* Serial encoding: EncodeSerial(cnt, tid) = cnt * SerialBase + tid
\*   SerialBase = 1 + |Threads|  (> max TID)
Init ==
    /\ ...  \* ツリー / linkage / pc の初期化
    /\ serial = [t \in Threads |-> EncodeSerial(0, t)]  \* TID 埋め込み
    /\ priorityTag = [n \in Nodes |-> Null]

派生量と補助オペレータ

\* iter(t): 完了したフル iteration 数。t と組み合わせて
\* <> の全順序を作る (smaller = older = 優先)。
iter(t) == MaxCommits - iterBudget[t]

MyTag(t) == <<iter(t), t>>

\* a が b より older。(iter, tid) の lex 順序で a が小。
TagOlder(a, b) ==
    \/ a[1] < b[1]
    \/ (a[1] = b[1] /\ a[2] < b[2])

\* Lamport serial helpers (C++ SerialGenerator, transaction.h:816-844 に対応)
SerialBase == 1 + Cardinality(Threads)
SerialCounter(s) == s \div SerialBase
SerialTID(s)     == s % SerialBase
EncodeSerial(cnt, tid) == cnt * SerialBase + tid

各オペレータの意味と C++ 対応

iter(t) が 派生量 である理由

なぜ Threads は Nat でなければならないか

状態空間への寄与

現行 spec では micro cfg 全体での distinct states は 867,696（depth 89）。 （初版 a35c4310 時点は 665,218 — proof_semantics.md §1。同 depth で到達インターリーブが増加）。 priorityTag が掛け算で効くものの、retry 数を有界に保つことで他変数の爆発を抑え、 全体としては 有限 に収まる。

CanProceed(t, n) — CAS の前提条件

LLfree の中核 gate。すべての CAS 試行に CanProceed(t, n) /\ ... が前置され、 登録 tag が許可しなければ その thread は進めない。これが priority 機構の中心。

定義

\* CanProceed: gate for any CAS attempt at node n by thread t.
\* Matches C++ tag_as_contender(): a thread proceeds when:
\*   (a) no privileged tidstamp registered, OR
\*   (b) the registered tidstamp's tid is mine.
\* No zombie-tag check: tags are cleared only on commit success
\* (ClearMyTags), so inactive state is reached exclusively via success.
CanProceed(t, n) ==
    LET tag == priorityTag[n] IN
    \/ tag = Null
    \/ tag /= Null /\ tag[2] = t

2 つの disjunct

旧版にあった ~ActiveThread(tag[2]) (zombie tag 判定) は削除。 タグはコミット成功時にのみ解放されるため、非アクティブ状態は必ず成功経路を経る → stale tag が残ることはなく、このケースは不要。

適用箇所 (priority-gated CAS site)

proof_semantics.md §8: 8/8 priority-gated CAS site で C++ 1:1 対応検証済み。 spec 側の主な call site は以下 10 箇所:

典型的な CAS パターン

\* CommitParent を例に
CommitParent(t) ==
    /\ pc[t] = "commit_parent"
    /\ ...
    /\ CanProceed(t, Parent)                  \* ★ gate: tag が許可しない限り進めない
    /\ LET ser == GenSerial(t, pw.serial)    \* Lamport serial
       IN
       \/ \* CAS 成功
          /\ ...
          /\ priorityTag' = [priorityTag EXCEPT ![Parent] = TagAfterSuccess(t, Parent)]
          /\ ...
       \/ \* CAS 失敗
          /\ ...
          /\ priorityTag' = [priorityTag EXCEPT ![Parent] = TagAfterFail(t, Parent)]
          /\ ...

全アクションで CanProceed を前置し、CAS の成否分岐ごとに TagAfterSuccess / TagAfterFail で priorityTag を更新する。 これにより「進めない thread は登録だけして待つ」「進めた thread は tag を保持 (Transaction-scope persistence)」という C++ tag_as_contender() 動作を表現する。

「進めない」場合の挙動

TagAfterFail / TagAfterSuccess — タグ更新規則

CAS の成否ごとに priorityTag[n] をどう更新するかを定義する 2 つの関数。 失敗時は 4 段階のラダー、成功時は 不変 (Transaction-scope persistence)。

TagAfterFail(t, n) — CAS 失敗時のタグ更新

\* TagAfterFail(t, n): the value priorityTag[n] should hold after thread t's
\* CAS at n fails. Mirrors C++ tag_as_contender():
\*   - No tag (slot empty): register mine.
\*   - My own tag: refresh to current MyTag(t).
\*   - Other thread's tag, I'm older: overwrite with mine.
\*   - Other thread's tag, I'm younger: keep theirs (defer to older).
TagAfterFail(t, n) ==
    IF   priorityTag[n] = Null
    THEN MyTag(t)
    ELSE IF priorityTag[n][2] = t
         THEN MyTag(t)
         ELSE IF TagOlder(MyTag(t), priorityTag[n])
              THEN MyTag(t)
              ELSE priorityTag[n]

4 分岐のラダー

旧版にあった「holder が inactive (zombie)」ケースは削除。 タグはコミット成功時のみ解放され、非アクティブ = 必ず成功済み → zombie tag は存在しない。

TagAfterSuccess(t, n) — CAS 成功時の更新

\* TagAfterSuccess(t, n): on CAS success at n, KEEP the tag — Transaction-
\* scope persistence (the per-linkage Linkage::m_transaction_started_time slot
\* is released only on commit success via drop_tags_n_privilege, not at each
\* inner CAS). Per-CAS clearing allows a peer Transaction to race in between
\* CAS phases of the holding Transaction and force endless re-bundling. The
\* actual release happens at Transaction boundaries via ClearMyTags below.
TagAfterSuccess(t, n) == priorityTag[n]   \* ← 不変 (KEEP)

C++ per-linkage priority スロットとの対応

「自分より若い tag を上書きしない」の意味

PreemptTag アクション + ClearMyTags

LLfree が追加する独立アクション (CAS と並行) と Transaction-end での tag 一括解放。 これらが揃って初めて「古い thread が永久 lockout されない」性質が成立する。

PreemptTag(t, n) — 独立アクション

\* @c11_action PreemptTag(t, n):
\*   An older thread can replace a younger thread's tag at a node, allowing
\*   it to subsequently proceed via CanProceed. Mirrors the symmetric
\*   preempt-window inside C++ tag_as_contender() firing for an older
\*   Transaction. Without this action, a younger thread that grabbed the
\*   tag first could permanently lock out an older thread.
PreemptTag(t, n) ==
    /\ priorityTag[n] /= Null
    /\ priorityTag[n][2] /= t              \* not already mine
    /\ TagOlder(MyTag(t), priorityTag[n])
    /\ priorityTag' = [priorityTag EXCEPT ![n] = MyTag(t)]
    /\ UNCHANGED <<serial, linkage, pc, op, target,
                 local, iterBudget, childQueue>>

PreemptTag の 3 つの enabling 条件

旧版にあった ActiveThread(t) (自分が活性) と ActiveThread(holder) (holder が活性) の 2 条件は削除。 zombie tag が存在しないため「inactive holder → CanProceed 経路で進める」 という分岐が不要になった。

なぜ独立アクションが必要か

ClearMyTags(t) — Transaction-end での一括解放

\* ClearMyTags(t): release ALL of thread t's tags at every node. Called only
\* on commit SUCCESS (CommitParent success, CommitDone success) — matches
\* C++ finalizeCommitment → drop_tags_n_privilege. On failure, tags are
\* preserved across retries (C++ operator++ does not call drop_tags).
ClearMyTags(t) ==
    [n \in Nodes |->
        IF priorityTag[n] = Null
        THEN priorityTag[n]
        ELSE IF priorityTag[n][2] = t
             THEN Null
             ELSE priorityTag[n]]

呼び出し箇所 (コミット成功時のみ)

C++ 対応

EventuallyAllDone PROPERTY と構造的 LL-free 性

LLfree が形式検証で示すべきものは何か。proof_semantics.md §2 の論証チェーンが livelock-free 性の証明である理由を確認する。

Spec 全体の構造

\* AllDone: terminal condition — every thread has consumed its full
\* iteration budget and returned to idle.
AllDone == \A t \in Threads : pc[t] = "idle" /\ iterBudget[t] = 0

\* NextStep: every action that can make real progress.
NextStep ==
    \E t \in Threads :
        \/ SnapRead(t) \/ SnapCheck(t)
        \/ BundlePhase1(t) \/ ... \/ BundlePhase4(t)
        \/ CommitParent(t) \/ ... \/ CommitDone(t)
        \/ UnbundleWalk(t) \/ ... \/ UnbundleCASChild(t)
        \/ \E n \in Nodes : PreemptTag(t, n)   \* ★ tag preempt も progress

\* Terminating: self-loop at AllDone — deadlock detection を有効のまま
\* 真の deadlock を見逃さないためのイディオム (proof_semantics §6)
Terminating ==
    /\ AllDone
    /\ UNCHANGED vars

Next == NextStep \/ Terminating

Spec == Init /\ [][Next]_vars /\ WF_vars(NextStep)
                              \* ↑ Terminating は WF 外。さもなくば
                              \* "永遠にスタッターすればよい" になり
                              \* 活性が無意味化 (proof_semantics §6)

EventuallyAllDone PROPERTY

\* EventuallyAllDone: under WF, every execution eventually reaches AllDone.
\* This is the key LL-free property — if priority gating is correct, no
\* thread can be starved indefinitely, so all threads eventually finish.
EventuallyAllDone == <>AllDone

TLA+ の <>P は「P が いつか 真になる」(eventually)。WF_vars(NextStep) で「enabled な NextStep 遷移は永遠に無視されない」を仮定すれば、priority 機構が正しい限り 全スレッドが必ず AllDone に到達することを TLC が verify する。

論証チェーン (proof_semantics.md §2)

cfg 構成 (LLfree)

検証結果 (現状、2-level LLfree)

関連仕様

Privilege=FALSE 検証 + wait-free との区別

priority 機構が必須であることを示す Privilege=FALSE 検証 (proof_semantics §5)、 および「livelock-free」と「wait-free」の混同を防ぐ整理 (proof_semantics §7)。

Privilege=FALSE — priority 機構を無効化した場合

3-level spec (BundleUnbundle_3level_LLfree.tla) では Privilege が 明示的な CONSTANT として存在する。Privilege=FALSE に設定すると priority 機構が すべて無効化される。これは priority 機構が本質的に必要であることを検証するためのスイッチ であり、無効化すると状態空間が発散する。

Wait-free は別問題

形式検証で示せること・示せないこと