Layer 2: Bundle/Unbundle + Commit

TLA+ Model — 2-level / 3-level bundle/unbundle protocol (LLfree premise: `BundleUnbundle_2level_LLfree.tla` / `BundleUnbundle_3level_LLfree.tla`)

This deck covers the bundle/unbundle/commit protocol itself (LLfree assumed). The hard-link, dynamic, and 3-level topics are covered in separate decks.

The most complex model. Integrated verification of 4-phase bundle, multi-level unbundle, and optimistic commit on 2-level and 3-level trees. The single-node CAS commit from the old "Layer 1 (stm_commit)" is now subsumed into this layer's CommitTryCAS direct path (2-layer architecture).

Model supports 3 fidelity tiers (coarse / fine / superfine — see next slide).

Tree Structure (Fixed)

    Grand
     └── Parent
         ├── Child1
         └── Child2

Data Structures

(* Packet: payload + child packets + missing flag *)
MakePacket(node, payload, sub, miss) ==
    [payload |-> payload, sub |-> sub, missing |-> miss, node |-> node]

(* PacketWrapper: priority (independent) or bundled (absorbed by parent) *)
PriorityWrapper(packet, ser) ==
    [packet |-> packet, hasPriority |-> TRUE, bundledBy |-> Null, serial |-> ser]

BundledRefWrapper(parentNode, ser) ==
    [packet |-> Null, hasPriority |-> FALSE, bundledBy |-> parentNode, serial |-> ser]

Variables (9)

VARIABLES
    serial,        \* per-thread Lamport serial (monotone Nat)
    linkage,       \* linkage[n]: PacketWrapper for each node
    pc, op, target, local,  \* per-thread state
    iterBudget,    \* per-thread remaining full iterations
    childQueue,    \* per-thread children pending CommitChild
    priorityTag    \* per-node LL-free negotiate tag (Null | <<iter, tid>>)

LLfree has no globalSerial (the C++ has no such variable); the serial is a Lamport monotone Nat.

3-Tier Fidelity Model (coarse / fine / superfine)

This layer's TLA+ spec can verify the same invariants at different granularities. Granularity is selected via constant flags in the .cfg file. Finer modes increase state count but also raise fidelity to the C++ implementation.

Mode	Characteristics	Use case
coarse	Phases collapsed into single atomic steps (fastest). May miss some interleavings, but high-level invariants are still verifiable.	Smoke tests on large models (3-level, 3-thread, etc.)
fine	Per-child CAS with separate failure paths. Phase3 rollback is omitted (matching C++).	Standard exhaustive verification
superfine	Five C++-faithful optimization paths enabled: #1 pre-bundle serial CAS, #2 inner-bundle phase split, #4 Phase3 DISTURBED check, #5 root-first unbundle ordering, #6 same-child retry	Strict correspondence with C++

An example of a bug introduced during TLA+ modeling: BundlePhase3's allDone check was only testing ~hasPriority, so it incorrectly counted children already bundled by another thread as "done." Fixed by matching against BundledRefWrapper(node, ser) for the current thread. The C++ implementation runs CAS on every child without a "skip if already bundled" optimization, so it never exhibited this bug — it was a TLA+ model-only issue.

TLA+ Notation (See Layer 1)

For basic TLA+ notation, refer to the beginning of the Layer 1 slides (slides_layer1_en.html).
New notation introduced in these slides:

Notation	Meaning
`MakePacket(node, payload, sub, miss)`	Record construction function. Returns `[payload \|-> ..., sub \|-> ..., missing \|-> ..., node \|-> ...]`.
`PriorityWrapper(packet, ser)`	PacketWrapper record. `hasPriority=TRUE`.
`BundledRefWrapper(parentNode, ser)`	Wrapper in bundled state. `hasPriority=FALSE, bundledBy=parentNode`.
`[n \in AllNodes \|-> IF ... THEN ... ELSE ...]`	Conditional function definition. Sets different initial values per node.
`r.field`	Record field access. Examples: `w.hasPriority`, `w.packet.sub[c]`
`serial` comparison	The serial is a Lamport monotone Nat. LLfree does not finitize via modular wrapping — finiteness is structural (the priorityTag mechanism). The order comparison is a fixed-width signed difference: C++ `isOlderThan` (unsigned subtraction → signed reinterpretation), generated C11 `ser_gt`.

