▲ Overview

Dynamic LL-free — online insert / release

BundleUnbundle_2level_LLfree_dynamic.tla / _3level_LLfree_dynamic.tla

Extends the static LLfree spec (BundleUnbundle_2level_LLfree.tla) with 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 slides_layer2_LLfree.html.

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

InsertOnline action

InsertOnline(t) ==
    /\ t \in InsertThreads
    /\ pc[t] = "idle"
    /\ \E c \in UninsertedChildren :
        /\ \* ① read parent's wrapper
        /\ CanProceed(t, Parent)              \* ★ priority gate
        /\ \* ② CAS a new wrapper that writes the child's packet into parent.sub[c]
        /\ LET newSubs == [Parent.sub EXCEPT ![c] = childPacket]
               newW == PriorityWrapper(MakePacket(Parent, payload, newSubs, FALSE), ser)
           IN linkage' = [linkage EXCEPT ![Parent] = newW,
                                       ![c] = BundledRefWrapper(Parent, ser)]
    /\ ClearMyTags(t)                       \* same tag release as commit success

Release action

Release(t) ==
    /\ t \in ReleaseThreads
    /\ \E c \in InsertedChildren :
        /\ \* Set parent.sub[c] to Null and restore the child to its own priority wrapper
        /\ CanProceed(t, Parent)
        /\ CanProceed(t, c)
        /\ ...
        /\ linkage' = [linkage EXCEPT ![Parent] = parentWithNullSlot,
                                   ![c] = PriorityWrapper(originalChildPkt, ser)]

Interference between insert and bundle/commit: If another thread runs bundle(Parent) while insert(c) fires, the Phase 4 m_missing=false finalise triggers the Phase 4 reachability gate → DISTURBED retry; the bundling thread sees the newly inserted child on re-collect. Priority gating arbitrates between the inserter and the bundler by transaction age.

Diff vs static spec + verification results

Summary of differences

ItemStatic (_LLfree.tla)Dynamic (_LLfree_dynamic.tla)
Child setFixed from init (Child1, Child2)Dynamically inserted / released (DynChild1, DynChild2)
New actions—InsertOnline / Release
Thread rolesAll threads symmetricConfigured via InsertThreads / RootThreads / LeafThreads / ReleaseThreads
Commit targetsHardcodedDiscovered dynamically from snapshot
Invariants5 (SnapshotConsistency etc.)+ insert/release consistency checks

Verification results

cfgThreadsStatesDepthTimeResult
2-level dynamic 2-thread superfine2(~M)——✅ Pass + liveness
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_3thr_B_live_mc.cfg \
  BundleUnbundle_2level_LLfree_dynamic.tla

Related specs / decks