3-level LL-free (Gen 3) — diff from 2-level

`BundleUnbundle_3level_LLfree.tla`

This deck builds on slides_layer2_LLfree.html (2-level LL-free). The 3-level spec inherits the privilege-TID mechanism unchanged and adds one level of tree depth: Grand → Parent → {Child1, Child2}.

Priority gating (CanProceed / TagAfterFail / TagAfterSuccess / PreemptTag / ClearMyTags) and the EventuallyAllDone liveness property are identical — see the 2-level deck.

Tree

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

Additional coverage vs the 2-level spec

Item	2-level	3-level (this spec)
commit root	`CommitParent`	`CommitGrand` (Grand scope: +1 on all grandchild payloads)
recursive bundle	(none)	`InnerPhase2`/`3`/`4`: `snapshot(Grand)` bundles Parent inside
unbundle walk	1 hop (`UnbundleCASAncestors`)	2 hops (`UnbundleCASLoop`): Child → Parent → Grand
chain navigation	(trivial)	`WalkUpChain` / `SnapshotForUnbundle` walk `bundledBy` upward
new invariants	—	`BundleChainValid` / `BundledByCorrect` / `GrandAlwaysPriority`

Recursive inner bundle

`InnerPhase2` / `InnerPhase3` / `InnerPhase4`

When snapshot(Grand) encounters Parent with missing=TRUE, it triggers an inner bundle of Parent (recursive bundling). The 4-phase protocol body is identical to the outer bundle, but the inner pass is modelled as separate actions (InnerPhase2/3/4) to control state-space forking.

InnerPhase structure (superfine splits phases; fine folds into `BundlePhase1`)

InnerPhase2(t) ==
    \* CAS Parent to missing=TRUE wrapper
    /\ CanProceed(t, Parent)         \* ★ priority gate
    /\ LET newW == PriorityWrapper(MakePacket(Parent, _, _, TRUE), ser)
       IN linkage' = [linkage EXCEPT ![Parent] = newW]

InnerPhase3(t) ==
    \* CAS every Child to BundledRefWrapper(Parent, ser)
    /\ \A c \in {Child1, Child2} : CanProceed(t, c)
    /\ ...

InnerPhase4(t) ==
    \* Final CAS: Parent to missing=FALSE
    /\ CanProceed(t, Parent)
    /\ ...

InnerPhase restart history: Subtle bugs found and fixed during spec development (commit history):

1d9820bc: InnerPhase3 restart with stale subpackets caused lost increments
8d6026e3: InnerPhase4 restart failed to clear outer bundle state
73bcef3a: InnerPhase2 restart fix

All these were model-only issues — the corresponding C++ paths were already correct. TLA+ modelling at finer granularity surfaced them.

Multi-level unbundle walk

`UnbundleWalk` + `UnbundleCASLoop` + `UnbundleCASChild`

If a Child is bundled two levels deep (Child → Parent → Grand), committing that child requires marking both ancestors on the bundledBy chain as missing=TRUE before restoring the child to priority.

Step 1: UnbundleWalk — build the chain

UnbundleWalk(t) ==
    \* Walk from child upward via bundledBy and build casTargets
    \* casTargets = <<Grand, Parent>>  (root-first)
    /\ local' = [local EXCEPT ![t].casTargets = chain]
    \* superfine #5: 3-level uses root-first order (matches C++ traversal)

Step 2: UnbundleCASLoop — mark each ancestor missing=TRUE

UnbundleCASLoop(t) ==
    \* For each ancestor in casTargets, CAS its wrapper to a missing=TRUE PriorityWrapper
    \* sub[c] is preserved (Phase 3 rollback / recovery still uses it; not nulled)
    /\ CanProceed(t, anc)
    /\ LET newW == PriorityWrapper(MakePacket(anc, _, anc.sub, TRUE), ser)
       IN linkage' = [linkage EXCEPT ![anc] = newW]
    \* coarse: all ancestors in one step; fine: per-ancestor step

Step 3: UnbundleCASChild — restore Child to priority with new payload

UnbundleCASChild(t) ==
    /\ LET newChildW == PriorityWrapper(newpacket, ser)
       IN linkage' = [linkage EXCEPT ![node] = newChildW]

Added invariants

Invariant	Meaning
`BundleChainValid`	A bundled node's `bundledBy` target is either priority or itself bundled
`BundledByCorrect`	`bundledBy` always points to the structural parent
`GrandAlwaysPriority`	The root (Grand) always has priority

Verification results + related specs

3-level LL-free results

cfg	Threads	States	Depth	Time	Result
1-thread superfine	1	(small)	—	<1s	✅ Pass (sanity)
2-thread coarse	2	1,497,098	98	1:35	✅ Pass + liveness
2-thread superfine	2	14,109,731	148	19:13	✅ Pass + liveness
3-thread superfine confC (all-root)	3	640,894,951	88	15:25	✅ Pass + liveness (ohtaka)

What this proves: All interleavings of 3 threads concurrently running snapshot / commit / bundle / unbundle in a 3-level tree preserve both safety and liveness. LL-free priority gating structurally finitizes the state space even with depth-2 bundle/unbundle chaining. Details: kamestm/tests/VERIFICATION.md §4.

Related specs / decks

BundleUnbundle_2level_LLfree.tla + slides_layer2_LLfree.html — base spec (Gen 3 LLfree)
BundleUnbundle_3level_LLfree_dynamic.tla + slides_layer2_LLfree_dynamic_en.html — online insert/release extension
BundleUnbundle_hardlink_*.tla + slides_hardlink_en.html — hard-link topologies

Running larger configs

# 1-thread sanity (< 1 s)
java -XX:+UseParallelGC -Xmx8g -cp tla2tools.jar tlc2.TLC \
  -workers auto -config BundleUnbundle_3level_LLfree_1thr_superfine_mc.cfg \
  BundleUnbundle_3level_LLfree.tla

# 2-thread coarse with liveness (~2 min)
java -XX:+UseParallelGC -Xmx14g -cp tla2tools.jar tlc2.TLC \
  -workers auto -config BundleUnbundle_3level_LLfree_coarse_mc.cfg \
  BundleUnbundle_3level_LLfree.tla

3-thread superfine etc. require ohtaka. See doc/ohtaka_handoff.md.