Characteristics of this model: The variable local has a nested record structure (local[t].wrapper.packet.sub[c], etc.). This corresponds to nested structs in C++. In TLA+, nested fields are updated with [local EXCEPT ![t].wrapper = w].

Bundle: 4-Phase CAS Protocol

Phase 1: Collect — Gather child packets

BundlePhase1(t) ==
    /\ LET childPkts == [c \in children |->
           IF childWs[c].hasPriority /\ ~childWs[c].packet.missing
           THEN childWs[c].packet     \* child is complete → acquire
           ELSE IF childWs[c].bundledBy = node
           THEN parentW.packet.sub[c]  \* already bundled → use existing
           ELSE Null]                  \* cannot acquire → restart
       IN
       IF allCollected
       THEN pc' → "bundle_phase2"
       ELSE pc' → "snap_read"  \* restart (2-level; 3-level uses "snap_check")

Phase 2: CAS Parent — New PacketWrapper (missing=TRUE)

BundlePhase2(t) ==
    /\ LET newPkt == MakePacket(node, payload, subs, TRUE)
           newW   == PriorityWrapper(newPkt, ser)
       IN
       IF linkage[node] = oldW    \* CAS: if unchanged
       THEN linkage' = [linkage EXCEPT ![node] = newW]

Phase 3: CAS Children — Replace with BundledRefWrapper

BundlePhase3(t) ==
    /\ IF allMatch   \* all children match expected values
       THEN linkage' = [n \in AllNodes |->
           IF n \in children
           THEN BundledRefWrapper(node, ser)  \* child → back-reference to parent
           ELSE linkage[n]]

Phase 4: Finalize — missing=FALSE

BundlePhase4(t) ==
    /\ LET finalPkt == MakePacket(node, payload, sub, FALSE)  \* ← FALSE!
       IN
       IF linkage[node] = oldW
       THEN linkage' = [linkage EXCEPT ![node] = finalW]
            \* → consistent snapshot is now possible

Unbundle: Disassembly at Commit Time

Why Is It Needed?

To commit to a bundled child node, the ancestor bundle chain must first be disassembled. Starting from the target child, we follow bundledBy upward to identify the ancestors, set each ancestor's missing to TRUE, and then restore the child to a priority wrapper.

Step 1: UnbundleWalk — Build ancestor list

UnbundleWalk(t) ==
    \* Starting from the target child, walk the bundledBy chain upward
    \* and build the list casTargets of ancestor nodes to CAS
    \* (child → parent → (at 3-level) grand)
    /\ local' = [local EXCEPT ![t].casTargets = chain]
    \* superfine #5: at 3-level, build the list root-first
    \* (matching the C++ traversal order: CAS from root → leaf)

Step 2: UnbundleCASAncestors / UnbundleCASLoop — Set missing=TRUE on ancestors

UnbundleCASAncestors(t)   \* 2-level (BundleUnbundle_2level_LLfree.tla)
UnbundleCASLoop(t)         \* 3-level (BundleUnbundle_3level_LLfree.tla)
    \* For each ancestor in casTargets, CAS its wrapper to a new wrapper
    \* with missing=TRUE. The child sub-slots sub[c] are KEPT (not nulled),
    \* so Phase-1 re-collection (bundledBy==node re-adoption) can still find the child packet.
    /\ LET newPkt == MakePacket(anc, anc.payload, anc.sub, TRUE)
           newW   == PriorityWrapper(newPkt, ser)
       IN linkage' = [linkage EXCEPT ![anc] = newW]
    \* coarse: all ancestors in one step; fine: one ancestor per step

Step 3: UnbundleCASChild — Restore target child to priority

UnbundleCASChild(t) ==
    \* Restore the target child from BundledRefWrapper to PriorityWrapper,
    \* carrying the new (committed) payload.
    /\ LET newChildW == PriorityWrapper(newpacket, ser)
       IN linkage' = [linkage EXCEPT ![node] = newChildW]

