▲ Overview

Dynamic LL-free — online insert / release

BundleUnbundle_2level_LLfree_dynamic.tla / _3level_LLfree_dynamic.tla

The dynamic mode of the LLfree Layer 2 spec: it adds runtime child insertion (insert(online=true)) and release (release). The tree structure is no longer fixed; it mutates dynamically each iteration.

Priority gating (CanProceed / TagAfterFail / TagAfterSuccess / PreemptTag / ClearMyTags) is identical to 2-level LLfree — see also slides_layer2_LLfree.html for tree-structure detail.

Dynamic tree

    Parent
     ├── DynChild1  (inserted / released at runtime)
     └── DynChild2  (ditto)

Both children start unattached (their own priority wrappers). Phase 1 attaches via insert; Phase 2 interleaves commit + release.

Per-thread role configuration

Role (CONSTANT)Behavior
InsertThreadsRun insert(online=true) — pick an uninserted child and attach to Parent
RootThreadsRun CommitParent — snapshot Parent, increment every discovered child's payload
LeafThreadsRun CommitChild — direct commit per child discovered in the snapshot
ReleaseThreadsRelease children (only after own commits are done)

Dynamic discovery is key: children are not hardcoded; commit targets come from the snapshot. This covers boundary races such as "commit while a half-constructed insert is in flight" and "commit just before release."

insert(online=true) and release

insert(online=true) — a 5-step CAS pipeline (not one action)

\* Insert is split into 5 actions so TLC explores every
\* half-constructed-insert interleaving (target: \E c : ~inserted[c]).
InsertStart → InsertCASParent → InsertReadChild →
InsertCASChild(t):  linkage'[c] = InsertedRef(Parent, ser, cpkt)   \* packet-carrying ref
InsertFinal(t):     linkage'[Parent] = PriorityWrapper(
                       MakePacket(Parent, _, newSub, TRUE), ser)   \* SEPARATE CAS, missing=TRUE
                     \* on success: inserted'[c]=TRUE, ClearMyTags(t)

release — a 4-step CAS pipeline

ReleaseStart → ReleaseCASParent → ReleaseReadChild → ReleaseCASChild
    \* the Parent-slot CAS and the child-slot CAS are SEPARATE actions;
    \* the two CanProceed gates (Parent / c) live in different steps.

Interference between insert and bundle/commit: If another thread runs bundle(Parent) while insert(c) fires, the Phase-4 CAS fails its freshness check (the parent linkage changed) → retry; the bundling thread sees the newly inserted child on re-collect. (No reachability gate exists in the dynamic specs — that is hardlink-only.) Priority gating arbitrates between the inserter and the bundler by transaction age.

static vs dynamic mode + verification results

static / dynamic mode contrast

ItemStatic (_LLfree.tla)Dynamic (_LLfree_dynamic.tla)
Child setFixed from init (Child1, Child2)Dynamically inserted / released (DynChild1, DynChild2)
New actions—Insert* (5-step) / Release* (4-step) pipelines
Thread rolesRoot / Leaf roles (RootThreads / LeafThreads)+ Insert / Release roles (InsertThreads / ReleaseThreads)
Commit targetsHardcodedDiscovered dynamically from snapshot
Invariants5 (SnapshotConsistency etc.)+ insert/release consistency checks

Verification results

cfgThreadsStatesDepthTimeResult
2-level dynamic 2-thread superfine (no release)2(~M)——✅ Pass (safety); liveness via the release run below
2-level dynamic release superfine live2413,884,5163207:13✅ Pass + liveness (ohtaka)
3-level dynamic 2-thread coarse2(M~)——✅ Pass + liveness
3-level dynamic 3-thread release3(large)——ohtaka pending

What the 413M-state run proves: The 2-level dynamic release superfine liveness run is one of the largest verifications in the corpus. All interleavings that include dynamic insert/release satisfy safety + liveness — proven by exhaustion. Priority gating + dynamic discovery + bounded variable domains achieve CONSTRAINT-free termination.

Running large configs

# 2-level dynamic release superfine (ohtaka recommended)
java -XX:+UseParallelGC -Xmx32g -cp tla2tools.jar tlc2.TLC \
  -workers auto -config BundleUnbundle_2level_LLfree_dynamic_release_superfine_live_mc.cfg \
  BundleUnbundle_2level_LLfree_dynamic.tla

Related specs / decks