TLC is exhaustive only for the finite instance it is given (a fixed thread count T,
a fixed tree of height H / width N, a fixed MaxCommits).
Enlarging the instance never reaches "∀T, ∀ tree" — it is an unbounded regress.
This deck captures the argument that lifts the finite TLC results toward a claim over the
unbounded family (source: doc/parameterized_cutoff.md).
| Axis | Reaches | Mechanism |
|---|---|---|
| Tree (height & width) | a theorem ∀ tree shape | structural cutoff (catamorphism reduction): reduce to H=3, N=2 → discharge exhaustively with TLC |
Thread T | ∀T as a strongly-evidenced conjecture (not a theorem) | identity-free safety + exhaustive to the contention bound + measured σ-saturation |
| Liveness (livelock-free) | a ranking argument ∀N | oldest-tag ranking function (no thread cutoff) + one remaining lemma |
How to read it: "∀ tree shape, all thread counts" means "proven for trees;
conjectured-with-strong-evidence for threads." Parameterized verification is undecidable in
general (Apt–Kozen 1986), so we do not claim an unmechanized ∀T theorem.
Every bundle and unbundle transition is a fold (catamorphism) over the tree.
(* bundle folds DOWNWARD over the subtree *)
bundle(n) = collect( linkage[n], { bundle(c) : c ∈ children(n) } )
(* unbundle folds UPWARD over the ancestor chain (priority root = base case) *)
unbundle(n) = extract( linkage[n], unbundle(parent(n)) ){linkage[n]} together with the fold result of the
immediate fold-neighbour(s) — children for bundle, the parent for unbundle. The combining
function is independent of the tree's height and of the number of children beyond the one
slot it indexes. Children enter only through symmetric aggregates ([c ↦ linkage[c]], ∀ c …)
and monotone "all-children-done" thresholds.
Key point: it is not that an action touches only two levels (it does not —
SnapshotForUnbundle reads the whole ancestor chain in one evaluation; an inner bundle reaches a
grandchild). It is that the cross-level access is a fold with a height-uniform local step —
a catamorphism — so the depth induction goes through without restructuring the algorithm.
| Action | linkage footprint | role |
|---|---|---|
BundlePhase1 (collect) | self + each immediate child (grandchildren only via the recursive inner-bundle of a non-leaf child) | bundle↓ |
BundlePhase3 (per-child CAS) | self + immediate children (one child / action) | bundle↓ |
UnbundleWalk / UnbundleCASLoop / UnbundleCASChild | self + immediate parent / one ancestor + root anchor / self + immediate parent | unbundle↑ |
BundlePhase2/4, CommitTryCAS, CommitGrand | self only (incl. root-anchor read) | local |
Every action's footprint ⊆ {self} ∪ {immediate fold-neighbours} ∪ {root anchor}. Obligation #1 discharged.
is_bundle_root ⇔ all children
bundled) is a monotone threshold over the child set. Hence every behaviour over N ≥ 2 children is
simulated by a 2-children behaviour, collapsing children 3..N onto child 2.
Two children already realise the three width-sensitive patterns: one done / one pending; two threads contending the same child; two threads on different children. A third only repeats them.
SnapshotConsistency, BundleChainValid, NoPriorityLoss,
GrandAlwaysPriority, MissingPropagation, TerminalPayloadCheck, …) hold on a tree
of arbitrary height H and arbitrary width N iff they hold
on the instance with H=3 (root + one internal node + leaves) and N=2 children.
H via Lemma 1. Node roles are only leaf / internal / root; H=3 instantiates all three and exercises both fold directions at the internal node. Any H≥4 adds only further applications of the same uniform step — no new role-interaction.N to 2.Consequence: the exhaustive H=3, N=2, superfine TLC runs constitute, for the tree axis,
a complete proof of the safety invariants on the unbounded family of trees — not merely the
instances checked: they are the base case of the cutoff, and Lemmas 1–2 lift them to all H, N.
T theorem + identity-free safetyWe do NOT claim a ∀T theorem (deliberate scope). Parameterized verification is
undecidable in general (Apt–Kozen 1986). A mechanized ∀T proof (a guided TLAPS
Spec(T) ⊑ Spec(3) simulation, or a separately-validated thread-free abstract CAS model) is future work.
Instead we support ∀T as a strongly-evidenced conjecture via three machine-checkable
ingredients: ① identity-free safety (this slide), ② exhaustive checking to the contention bound, ③ a measured
σ-saturation (next slide).
| A | Structural predicates. Every safety invariant (SnapshotConsistency, NoPriorityLoss, BundleChainValid, BundledByCorrect, GrandAlwaysPriority, MissingPropagation, TerminalPayloadCheck) is a predicate over the bundle-tree linkage (hasPriority/bundledBy/sub[·]/missing) and payload counts. It reads neither priorityTag nor serial — it never mentions a thread. |
| B | Per-node CAS serialization. linkage[n] is mutated only by a successful CAS → for any T its per-node history is a single serialized value-sequence. The gate only restricts which thread attempts a CAS (writes priorityTag, never linkage) → it cannot manufacture a safety violation. |
| C | Identity is only a uniquifier. Thread identity appears in the state only as the low-order uniquifier in the Lamport serial = counter·Base + tid. GenSerial makes counter dominate causal order; tid only tie-breaks causally-concurrent events (order-sensitive data-independence, Lazić 1999). |
⇒ Thread symmetry holds semantically (the safety state is invariant under any permutation of identities).
But it is not applicable as a TLC SYMMETRY reduction: TagOlder's tid-< (the Lamport tie-break)
forces Threads to be ordered naturals, whereas TLC SYMMETRY needs a model-value set —
mutually exclusive (TLC rejects SYMMETRY Permutations(Threads)). So the runs below are full, with no symmetry reduction.
And symmetry is permutation-only — it would never reduce the thread count (symmetry ≠ cutoff).
Measurement scope, stated explicitly: all the saturation measurements below are on the
2-level tree (Parent → {Child1, Child2}), MaxCommits=1, no symmetry (raw reachable sets).
The headline is the all-root workload (commit target = root, exposing the bundle-side structures);
the both-roles workload (with leaf commits) separately exposes the multi-level unbundle-side structures.
| Tree | Atomicity | Workload | T | Raw distinct states | Structural σ | Safety |
|---|---|---|---|---|---|---|
| 2-level | superfine | all-root | 2 | 124,244 | 6 | Pass |
| 2-level | superfine | all-root | 3 | 137,333,348 | 6 — set-identical to T=2 (diff empty; σ=6 across all 137 M) | Pass (ohtaka 5h08m + 736 GB dump) |
| 2-level | coarse | all-root | 4 | 136,366,732 | — (not dumped; larger-T violation check) | Pass (28 min) |
| 2-level | coarse | all-root | 2 / 3 | 1,093 / 339,744 | 4 / 4 (set-identical) | Pass |
| 2-level | coarse | both-roles | 2 | 350,281 | 6 (4 bundle + 2 partial-unbundle) | Pass |
What saturation means: project each reachable state onto its identity-free bundle structure
(per node ⟨hasPriority, bundledBy, missing, which sub slots are populated⟩; drop serial & payload value — exactly the fields the structural invariants read).
In the faithful superfine all-root model the structural set is 6 and saturates at T=2: dumping the complete T=3 exhaustion (137,333,348 states) and projecting shows it is T=2 ≡ T=3 set-identical.
superfine's 6 = coarse's 4 (bundle structures) + the two within-operation Phase-3 intermediates (one child re-pointed to a bundled-ref, the other not yet — exactly where a concurrency hazard could hide).
The both-roles 6 = 4 bundle + 2 partial-unbundle (the unbundle-side structures).
A third thread reaches no new safety-relevant structure. Meanwhile the raw count explodes (~10⁵ → 1.37×10⁸) — more threads, no new structure.
3-level is by extrapolation (honest scope): the 3-level superfine σ-saturation is intractable to dump directly
(superfine T=4 and 3-level superfine dumps are out of reach). The 3-level case is reached by extrapolation via the tree-independence of the commit-role structure (Facts A–C) — not a direct measurement.
(3-level coarse T=2 already reaches ≥9 structures; its exhaustion was not completed.)
The derived local structural invariants (SubNeverMissing / BundledHasCopy / StaleParentExcluded / SubPresenceUniform) are validated with
no violation up to 3-level superfine T=3 all-root + T=2 both-roles (the most-interleaved model on both fold paths).
N)Safety invariants do not parameterize liveness. We prove EventuallyAllDone
(<>AllDone) by a well-founded ranking function. The argument is independent
of the tree axes and of the thread count N.
t carries MyTag(t)=⟨iter(t), t⟩ (TagOlder total order; smaller = older).priorityTag[n] becomes the older of its value and MyTag(t) (TagAfterFail) → monotone non-increasing in tag order.CanProceed(t,n) permits a CAS only when priorityTag[n] is Null or held by t → younger contenders are gated out.R(s) = ( M(s), d(s) ) -- lexicographic, well-founded
M(s) : multiset ⟦ MyTag(t) : t ∈ Active ⟧ (Dershowitz–Manna multiset extension)
d(s) : for the global-oldest t★ = argmin MyTag, remaining pc[t★]→"done" path length
(finite, acyclic single-transaction CFG)WF_vars(NextStep) and Privilege=TRUE,
EventuallyAllDone holds for every finite Threads, independent of |Threads|.
Because the rank quantifies over the global oldest — which exists for any finite Active —
liveness needs no thread cutoff (the cleaner half of the parameterized result).
Remaining obligation (§7.5, the one open lemma): Lemma (progress) assumes the privileged
t★ completes without unbounded retry. Peers are gated out of t★'s contended node,
but a peer on a different node (an ancestor/child in the chain) can still raise a DISTURBED/COLLIDED
through the bundle chain. The proof must show these structural disturbances are bounded (each is caused
by a peer commit that itself removes a younger element from M → cannot recur forever). The bounded
EventuallyAllDone runs (2-thread all-roles superfine, 3-thread confC both levels, the 413 M dynamic-release)
discharge this at the cutoff; the general bound is the open liveness lemma.
The cutoff (tree axis), the saturation (thread axis), the §7 liveness ranking, and any derived local structural invariant
(SubNeverMissing / BundledHasCopy / StaleParentExcluded / SubPresenceUniform,
validated with no violation up to 3-level superfine T=3 all-root + T=2 both-roles) are stated for a
fixed, single-parent rooted tree (Next has no node-insert/remove; ParentOf is single-valued).
Two regimes lie outside and are verified separately, not by extension of this argument:
| Regime | Covered by |
|---|---|
| Dynamic topology (online insert/release) | *_dynamic_* specs (e.g. the 413 M dynamic-release run) + transaction_dynamic_node_test. SubPresenceUniform breaks transiently on insert into an already-bundled parent |
| Hard links / DAG (a child with ≥ 2 parents) | §5 BundleUnbundle_hardlink_* + the Phase-3 fix. Conjuncts naming the parent are ill-formed under a multi-valued ParentOf |
The distinct-state count is a deterministic function of (.tla, cfg): TLC's BFS reproduces the
reachable set exactly for a fixed model (seed/worker count affect only discovery order). So counts are
not comparable across spec versions: the same confC superfine T=3 configuration moved through
514 M → 1.155 G → 640 M → 540 M as successive protocol fixes landed in Next (identical cfg constants throughout).
The version-independent quantity is the σ-projection (the saturated structure set), never the raw count.
Safety, tree axis: ∀ tree shape via a structural-cutoff theorem (catamorphism ⇒ depth-3/width-2 cutoff, discharged exhaustively by TLC).
Safety, thread axis: not a ∀T theorem — symmetry is semantic but TLC can't apply it and is permutation-only.
Verify exhaustively to the contention bound (superfine T=3=137 M, coarse T=4=136 M) + measure σ-saturation (T=2 ≡ T=3, 6 structures) ⇒ a strongly-evidenced conjecture.
Liveness: ∀N via an oldest-tag ranking-function argument (no thread cutoff; verified exhaustively at small T). The gate is a pure liveness device, disjoint from safety.
Source: doc/parameterized_cutoff.md (§1–§9) / VERIFICATION.md Thread-axis saturation §. Related: LL-free specification / coverage overview.