Unbundle flow (shared across depths):
(1) UnbundleWalk builds the ancestor list casTargets → (2) CAS each ancestor to missing=TRUE (child slots preserved) → (3) CAS the target child back to Priority with the new payload.
Important: ancestor sub[c] slots are not nulled out. The missing=TRUE flag alone signals "this subtree is temporarily not snapshottable," and keeping sub intact lets Phase-1 re-collection (the bundledBy==node re-adoption path) and the unbundle walk find the child packet — there is no Phase-3 rollback in C++.

superfine #5 (3-level only): casTargets is built in root-first order (grand → parent → child direction) and ancestor CAS also runs root-first, matching the C++ traversal. This faithfully reproduces the race cases against concurrent bundle/unbundle.

Commit: Direct Path and Parent/Grand-Scope Commit

Two Kinds of Commit

The model has two commit families:

Direct commit (child scope): the 3-step pipeline CommitRead → CommitTryCAS → CommitDone. Performs the ordinary +1 to a child payload, inserting an unbundle when the target is bundled.
Deep commit (parent / grand scope): CommitParent (2-level) / CommitGrand (3-level). Takes a snapshot at parent / grand scope and applies +1 to every child payload inside that scope. This stresses whether payload integrity is preserved through bundle/unbundle chains.

CommitParent (2-level) / CommitGrand (3-level)

CommitParent(t)   \* 2-level: parent-scope +1 propagated to every Child payload
CommitGrand(t)    \* 3-level: grand-scope +1 propagated to every Grandchild payload
    \* Single CAS against the parent / grand wrapper. Updates every payload inside
    \* sub[c] to (p + 1) — payload is a monotone Nat — and commits the whole scope in one action.
    \* Even bundled subtrees must see their internal payloads advance by +1.

Direct-commit pipeline (CommitRead → CommitTryCAS → CommitDone)

CommitRead(t) ==
    \* Reload linkage[node] immediately before attempting the CAS
    /\ local' = [local EXCEPT ![t].wrapper = linkage[target[t]]]

CommitTryCAS(t) ==
    IF linkage[node] = oldW
    THEN linkage' = [linkage EXCEPT ![node] = newW]   \* CAS success → commit_done
    ELSE IF linkage[node].hasPriority
    THEN
        IF linkage[node].packet.payload = oldW.packet.payload
        THEN \* ★ Single-node optimization: same payload → re-adopt new child and retry ★
             local' = [local EXCEPT ![t].wrapper = linkage[node], ...]
        ELSE \* True conflict → fail
    ELSE
        \* Bundled → transition to unbundle_walk
        pc' → "unbundle_walk"

CommitDone(t) ==
    \* Commit finalization: decrement iterBudget, pop next child from childQueue
    \* If the queue is empty, return to idle; if iterBudget=0 as well, move to terminal
    /\ iterBudget' = [iterBudget EXCEPT ![t] = @ - 1]

Lifecycle variables and terminal condition

iterBudget / childQueue / MaxCommits: each thread runs MaxCommits iterations. Each iteration consists of "one parent / grand-scope commit (CommitParent / CommitGrand) plus one direct commit per child (CommitRead / TryCAS / Done)." childQueue[t] holds the children still pending in the current iteration and iterBudget[t] the remaining iterations.

TerminalPayloadCheck: in the terminal state where all threads have iterBudget=0 and are idle, each direct child's payload must equal MaxCommits × (|RootThreads| + |LeafThreads|) (= 2 × MaxCommits × |Threads| when both roles cover all threads; payload is a monotone Nat, no modulo). This guarantees that both the deep (+1) and direct (+1) commit streams were applied correctly.

Single-node optimization: On CAS failure, if linkage[node].hasPriority is still true and the payload matches our expected value, treat it as "only the child slot was swapped by another thread," adopt the new child packet, and retry the CAS. This reduces wasted aborts.

Verified Invariants (3-level set; 5 items)

\* 1. If missing=FALSE then all child packets exist
SnapshotConsistency ==
    \A n \in InnerNodes :
        (w.hasPriority /\ ~w.packet.missing) =>
            (\A c \in ChildrenOf(n) : w.packet.sub[c] /= Null)

\* 2. Non-root nodes have priority OR bundledBy≠Null
NoPriorityLoss ==
    \A n \in AllNodes \ {Grand} :
        w.hasPriority \/ w.bundledBy /= Null

\* 3. bundledBy chains are valid (reach priority within 2 hops)
BundleChainValid ==
    \A n \in AllNodes \ {Grand} :
        (~w.hasPriority /\ w.bundledBy /= Null) =>
            pw.hasPriority \/ pw.bundledBy /= Null

\* 4. bundledBy always points to the structural parent
BundledByCorrect ==
    \A n \in AllNodes \ {Grand} :
        ~w.hasPriority => w.bundledBy = ParentOf(n)

\* 5. Root always has priority
GrandAlwaysPriority ==
    linkage[Grand].hasPriority

The five above are the 3-level set (the Grand node and bundledBy chains are 3-level-only). The 2-level spec verifies SnapshotConsistency, NoPriorityLoss, BundleRefConsistency, and MissingPropagation instead of INV3/4/5.

Verification Results (CONSTRAINT-free exhaustion)

Model	Fidelity	Threads	States	Depth	Time	Result
2-level LLfree	micro (fine)	2	867,696	89	~35s	✅ Pass + liveness
2-level LLfree	superfine	2	2,676,196	129	3:12	✅ Pass + liveness
2-level LLfree	superfine confC (all-root)	3	137,333,348	96	2h 57min	✅ Pass + liveness (ohtaka)
2-level LLfree	MaxCommits=2 superfine	2	127,586,599	311	4:40	✅ Pass (ohtaka)
2-level dynamic LLfree	release superfine live	2	413,884,516	320	7:13	✅ Pass + liveness (ohtaka)
3-level LLfree	coarse	2	1,497,098	98	1:35	✅ Pass + liveness
3-level LLfree	superfine	2	15,094,117	146	15m 11s	✅ Pass + liveness
3-level LLfree	superfine confC (all-root)	3	640,894,951	88	15:25	✅ Pass + liveness (ohtaka)

What is covered: Across all 2–3 thread interleavings of snapshot/commit/bundle/unbundle, all invariants are preserved — proven by TLC exhaustion. Coarse collapses phases into single steps (fastest); fine separates per-child CAS; superfine faithfully models the C++ optimization paths. LLfree finitizes the state space structurally via the priority-TID mechanism (no CONSTRAINT) so that safety + liveness (EventuallyAllDone) are verified at the same time.

Bug found in TLA+: In the fine granularity, BundlePhase3's allDone test was only checking ~hasPriority, so it incorrectly counted children already bundled by another thread as "done." Fixed by matching against BundledRefWrapper(node, ser) for the current thread. (The C++ implementation runs CAS on every child without a "skip if already bundled" optimization, so it never exhibited the bug.)

Phase 4 reachability gate (hard-link safeguard; no impact on this spec)

Commits 87892b35 / 92b15f62 / 404fa137 / b12e1895 added a reachability gate (Packet::allSubReachable) to bundle Phase 4: under is_bundle_root=true, before m_missing is cleared, every Null sub-slot must be reverseLookup-able from the global root, otherwise Phase 4 returns BundledStatus::DISTURBED and the outer snapshot() retries.

This 2-level / 3-level spec needs no update. In the standard non-hard-link topology, every child has exactly one parent, so any Null sub-slot encountered at Phase 4 is always reverseLookup-able. The existing SnapshotConsistency invariant — one of this spec's five — already captures the gate's precondition. The gate is only effectful in hard-link topologies, covered separately by the BundleUnbundle_hardlink_* family (see slides_hardlink_en.html).

Two-Layer Overview (Current Status)

Layer	Spec	What It Verifies	States (largest confirmed)
Layer 1	`atomic_shared_ptr.tla` + commit primitives	Tagged-pointer reference counting, drain release, `scoped_atomic_view`; safety only	66.5M (2-thread MaxOps=3 full)
Layer 2	`BundleUnbundle_2level_LLfree` `BundleUnbundle_3level_LLfree` + `_dynamic` specs	4-phase bundle / unbundle / commit + LL-free priority gating; safety + liveness	2L: 413M (dynamic release superfine) 3L: 640M (3-thread superfine confC)
Layer 2 (hard-link)	`BundleUnbundle_hardlink_*` (5 topologies)	Multi-parent / 1-child; Phase 4 reachability gate; bug repro + fix; per-action fairness	~1k–10k (small-scale, complete)

Why only 2 layers: The former "Layer 1 (stm_commit)" single-node CAS commit integrates naturally into Layer 2's CommitTryCAS direct path, so a separate layer was redundant. Verifying bundle/unbundle together with optimistic commit in the same spec improves coverage of interference patterns.

LLfree priority mechanism: the Layer 2 spec introduces priorityTag + PreemptTag + ClearMyTags to structure older-wins arbitration, letting TLC exhaust without CONSTRAINT and structurally prove liveness (details: doc/proof_semantics.md).

Related Decks

Layer 2 LLfree (2-level) — slides_layer2_LLfree.html (the LLfree priority mechanism + verification)
Hard-link family — slides_hardlink_en.html (5 topologies + Phase 4 reachability gate)
3-level / dynamic LLfree — slides_layer2_LLfree_3level_en.html / slides_layer2_LLfree_dynamic_en.html

C++ ↔ TLA+ ↔ Generated C11 Correspondence Table

Variable Mapping

TLA+ Variable	C++ (transaction_impl.h)	Generated C11 (test_bundle_3level_LLfree.c)
`linkage[n]`	`atomic_shared_ptr<PacketWrapper> n->m_link`	`_Atomic(uint64_t) linkage[4]` 64-bit packed (Wrapper struct)
`linkage[n].hasPriority`	`PacketWrapper::hasPriority()`	`Wrapper.has_priority` (bit field)
`linkage[n].bundledBy`	`PacketWrapper::bundledBy()`	`Wrapper.bundled_by`
`linkage[n].packet.payload`	`Packet::payload()`	immutable slot `pkt_pack(payload,…)` via `Wrapper.packet_slot`
`linkage[n].packet.sub[c]`	`Packet::subpackets()[i]`	`pkt_pack(…, s0, s1, …)` sub-slots (via `packet_slot`)
`serial[t]`	`SerialGenerator` (Lamport clock)	`uint32_t thread_ser` (local)
serial comparison (Lamport, no modular wrap)	`isOlderThan` unsigned subtraction → signed reinterpretation	`ser_gt(a,b)`: `(a-b)&MASK, diff < MOD/2`

Action Mapping

TLA+ Action	C++ Code	Generated C11 Function
`SnapRead` + `SnapCheck` (3-level uses only `SnapCheck`)	`snapshot()` transaction_impl.h:2038/2053	`snapshot_grand()` `load_w()` → priority/missing decision
`BundlePhase1`–`4`	`bundle()` transaction_impl.h:2355	Within `snapshot_grand()` collect → CAS parent → CAS children → finalize
`InnerPhase2`/`3`/`4` (3-level only)	Inner-bundle portion of `bundle()` transaction_impl.h:2355	Within `snapshot_grand()` Inner bundle on Parent when Grand bundles (explicit in superfine; collapsed into `BundlePhase1` in fine)
`CommitParent` (2-level) `CommitGrand` (3-level)	Parent / grand-scope `commit()` transaction_impl.h:2757	`commit_parent()` / `commit_grand()` Deep commit: +1 to every child payload in the scope
`CommitRead`	Reload just before CAS in `commit()` transaction_impl.h:2757	Within `commit_child()` `load_w` immediately before the CAS attempt
`CommitTryCAS`	`commit()` transaction_impl.h:2757	`commit_child()` Direct CAS + single-node optimization
`CommitDone`	Finalization tail of `commit()` transaction_impl.h:2757	Tail of `commit_child()` Decrement `iterBudget`, advance to next child or idle
`UnbundleWalk`	`reverseLookup()` transaction_impl.h:1590/1665/1675	Within `commit_child()` Walk `bundledBy` chain to build casTargets (superfine #5 is root-first)
`UnbundleCASAncestors` (2-level) `UnbundleCASLoop` (3-level)	`unbundle()` transaction_impl.h:2904	Within `commit_child()` `cas_w(anc, ... missing=TRUE)` per ancestor. Child sub-slots kept (not nulled)
`UnbundleCASChild`	`unbundle()` transaction_impl.h:2904	Within `commit_child()` child → priority restoration with new payload

Layer 2 characteristics: In the generated C11, all node linkage is packed into 64 bits, and all fields are atomically updated with a single atomic_compare_exchange. This is faithful to the "1 action = 1 step" principle of TLA+.