Add TLA+ verification suite for OLC ART concurrency#857
Open
thompsonbry wants to merge 14 commits into
Open
Conversation
added 8 commits
June 11, 2026 14:42
8 staged models verifying correctness of the OLC ART algorithm under concurrent insert, remove, and scan operations: Stage 1: Inode256VIS — sequential scan correctness with bitmask-only encoding (no XOR sentinel). Demonstrates the value=0 bug. Stage 2: OLCSlot — single-slot OLC protocol (writer/reader interleaving) Stage 3: OLCInsert — two writers racing for same node (mutual exclusion) Stage 4: OLCChainMembership — chain precondition under concurrent insert Stage 5: OLCChainCut — cut_point_parent evaluation (Cases A/B/C) Stage 6: OLCIterRemove — iterator detects node obsolescence Stage 7: OLCInsertChainVIS — transient VIS state during chain insert Stage 8: OLCDoubleCut — two removes on same chain (at-most-one-cut) Key findings: - Stage 6 revealed the QSBR window: iterator can act on a disconnected (but not yet obsoleted) node. This is safe by design — QSBR prevents reclamation while the iterator is in its critical section. - The bitmask-only encoding is proven correct: slot[i]!=NULL || bitmask[i] is equivalent to ground truth for all reachable states. Total: 21,598 distinct states, all pass in <5s. Run: bash spec/tla/run-all-stages.sh (requires tla2tools.jar)
Stage 3 (OLCInsert): Split WWrite into WWriteSlot + WWriteCount to model non-atomic count maintenance. CountConsistency now only checks when unlocked. (Critical C2) Stage 5 (OLCChainCut): Add grandparent node with lock-failure path. Replace trivially-true ChainLockValid with RemoverLockedImpliesChainSingle. Add InsertDone cycling. (Major M1, M4) Stage 6 (OLCIterRemove): Expand to 3 nodes (gp→parent→child). Fix SnapshotValid to be general. Remover can target either parent or child. Tests cascading obsolescence detection. (Major M2, depth gap) Stage 8 (OLCDoubleCut): Add RDone cycling so AtMostOneCut is non-trivial. Replace NoDoubleFree with NoDoubleObsolete. (Major M3) All 8 stages pass. Total: 21,980 distinct states, <5s.
…ete) Stage 6 (OLCIterRemove) now has 3 processes: - Iterator: descends gp→parent→child with OLC validation - Remover: can obsolete parent or child - Writer: locks parent or child, bumps version, unlocks (no obsolete) This exercises the critical interleaving where a concurrent INSERT (not remove) modifies a node the iterator has cached. The iterator must detect the version change and restart. State space: 96 → 23,458 distinct states. Still <1s.
Models parent → chain0 → chain1 topology. Exercises: - cut_level moves DOWN: insert breaks chain0 after chain1 locked - cut_level stays at 0: both chain nodes lock successfully - Partial cut (chain0 as CPP): chain1 removed from chain0 - Full cut (parent as CPP): chain0+chain1 removed from parent This is the novel complexity in key_view trees: the bottom-up locking with cut_level adjustment when a concurrent insert breaks chain membership at an intermediate level. 211 distinct states, <1s. All key actions exercised per coverage.
Models the complete chain cut with all critical paths:
- P1: Normal cut (parent is CPP, no shrink)
- P2: Parent needs shrink → acquire grandparent
- P3: Case B (parent single-child → chain extends up)
- P4: Cascading Case B (gp also single-child → root is CPP)
- P5: Root as CPP (set root=nullptr, tree emptied)
- P6: Grandparent acquisition fails → restart
- P7: Case C (child pointer gone → restart)
Topology: root_ptr → gp → parent → chain → leaf
Non-deterministic init: gp_count ∈ {1,2}, p_count ∈ {1,2}
Concurrent inserter can add children to parent or gp.
All paths exercised per coverage analysis:
- RCaseBParent, RCaseBGP, RAcquireRoot all reachable
- RAcquireGPForShrink_Parent and _GP both reachable
- All 4 cut_level variants in RCut exercised
1,494 distinct states, <1s. 10 stages total: 47,049 states.
Models the critical key_view scenario: two keys share a prefix, one stored as VIS (short key) and one continuing deeper (long key). Tree: parent → shared_node(VIS + child_B) → chain_B → leaf_B Verifies: chain identification for key B correctly excludes shared_node when it has a VIS entry (CorrectCount=2, not chain member). Bug demonstration (OLCKeyViewChain_BugDemo.cfg): with BuggyCount (VIS invisible to nullptr scan), the chain cut incorrectly includes shared_node → NoDataLoss invariant VIOLATED → key A's value lost. This directly models the variable-length key complexity: - Concurrent remove of key A (VIS) while key B is being chain-cut - OLC version check correctly detects the VIS removal - After VIS removed, shared_node correctly becomes chain member (count=1) 262 distinct states (correct), bug demo violated in 233 states.
Verifies the ART key_view tree maintenance algorithm for variable-length
keys. Sequential model (no concurrency) checking:
- Well-formedness: no single-child non-VIS node unless prefix overflow
- Key preservation: all inserted keys remain reachable
- No orphans: all nodes reachable from root
- Type correctness: all node fields in valid domains
Key set: {<<1>>, <<1,2>>, <<1,2,1>>, <<2,1>>, <<1,2,1,2,1>>}
PrefixCapacity=2 exercises both collapse-success and collapse-blocked.
5,035 distinct states, depth 14, <1s.
Algorithmic paths exercised:
- Prefix overflow persistence (collapse blocked)
- Collapse after remove (VIS cleared, single-child remains)
- Collapse after insert (prefix split shortens child prefix)
- VIS + child coexistence (key is prefix of another)
- Chain split (insert diverging mid-chain)
Includes design parameters document (tree-structure-model-design.md).
The real implementation's insert_internal_key_view is iterative and returns immediately after a prefix split. It does NOT check whether ancestor nodes became collapsible (single-child non-VIS with combined prefix <= key_prefix_capacity). Counterexample (3 inserts, no removes): Insert <<1,2,1,2,1>>, <<1>>, <<1,2,1>> → Node1 left as single-child non-VIS with combined=1<=2 The correct model (Spec) passes WellFormed by collapsing on unwind. The buggy model (BuggySpec) violates WellFormed in 4 states. This affects both art.hpp and olc_art.hpp insert paths. Impact: suboptimal tree structure (memory waste, extra traversal hop). No data loss — keys remain reachable. See also: ARTTreeMaintenance_NoAncestorCollapse.cfg
Contributor
WalkthroughThis PR adds a staged TLA+ verification suite: VIS/inode models, single-slot OLC and multi-writer protocols, chain-membership/cut models (multi-level/full), iterator/remove and VIS TOCTOU models (with bug variants), sequential ART tree maintenance, docs, and TLC runner scripts. ChangesTLA+ Staged Verification Suite for Concurrent Data Structures
Estimated code review effort🎯 5 (Critical) | ⏱️ ~120 minutes
✨ Finishing Touches🧪 Generate unit tests (beta)
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 15
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@spec/tla/OLCChainCut.tla`:
- Around line 237-239: The invariant RemoverLockedImpliesChainSingle references
non-existent states "case_b" and "case_c" in the rpc set; update this invariant
to match the protocol by removing "case_b" and "case_c" from the set (leaving
{"read_parent", "validate_parent", "case_a", "cut"}) or, if those states are
intended, add corresponding state definitions and transitions to TypeOK and the
remover actions; ensure the symbols r_chain_locked, rpc and c_count remain used
consistently with the rest of the spec.
- Around line 211-216: StateConstraint currently bounds p_ver and gp_ver but
omits c_ver, allowing c_ver to grow unbounded; update StateConstraint to include
a symmetric bound for c_ver (e.g., /\ c_ver <= MaxVersion and optionally /\
c_ver >= 0 or same lower bound as p_ver) so the child node version is
constrained like p_ver/gp_ver; modify the StateConstraint definition
(referencing StateConstraint, p_ver, c_ver, gp_ver, and MaxVersion) to add the
c_ver bound.
- Around line 99-110: The AcquireGP transition currently snapshots r_gp_ver_snap
= gp_ver before locking, which can be 0 and leads Unlock to skip releasing the
grandparent; add a boolean flag (e.g., r_gp_locked) to track whether AcquireGP
actually succeeded in locking the grandparent, set r_gp_locked' = TRUE in
AcquireGP's THEN branch (and FALSE in the ELSE branch), update the state tuple
in AcquireGP to include this new flag, and modify Unlock to check r_gp_locked
(not r_gp_ver_snap) to decide whether to perform the grandparent unlock and then
reset r_gp_locked' = FALSE after unlocking.
In `@spec/tla/OLCChainCutFull.tla`:
- Around line 264-294: RCut contains an unreachable branch for r_cut_level = 3
(the "cut" case) because RLockChain sets r_cut_level = 3 but always transitions
to "eval_parent" then to 0/1/2 before "cut"; remove the r_cut_level = 3 branch
from RCut or, if kept intentionally for future-proofing, add a clear comment in
RCut referencing RLockChain and the "eval_parent" transition to explain why the
branch is retained; update any related invariants or tests that assumed the
branch existed.
- Around line 296-307: RRestart currently only clears r_parent_locked and
r_gp_locked, so when the parent or grandparent were locked as the CPP (set via
RUpgradeParent/RUpgradeGP using r_cpp_locked and r_cut_level) they remain locked
after restart; update RRestart to also clear the CPP-derived locks by checking
r_cpp_locked and r_cut_level: if r_cpp_locked and r_cut_level = 2 treat the
parent as unlocked (clear the parent/CPP lock state for the parent), and if
r_cpp_locked and r_cut_level = 1 treat the grandparent as unlocked (clear the
gp/CPP lock state for the grandparent); modify the RRestart transition to
include these additional conditions when resetting lock flags (refer to
RRestart, r_parent_locked, r_gp_locked, r_cpp_locked, and r_cut_level) so
restart always releases parent/gp CPP locks.
In `@spec/tla/OLCChainMembership.cfg`:
- Around line 6-8: The INVARIANTS block currently lists ChainSafety and
NotChainCorrect but omits the TypeOK invariant; update the INVARIANTS section to
include TypeOK alongside ChainSafety and NotChainCorrect so the model checks
type correctness (i.e., add TypeOK to the list that contains ChainSafety and
NotChainCorrect in OLCChainMembership.cfg).
In `@spec/tla/OLCChainMembership.tla`:
- Line 125: The Spec currently omits weak fairness (WF_vars) while OLCInsert and
OLCDoubleCut include WF_vars for liveness; to resolve the inconsistency, either
add the same weak fairness conjunct to Spec (change Spec to: Init /\
[][Step]_vars /\ WF_vars(Step)) so the stage matches the liveness assumptions,
or else add an explicit comment near Spec/Init/Step stating that WF_vars is
intentionally omitted because this stage verifies only safety properties
(ChainSafety, NotChainCorrect) and liveness is out of scope; reference symbols:
Spec, Init, Step, WF_vars, OLCInsert, OLCDoubleCut, ChainSafety,
NotChainCorrect.
- Around line 30-37: Init lacks an accompanying TypeOK invariant to assert
expected variable types; add a TypeOK definition that checks types/finite
domains for all variables used in Init (e.g., count, version, rpc, r_count,
r_ver, ipc) and then include TypeOK in the OLCChainMembership.cfg invariants
list so the model checks type correctness like the other specs (referencing Init
and OLCChainMembership.cfg to locate where to add the predicate and to add it to
the invariant set).
In `@spec/tla/OLCSlot.tla`:
- Around line 55-56: The current guard "/\ version <= MaxVersion" lets a write
start at version = MaxVersion but the write logic increments version twice (at
the actions around the blocks referenced by lines 74-75 and 95-96), allowing
version to exceed MaxVersion; change the precondition to ensure any write that
can increment twice cannot start so close to the cap (e.g., replace the guard
with "/\ version <= MaxVersion - 2") or alternatively add checks/clamping in the
incrementing actions so they never increase version beyond MaxVersion (adjust
the guards or use Min(MaxVersion, version + n) in the increment logic); refer to
the variables version and MaxVersion and the write/increment actions around the
noted locations when applying the fix.
In `@spec/tla/run-all-stages.sh`:
- Line 16: The script run-all-stages.sh hardcodes the TLA tools JAR path
(~/tools/tla/tla2tools.jar); update the script to read the path from an
environment variable (e.g., TLA_TOOLS_JAR or TLA_TLA2TOOLS_JAR) and fall back to
the current default if unset, or alternatively add a clear comment at the top
documenting the required installation path and how to override it via the env
var; update the invocation symbol (the -cp argument that currently references
~/tools/tla/tla2tools.jar) to use that env var so the script becomes
configurable.
- Line 23: The shell uses grep -P in the assignment to the variable states which
relies on GNU grep; replace the Perl-regex usage by switching to a
POSIX-compatible expression (use grep -oE and replace \d with [0-9]+) in the
command that generates states so the script works on macOS without GNU grep;
update the command that sets the states variable accordingly (the line assigning
to states in run-all-stages.sh).
- Line 19: Remove the unused local variable assignment "local rc=$?" from
spec/tla/run-all-stages.sh; locate the assignment (the "rc" variable) and delete
that line so the script no longer creates an unused variable—no further logic
changes needed since the script already checks TLC's output directly.
In `@spec/tla/staged-model-plan.md`:
- Around line 85-249: The spec is missing documentation for stages 9-12
referenced by run-all-stages.sh and the PR objectives; add entries for
OLCChainMultiLevel.tla, OLCChainCutFull.tla, OLCKeyViewChain.tla (bug `#850`), and
ARTTreeMaintenance.tla specifying for each: hazard(s), brief description of
"What", variables/roles (unique names like multi-level shared arrays,
parent/child versions, key_view flags), bounded domains (slot/count/version
ranges), key properties to verify (safety/progress invariants), and expected
state counts/runtime; update the stage index and any PR objective text to
reference these filenames and the discovered bug number consistently so the plan
and run-all-stages.sh remain in sync.
- Around line 252-266: The Verification Matrix currently lists only stages 1–8
and an incorrect total time; update the matrix table under the "Verification
Matrix" heading to include rows for stages 9–12 (fill in Hazards, Slots, Procs,
Est. States, Time, and Key Property consistent with the other rows or the test
plan), and adjust the "**Total estimated time:**" summary to reflect the full
runtime for all 12 stages; locate the table by the "Verification Matrix" header
and the final "Total estimated time" line in staged-model-plan.md when making
the edits.
In `@spec/tla/tree-structure-model-design.md`:
- Line 69: The table entry incorrectly lists StateConstraint as "nxt ≤ 8 (max 7
nodes)" while the actual constant is StateConstraint == nxt <= 7 in
ARTTreeMaintenance (symbol: StateConstraint); update the markdown row to "nxt ≤
7 (max 7 nodes)" so the doc matches the implementation and retains the same note
"Keeps state space at ~5000".
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 83f8c934-fe24-4a42-b548-f99d37168e6c
📒 Files selected for processing (30)
spec/tla/ARTTreeMaintenance.cfgspec/tla/ARTTreeMaintenance.tlaspec/tla/ARTTreeMaintenance_NoAncestorCollapse.cfgspec/tla/Inode256VIS.cfgspec/tla/Inode256VIS.tlaspec/tla/Inode256VIS_BugDemo.cfgspec/tla/OLCChainCut.cfgspec/tla/OLCChainCut.tlaspec/tla/OLCChainCutFull.cfgspec/tla/OLCChainCutFull.tlaspec/tla/OLCChainMembership.cfgspec/tla/OLCChainMembership.tlaspec/tla/OLCChainMultiLevel.cfgspec/tla/OLCChainMultiLevel.tlaspec/tla/OLCDoubleCut.cfgspec/tla/OLCDoubleCut.tlaspec/tla/OLCInsert.cfgspec/tla/OLCInsert.tlaspec/tla/OLCInsertChainVIS.cfgspec/tla/OLCInsertChainVIS.tlaspec/tla/OLCIterRemove.cfgspec/tla/OLCIterRemove.tlaspec/tla/OLCKeyViewChain.cfgspec/tla/OLCKeyViewChain.tlaspec/tla/OLCKeyViewChain_BugDemo.cfgspec/tla/OLCSlot.cfgspec/tla/OLCSlot.tlaspec/tla/run-all-stages.shspec/tla/staged-model-plan.mdspec/tla/tree-structure-model-design.md
Comment on lines
+99
to
+110
| AcquireGP == | ||
| /\ rpc = "acquire_gp" | ||
| /\ IF gp_ver % 2 = 0 | ||
| THEN /\ gp_ver' = gp_ver + 1 \* lock grandparent | ||
| /\ r_gp_ver_snap' = gp_ver | ||
| /\ rpc' = "cut" | ||
| ELSE /\ rpc' = "gp_failed" \* grandparent busy, must release all | ||
| /\ gp_ver' = gp_ver | ||
| /\ r_gp_ver_snap' = r_gp_ver_snap | ||
| /\ UNCHANGED <<r_chain_locked, r_p_ver_snap, p_ver, p_count, c_count, | ||
| gp_child, ipc, i_target>> | ||
|
|
Contributor
There was a problem hiding this comment.
Critical bug: Grandparent lock leak when initial gp_ver is 0.
The remover snapshots r_gp_ver_snap' = gp_ver (line 103) before locking the grandparent. When gp_ver = 0 initially (line 52), r_gp_ver_snap becomes 0. Later, Unlock (line 131) checks IF r_gp_ver_snap /= 0 to decide whether to unlock the grandparent, but this condition is FALSE when the snapshot is 0, so the grandparent remains locked indefinitely even though it was acquired.
The check should verify whether the remover actually locked the grandparent (e.g., track whether we reached "acquire_gp" successfully), not rely on the snapshot value.
🔒 Proposed fix: Track grandparent lock separately
Add a boolean flag to track grandparent acquisition:
VARIABLES
(* Remover state *)
rpc, \* remover program counter
r_chain_locked, \* remover holds chain lock on child
r_p_ver_snap, \* remover's snapshot of parent version
r_gp_ver_snap, \* remover's snapshot of grandparent version
+ r_gp_locked, \* remover holds grandparent lockUpdate AcquireGP to set the flag:
AcquireGP ==
/\ rpc = "acquire_gp"
/\ IF gp_ver % 2 = 0
THEN /\ gp_ver' = gp_ver + 1
/\ r_gp_ver_snap' = gp_ver
+ /\ r_gp_locked' = TRUE
/\ rpc' = "cut"
ELSE /\ rpc' = "gp_failed"
/\ gp_ver' = gp_ver
/\ r_gp_ver_snap' = r_gp_ver_snap
+ /\ r_gp_locked' = FALSEUpdate Unlock to use the flag:
Unlock ==
/\ rpc = "unlock"
/\ p_ver' = p_ver + 1
- /\ IF r_gp_ver_snap /= 0
+ /\ IF r_gp_locked
THEN gp_ver' = gp_ver + 1
ELSE gp_ver' = gp_ver
/\ r_chain_locked' = FALSE
- /\ r_gp_ver_snap' = 0
+ /\ r_gp_locked' = FALSE
/\ rpc' = "done"🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCChainCut.tla` around lines 99 - 110, The AcquireGP transition
currently snapshots r_gp_ver_snap = gp_ver before locking, which can be 0 and
leads Unlock to skip releasing the grandparent; add a boolean flag (e.g.,
r_gp_locked) to track whether AcquireGP actually succeeded in locking the
grandparent, set r_gp_locked' = TRUE in AcquireGP's THEN branch (and FALSE in
the ELSE branch), update the state tuple in AcquireGP to include this new flag,
and modify Unlock to check r_gp_locked (not r_gp_ver_snap) to decide whether to
perform the grandparent unlock and then reset r_gp_locked' = FALSE after
unlocking.
Comment on lines
+211
to
+216
| StateConstraint == | ||
| /\ p_ver <= MaxVersion | ||
| /\ p_count >= 1 | ||
| /\ p_count <= 4 | ||
| /\ gp_ver <= MaxVersion | ||
|
|
Contributor
There was a problem hiding this comment.
Missing version bound for child node.
The state constraint bounds p_ver and gp_ver but not c_ver. If the chain is repeatedly locked/unlocked, c_ver could grow unbounded, expanding the state space unnecessarily.
🔧 Proposed fix
StateConstraint ==
/\ p_ver <= MaxVersion
/\ p_count >= 1
/\ p_count <= 4
/\ gp_ver <= MaxVersion
+ /\ c_ver <= MaxVersion🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCChainCut.tla` around lines 211 - 216, StateConstraint currently
bounds p_ver and gp_ver but omits c_ver, allowing c_ver to grow unbounded;
update StateConstraint to include a symmetric bound for c_ver (e.g., /\ c_ver <=
MaxVersion and optionally /\ c_ver >= 0 or same lower bound as p_ver) so the
child node version is constrained like p_ver/gp_ver; modify the StateConstraint
definition (referencing StateConstraint, p_ver, c_ver, gp_ver, and MaxVersion)
to add the c_ver bound.
Comment on lines
+237
to
+239
| RemoverLockedImpliesChainSingle == | ||
| (r_chain_locked /\ rpc \in {"read_parent", "validate_parent", "case_a", "case_b", "case_c", "cut"}) | ||
| => c_count = 1 |
Contributor
There was a problem hiding this comment.
Invariant references non-existent states.
The invariant includes "case_b" and "case_c" in the state set (line 238), but these states don't exist in the remover protocol. TypeOK (line 221-223) only defines "case_a", and the remover actions never transition to "case_b" or "case_c".
This is likely a copy-paste error from an earlier version. Remove the invalid states or add them to the protocol if they're intended.
🛠️ Proposed fix
RemoverLockedImpliesChainSingle ==
- (r_chain_locked /\ rpc \in {"read_parent", "validate_parent", "case_a", "case_b", "case_c", "cut"})
+ (r_chain_locked /\ rpc \in {"read_parent", "validate_parent", "case_a", "acquire_gp", "gp_failed", "cut"})
=> c_count = 1🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCChainCut.tla` around lines 237 - 239, The invariant
RemoverLockedImpliesChainSingle references non-existent states "case_b" and
"case_c" in the rpc set; update this invariant to match the protocol by removing
"case_b" and "case_c" from the set (leaving {"read_parent", "validate_parent",
"case_a", "cut"}) or, if those states are intended, add corresponding state
definitions and transitions to TypeOK and the remover actions; ensure the
symbols r_chain_locked, rpc and c_count remain used consistently with the rest
of the spec.
Comment on lines
+264
to
+294
| RCut == | ||
| /\ rpc = "cut" | ||
| /\ CASE r_cut_level = 0 -> \* Root is CPP: empty tree | ||
| /\ root_child' = FALSE | ||
| /\ root_ver' = root_ver + 1 \* unlock root | ||
| /\ gp_ver' = OBSOLETE \* obsolete gp | ||
| /\ p_ver' = OBSOLETE \* obsolete parent | ||
| /\ c_ver' = OBSOLETE \* obsolete chain | ||
| /\ UNCHANGED <<gp_count, gp_child, p_count, p_child>> | ||
| [] r_cut_level = 1 -> \* GP is CPP: remove parent from gp | ||
| /\ gp_child' = FALSE | ||
| /\ gp_count' = gp_count - 1 | ||
| /\ gp_ver' = gp_ver + 1 \* unlock gp | ||
| /\ p_ver' = OBSOLETE \* obsolete parent | ||
| /\ c_ver' = OBSOLETE \* obsolete chain | ||
| /\ UNCHANGED <<root_ver, root_child, p_count, p_child>> | ||
| [] r_cut_level = 2 -> \* Parent is CPP: remove chain from parent | ||
| /\ p_child' = FALSE | ||
| /\ p_count' = p_count - 1 | ||
| /\ p_ver' = p_ver + 1 \* unlock parent | ||
| /\ c_ver' = OBSOLETE \* obsolete chain | ||
| /\ UNCHANGED <<root_ver, root_child, gp_count, gp_child, gp_ver>> | ||
| [] r_cut_level = 3 -> \* Chain-only (no additional chain on stack) | ||
| /\ c_ver' = OBSOLETE \* obsolete chain | ||
| /\ UNCHANGED <<root_ver, root_child, gp_count, gp_child, gp_ver, | ||
| p_count, p_child, p_ver>> | ||
| /\ r_chain_locked' = FALSE /\ r_parent_locked' = FALSE | ||
| /\ r_gp_locked' = FALSE /\ r_cpp_locked' = FALSE | ||
| /\ rpc' = "done" | ||
| /\ UNCHANGED <<r_cut_level, r_needs_shrink, r_cached_ver, ipc, i_target>> | ||
|
|
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial | 💤 Low value
Dead code: cut_level = 3 branch is unreachable.
The RCut action includes a case for cut_level = 3 (line 286), but this branch is unreachable in the current protocol. RLockChain initializes r_cut_level = 3 (line 91), but then always transitions to "eval_parent" (line 92), which eventually upgrades r_cut_level to 0, 1, or 2. There's no path to "cut" that preserves cut_level = 3.
This might be future-proofing or a design artifact. Consider removing it or adding a comment explaining its purpose.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCChainCutFull.tla` around lines 264 - 294, RCut contains an
unreachable branch for r_cut_level = 3 (the "cut" case) because RLockChain sets
r_cut_level = 3 but always transitions to "eval_parent" then to 0/1/2 before
"cut"; remove the r_cut_level = 3 branch from RCut or, if kept intentionally for
future-proofing, add a clear comment in RCut referencing RLockChain and the
"eval_parent" transition to explain why the branch is retained; update any
related invariants or tests that assumed the branch existed.
Comment on lines
+296
to
+307
| RRestart == | ||
| /\ rpc = "restart" | ||
| /\ c_ver' = IF r_chain_locked THEN c_ver + 1 ELSE c_ver | ||
| /\ p_ver' = IF r_parent_locked THEN p_ver + 1 ELSE p_ver | ||
| /\ gp_ver' = IF r_gp_locked THEN gp_ver + 1 ELSE gp_ver | ||
| /\ root_ver' = IF r_cpp_locked /\ r_cut_level = 0 THEN root_ver + 1 ELSE root_ver | ||
| /\ r_chain_locked' = FALSE /\ r_parent_locked' = FALSE | ||
| /\ r_gp_locked' = FALSE /\ r_cpp_locked' = FALSE | ||
| /\ rpc' = "idle" | ||
| /\ UNCHANGED <<root_child, gp_count, gp_child, p_count, p_child, | ||
| r_cut_level, r_needs_shrink, r_cached_ver, ipc, i_target>> | ||
|
|
Contributor
There was a problem hiding this comment.
Critical bug: Parent and grandparent not unlocked on restart when they are CPP.
When the parent is the CPP (r_cpp_locked = TRUE, r_cut_level = 2), it is write-locked (line 126), but RRestart only unlocks it if r_parent_locked is TRUE (line 299). The r_parent_locked flag tracks when the parent is locked as a chain member (Case B), not when it's the CPP. So if restart happens after RUpgradeParent, the parent remains locked.
The same issue affects the grandparent: when r_cut_level = 1 and the gp is the CPP, line 179 locks it, but RRestart line 300 only unlocks if r_gp_locked is TRUE, which isn't set in RUpgradeGP.
The restart logic must check r_cpp_locked and r_cut_level to unlock the correct CPP node.
🔓 Proposed fix
RRestart ==
/\ rpc = "restart"
/\ c_ver' = IF r_chain_locked THEN c_ver + 1 ELSE c_ver
- /\ p_ver' = IF r_parent_locked THEN p_ver + 1 ELSE p_ver
- /\ gp_ver' = IF r_gp_locked THEN gp_ver + 1 ELSE gp_ver
+ /\ p_ver' = IF r_parent_locked \/ (r_cpp_locked /\ r_cut_level = 2)
+ THEN p_ver + 1 ELSE p_ver
+ /\ gp_ver' = IF r_gp_locked \/ (r_cpp_locked /\ r_cut_level = 1)
+ THEN gp_ver + 1 ELSE gp_ver
/\ root_ver' = IF r_cpp_locked /\ r_cut_level = 0 THEN root_ver + 1 ELSE root_ver
/\ r_chain_locked' = FALSE /\ r_parent_locked' = FALSE
/\ r_gp_locked' = FALSE /\ r_cpp_locked' = FALSE
/\ rpc' = "idle"🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCChainCutFull.tla` around lines 296 - 307, RRestart currently only
clears r_parent_locked and r_gp_locked, so when the parent or grandparent were
locked as the CPP (set via RUpgradeParent/RUpgradeGP using r_cpp_locked and
r_cut_level) they remain locked after restart; update RRestart to also clear the
CPP-derived locks by checking r_cpp_locked and r_cut_level: if r_cpp_locked and
r_cut_level = 2 treat the parent as unlocked (clear the parent/CPP lock state
for the parent), and if r_cpp_locked and r_cut_level = 1 treat the grandparent
as unlocked (clear the gp/CPP lock state for the grandparent); modify the
RRestart transition to include these additional conditions when resetting lock
flags (refer to RRestart, r_parent_locked, r_gp_locked, r_cpp_locked, and
r_cut_level) so restart always releases parent/gp CPP locks.
| -cp ~/tools/tla/tla2tools.jar tlc2.TLC \ | ||
| "$tla" -config "$cfg" -workers 4 \ | ||
| -metadir /tmp/tlc-run -noGenerateSpecTE 2>&1) | ||
| local rc=$? |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial | ⚡ Quick win
Remove unused variable.
rc captures the exit code but is never used. The script correctly checks TLC's output instead, making this variable unnecessary.
🧹 Proposed fix
- local rc=$?
+ # Note: exit code ignored; TLC success is determined by output message📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| local rc=$? | |
| # Note: exit code ignored; TLC success is determined by output message |
🧰 Tools
🪛 Shellcheck (0.11.0)
[warning] 19-19: rc appears unused. Verify use (or export if used externally).
(SC2034)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/run-all-stages.sh` at line 19, Remove the unused local variable
assignment "local rc=$?" from spec/tla/run-all-stages.sh; locate the assignment
(the "rc" variable) and delete that line so the script no longer creates an
unused variable—no further logic changes needed since the script already checks
TLC's output directly.
Source: Linters/SAST tools
| rm -rf /tmp/tlc-run | ||
| if echo "$output" | grep -q "No error has been found"; then | ||
| local states | ||
| states=$(echo "$output" | grep "distinct states found" | grep -oP "\\d+ distinct" | tail -1) |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial | 💤 Low value
Grep -P requires GNU grep.
The -P flag (Perl regex) is a GNU extension not available in macOS default grep. Consider documenting this dependency or using POSIX regex instead.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/run-all-stages.sh` at line 23, The shell uses grep -P in the
assignment to the variable states which relies on GNU grep; replace the
Perl-regex usage by switching to a POSIX-compatible expression (use grep -oE and
replace \d with [0-9]+) in the command that generates states so the script works
on macOS without GNU grep; update the command that sets the states variable
accordingly (the line assigning to states in run-all-stages.sh).
Comment on lines
+85
to
+249
| ## Staged Model Design | ||
|
|
||
| ### Abstraction Principles | ||
|
|
||
| 1. **Model the protocol, not the data structure.** We don't need to model | ||
| actual key bytes or prefix compression. We model: nodes with slots, | ||
| version counters, and the lock protocol. | ||
|
|
||
| 2. **One hazard per stage.** Each stage targets one or two specific | ||
| interleavings. This keeps state space small and failures diagnosable. | ||
|
|
||
| 3. **Minimal domain.** Use the smallest constants that exercise the hazard: | ||
| typically 1-2 nodes, 2-3 slots, 1-2 values. | ||
|
|
||
| 4. **Bound version counters.** Version is modular — only even/odd and | ||
| same/different matter. Cap at 6 (3 full cycles). | ||
|
|
||
| 5. **Bound process counts.** 1 writer + 1 reader per stage (except H4/H5 | ||
| which need 2 writers). | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 1: VIS Slot Interpretation (Sequential) | ||
| **File:** `Inode256VIS.tla` — DONE ✓ | ||
| **Hazard:** H1 (foundation) | ||
| **What:** Single inode256, insert/remove values and pointers, verify scan predicates | ||
| **Domain:** N=4 slots, Values={0,1,2}, Pointers={-1,-2,-3,-4} | ||
| **Result:** 4,096 states, <1s. Correct predicate verified, buggy predicate violated. | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 2: OLC Single-Slot Protocol | ||
| **File:** `OLCSlot.tla` | ||
| **Hazard:** H1 + H6 (concurrent VIS modification) | ||
| **What:** 1 writer + 1 reader on a single slot. Writer modifies (slot, bitmask) | ||
| under version lock. Reader reads both, validates, interprets. | ||
| **Variables (7 scalars):** | ||
| - Shared: `slot`, `bitmask`, `version` | ||
| - Writer: `wpc` (idle|lock|write_slot|write_bitmask|unlock) | ||
| - Reader: `rpc` (idle|read_slot|read_bitmask|validate|interpret|done), `rslot`, `rbitmask` | ||
|
|
||
| **Domain:** slot ∈ {-1, 0, 1}, version ∈ 0..6 | ||
| **State constraint:** `version <= 6` | ||
| **Expected:** ~5K states, <5s | ||
| **Properties:** | ||
| - `NoDereferenceValue`: reader in "done" never has value in deref set | ||
| - `SnapshotConsistency`: if validate passes, (rslot, rbitmask) is a committed pair | ||
| - `WriterProtocol`: shared state only modified when version is odd | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 3: OLC Lock Coupling (Insert Path) | ||
| **File:** `OLCInsert.tla` | ||
| **Hazard:** H5 (two inserts racing for same slot) | ||
| **What:** 2 writers + 1 node with N=3 slots. Each writer: read version → find | ||
| empty slot → upgrade → write. Tests that only one succeeds. | ||
| **Variables (~10):** | ||
| - Shared: `slots[1..3]`, `version`, `count` | ||
| - Writer1: `w1pc`, `w1_target` | ||
| - Writer2: `w2pc`, `w2_target` | ||
|
|
||
| **Domain:** slots ∈ {0, 1} (empty/full), version ∈ 0..6 | ||
| **Expected:** ~50K states, <30s | ||
| **Properties:** | ||
| - `NoLostUpdate`: if both target same slot, exactly one succeeds | ||
| - `CountConsistency`: count always equals number of non-empty slots | ||
| - `MutualExclusion`: at most one writer holds write lock at a time | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 4: Chain Membership Under Concurrent Insert | ||
| **File:** `OLCChainMembership.tla` | ||
| **Hazard:** H2 (insert invalidates chain precondition) | ||
| **What:** 1 remover evaluating chain membership on an I4 node, 1 inserter | ||
| adding a child to that same I4. Models the revalidation pattern. | ||
| **Variables (~10):** | ||
| - Shared: `count` (1 or 2), `version` | ||
| - Remover: `rpc` (read_count|validate|upgrade|locked|done|restart), `r_cached_count`, `r_cached_ver` | ||
| - Inserter: `ipc` (idle|lock|insert|unlock) | ||
|
|
||
| **Domain:** count ∈ {1, 2}, version ∈ 0..6 | ||
| **Expected:** ~2K states, <5s | ||
| **Properties:** | ||
| - `ChainSafety`: remover never proceeds with cut when count=2 | ||
| - `ProgressUnderContention`: remover eventually either cuts or restarts | ||
| - `NoFalseChain`: if remover locks and proceeds, count was 1 at lock time | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 5: Chain Cut with Concurrent Insert (Cases A/B/C) | ||
| **File:** `OLCChainCut.tla` | ||
| **Hazard:** H2 + H4 (cut_point_parent evaluation under mutation) | ||
| **What:** A 3-node chain (parent → chain_node → leaf). Remover does upward | ||
| locking + CPP evaluation. Inserter can add children to parent or chain_node. | ||
| **Variables (~14):** | ||
| - Shared: `parent_count`, `chain_count`, `parent_ver`, `chain_ver`, `parent_child` (points to chain or null) | ||
| - Remover: `rpc` (lock_chain|eval_cpp|cut|done|restart), `cut_level`, `holds_chain_lock` | ||
| - Inserter: `ipc`, `i_target` (parent or chain) | ||
|
|
||
| **Domain:** counts ∈ {1,2,3}, version ∈ 0..6 | ||
| **Expected:** ~100K states, <60s | ||
| **Properties:** | ||
| - `WellFormedness`: after cut, no node has count < 1 (for I4 in key_view mode) | ||
| - `NoCutWithStaleView`: remover never cuts based on outdated count | ||
| - `CaseACorrect`: if parent has 2+ children including chain, cut proceeds | ||
| - `CaseBCorrect`: if parent became single-child, chain extends upward | ||
| - `CaseCCorrect`: if child pointer gone, remover restarts | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 6: Iterator × Concurrent Remove (Obsolescence) | ||
| **File:** `OLCIterRemove.tla` | ||
| **Hazard:** H3 + H7 (node obsolescence during scan) | ||
| **What:** 1 iterator descending/advancing, 1 remover that can obsolete a node. | ||
| Tests that iterator detects obsolescence and restarts. | ||
| **Variables (~12):** | ||
| - Shared: `nodes[1..2]` each with `{version, obsolete, child}` | ||
| - Iterator: `ipc`, `i_stack` (cached versions), `i_current` | ||
| - Remover: `rpc`, `r_target` | ||
|
|
||
| **Domain:** 2 nodes, version ∈ 0..6 | ||
| **Expected:** ~50K states, <30s | ||
| **Properties:** | ||
| - `NoUseAfterObsolete`: iterator never acts on data from an obsoleted node | ||
| - `RestartOnObsolete`: if rehydrate finds obsolete, iterator restarts | ||
| - `ProgressAfterRestart`: iterator eventually re-seeks and advances | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 7: Insert Chain × Scan (VIS Transient State) | ||
| **File:** `OLCInsertChainVIS.tla` | ||
| **Hazard:** H6 (set_value_bit → overwrite → clear_value_bit sequence) | ||
| **What:** 1 writer performing the chain-insert protocol (4 steps under one | ||
| write lock), 1 reader scanning. Verifies reader never sees the transient | ||
| state where bitmask=TRUE but slot holds a chain pointer. | ||
| **Variables (~10):** | ||
| - Shared: `slot`, `bitmask`, `version` | ||
| - Writer: `wpc` (lock|set_bit|write_chain|clear_bit|unlock) | ||
| - Reader: `rpc`, `rslot`, `rbitmask`, `rver` | ||
|
|
||
| **Domain:** slot ∈ {0, "chain_ptr", "packed_val"}, version ∈ 0..6 | ||
| **Expected:** ~3K states, <5s | ||
| **Properties:** | ||
| - `NoTransientVisible`: reader in "done" never sees (bitmask=TRUE, slot=chain_ptr) | ||
| - `ProtocolCovers`: all 4 writer steps are under one version lock | ||
|
|
||
| --- | ||
|
|
||
| ### Stage 8: Remove × Remove (Double Cut Prevention) | ||
| **File:** `OLCDoubleCut.tla` | ||
| **Hazard:** H4 (two removes targeting same chain) | ||
| **What:** 2 removers, 1 chain of 2 nodes. Both try to lock the chain bottom-up. | ||
| Only one can succeed at upgrading; the other sees version change. | ||
| **Variables (~12):** | ||
| - Shared: `chain_ver`, `chain_obsolete`, `parent_ver`, `parent_child` | ||
| - Remover1: `r1pc`, `r1_holds_lock` | ||
| - Remover2: `r2pc`, `r2_holds_lock` | ||
|
|
||
| **Domain:** version ∈ 0..8 (need more cycles for 2 writers) | ||
| **Expected:** ~20K states, <15s | ||
| **Properties:** | ||
| - `AtMostOneCut`: at most one remover reaches point-of-no-return | ||
| - `LoserRestarts`: the other remover detects conflict and restarts | ||
| - `NoDoubleFree`: a node is obsoleted at most once | ||
|
|
Contributor
There was a problem hiding this comment.
Document stages 9-12.
The plan documents only 8 stages but the verification suite includes 12. Missing:
- Stage 9: OLCChainMultiLevel
- Stage 10: OLCChainCutFull
- Stage 11: OLCKeyViewChain (discovered bug
#850) - Stage 12: ARTTreeMaintenance
These stages are executed by run-all-stages.sh and referenced in the PR objectives, but their domains, properties, and expected state counts are undocumented.
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 107-107: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 116-116: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 136-136: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 155-155: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 174-174: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 195-195: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 214-214: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
[warning] 233-233: Headings should be surrounded by blank lines
Expected: 1; Actual: 0; Below
(MD022, blanks-around-headings)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/staged-model-plan.md` around lines 85 - 249, The spec is missing
documentation for stages 9-12 referenced by run-all-stages.sh and the PR
objectives; add entries for OLCChainMultiLevel.tla, OLCChainCutFull.tla,
OLCKeyViewChain.tla (bug `#850`), and ARTTreeMaintenance.tla specifying for each:
hazard(s), brief description of "What", variables/roles (unique names like
multi-level shared arrays, parent/child versions, key_view flags), bounded
domains (slot/count/version ranges), key properties to verify (safety/progress
invariants), and expected state counts/runtime; update the stage index and any
PR objective text to reference these filenames and the discovered bug number
consistently so the plan and run-all-stages.sh remain in sync.
Comment on lines
+252
to
+266
| ## Verification Matrix | ||
|
|
||
| | Stage | Hazards | Slots | Procs | Est. States | Time | Key Property | | ||
| |-------|---------|-------|-------|-------------|------|--------------| | ||
| | 1 ✓ | H1 | 4 | 0 | 4K | <1s | Scan completeness | | ||
| | 2 | H1,H6 | 1 | 1W+1R | ~5K | <5s | No value-as-ptr | | ||
| | 3 | H5 | 3 | 2W | ~50K | <30s | No lost update | | ||
| | 4 | H2 | 1 | 1W+1R | ~2K | <5s | Chain membership | | ||
| | 5 | H2,H4 | — | 1W+1R | ~100K | <60s | Cut correctness | | ||
| | 6 | H3,H7 | — | 1W+1R | ~50K | <30s | No use-after-obsolete | | ||
| | 7 | H6 | 1 | 1W+1R | ~3K | <5s | No transient visible | | ||
| | 8 | H4 | — | 2W | ~20K | <15s | At-most-one cut | | ||
|
|
||
| **Total estimated time:** <4 minutes for all 8 stages. | ||
|
|
Contributor
There was a problem hiding this comment.
Update matrix to include all 12 stages.
The matrix shows only 8 stages and estimates <4 minutes total, but the suite actually runs 12 stages. The time estimate is incorrect without stages 9-12.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/staged-model-plan.md` around lines 252 - 266, The Verification
Matrix currently lists only stages 1–8 and an incorrect total time; update the
matrix table under the "Verification Matrix" heading to include rows for stages
9–12 (fill in Hazards, Slots, Procs, Est. States, Time, and Key Property
consistent with the other rows or the test plan), and adjust the "**Total
estimated time:**" summary to reflect the full runtime for all 12 stages; locate
the table by the "Verification Matrix" header and the final "Total estimated
time" line in staged-model-plan.md when making the edits.
| | Prefix capacity | 2 | Exercises both collapse-success (combined ≤ 2) and collapse-blocked (combined > 2) | | ||
| | Tree representation | `node_id → {prefix, children, is_vis}` | Minimal record per node | | ||
| | Operations | `Insert(key)`, `Remove(key)` non-deterministic | Full insert/remove interleaving | | ||
| | StateConstraint | nxt ≤ 8 (max 7 nodes) | Keeps state space at ~5000 | |
Contributor
There was a problem hiding this comment.
Fix state constraint value.
States nxt ≤ 8 but ARTTreeMaintenance.tla line 438 defines StateConstraint == nxt <= 7. The actual constraint is 7, not 8.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/tree-structure-model-design.md` at line 69, The table entry
incorrectly lists StateConstraint as "nxt ≤ 8 (max 7 nodes)" while the actual
constant is StateConstraint == nxt <= 7 in ARTTreeMaintenance (symbol:
StateConstraint); update the markdown row to "nxt ≤ 7 (max 7 nodes)" so the doc
matches the implementation and retains the same note "Keeps state space at
~5000".
added 6 commits
June 11, 2026 15:31
- OLCIterator.tla: Base model — forward scan with seek-restart, parametric ConcurrencyEnabled (db vs olc_db). Verifies OrderPreservation, NoRepeat, Completeness. 96K states in OLC mode. - OLCIterator_Bug850.tla: Bug injection suite — skip_backtrack catches unodb-dev#850 (Completeness violated), restart_from_beginning catches NoRepeat. - OLCIteratorRemove.tla: Phase 1 — structural remove with havoc model. Writer removes L2, collapses inode A. Correct code passes all invariants. skip_check bug triggers OrderPreservation violation via non-deterministic stale read (havoc pattern). All three bug classes now caught.
OLCIteratorVIS.tla: Models the critical section where an iterator reads a packed leaf (value-in-slot) from a parent inode. Packed leaves have no version lock — the parent's version protects them via check2. Correct code (BugMode=none): 67 states, all properties pass. Bug injection (skip_check2): NoGarbage violated — havoc delivers invalid value when writer mutates slot between check1 and skipped check2. Canary (SlotNeverMutated): proves writer interleaves with iterator. Also adds iterator-model-plan.md with revised phase plan.
OLCIteratorRoot.tla: Models the two-level locking protocol at the root. root_pointer_lock protects the root pointer variable, node version lock protects node contents. Writer can empty tree (root→null) between iterator's load and check. Correct code: 61 states, all properties pass. Bug (skip_rp_check): NoActOnInvalid violated — iterator acts on freed/null root when root_pointer_lock check is skipped. Canary (RootNeverNull): proves writer empties tree.
run-iterator-validation.sh: Runs all iterator specs in all configs, verifies expected pass/fail for correct code, bug injection, and canaries. Bug coverage matrix: - skip_backtrack → Completeness violated - restart_from_beginning → NoRepeat violated - skip_check + structural mutation → OrderPreservation violated (havoc) - skip_check2 on VIS slot → NoGarbage violated - skip_rp_check on root → NoActOnInvalid violated Also fixes OLCIteratorRemove_Canary.cfg (missing BugMode constant).
Contributor
There was a problem hiding this comment.
Actionable comments posted: 6
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@spec/tla/iterator-model-plan.md`:
- Around line 40-45: The fenced code block under "Iterator state machine:" is
missing blank lines and a language tag; update the markdown so there is a blank
line before and after the fence and specify a language (use "text") for the
diagram code block containing the state sequence ("start → snap_ver → at_L1 →
... restart") and ensure the closing triple-backticks are present on their own
line.
In `@spec/tla/OLCIterator.tla`:
- Around line 316-324: The NoStaleAct invariant currently only checks ipc \in
{"advance", "descend"} but omits the "descend_lm" action used by IterDescendLM;
update NoStaleAct to include "descend_lm" in the ipc set so it covers the same
stack/version checks as IterDescendLM (i.e., change the guard to ipc \in
{"advance", "descend", "descend_lm"} and keep the existing LET top ==
stack[Len(stack)] IN CheckOK(top.node, top.ver) logic).
In `@spec/tla/OLCIteratorRoot.tla`:
- Around line 181-192: NoActOnInvalid and NoGarbage are redundant because
NoActOnInvalid (visited[i] ∈ {"L","N"}) already excludes "freed", so remove the
weaker invariant NoGarbage or merge their intent: delete NoGarbage and keep
NoActOnInvalid (or replace both with a single invariant that explicitly states
visited[i] ∈ {"L","N"}), and update any references to NoGarbage to use
NoActOnInvalid (or the new combined invariant) so proofs and uses refer to the
single canonical invariant; reference symbols: NoActOnInvalid, NoGarbage,
visited.
In `@spec/tla/run-iterator-validation.sh`:
- Line 7: Remove the unused FAIL variable from the script: replace the current
initialization "PASS=0; FAIL=0; ERRORS=0" with only "PASS=0; ERRORS=0", and
ensure there are no remaining references to FAIL elsewhere in the script (e.g.,
any checks or increments) before committing the change.
- Line 4: The script currently runs cd "$(dirname "$0")" without checking its
result; if that cd fails the rest of the script runs in the wrong directory.
Update the invocation of cd "$(dirname "$0")" to handle failures (e.g. test the
exit status and exit with a non‑zero code or print an error before exiting) so
the script stops immediately when the directory change fails and does not
continue to run TLC commands in the wrong location.
- Line 27: The grep regex string in run-iterator-validation.sh uses an unescaped
backslash ("\\d+ distinct" should be used) causing inconsistent escape style
versus run-all-stages.sh; update the command that assigns to the variable states
(the line using states=$(echo "$output" | grep "distinct states found" | grep
-oP "\d+ distinct" | tail -1)) to use "\\d+ distinct" in the grep -oP argument
so the backslash is escaped consistently with the other stage runner script.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: dd5266dd-45e2-41ea-8bfb-457abff0b484
📒 Files selected for processing (22)
.gitignorespec/tla/OLCIterator.tlaspec/tla/OLCIteratorRemove.tlaspec/tla/OLCIteratorRemove_Canary.cfgspec/tla/OLCIteratorRemove_OLC.cfgspec/tla/OLCIteratorRemove_SkipCheck.cfgspec/tla/OLCIteratorRoot.cfgspec/tla/OLCIteratorRoot.tlaspec/tla/OLCIteratorRoot_Bug.cfgspec/tla/OLCIteratorRoot_Canary.cfgspec/tla/OLCIteratorVIS.cfgspec/tla/OLCIteratorVIS.tlaspec/tla/OLCIteratorVIS_Bug.cfgspec/tla/OLCIteratorVIS_Canary.cfgspec/tla/OLCIterator_Bug850.tlaspec/tla/OLCIterator_Bug850_Backtrack.cfgspec/tla/OLCIterator_Bug850_NoSeek.cfgspec/tla/OLCIterator_Bug850_SkipCheck.cfgspec/tla/OLCIterator_OLC.cfgspec/tla/OLCIterator_Seq.cfgspec/tla/iterator-model-plan.mdspec/tla/run-iterator-validation.sh
Comment on lines
+40
to
+45
| **Iterator state machine:** | ||
| ``` | ||
| start → snap_ver → at_L1 → check1 → read_slot2 → check2 → deliver → at_L3 → done | ||
| ↓ (fail) | ||
| restart | ||
| ``` |
Contributor
There was a problem hiding this comment.
Fix markdown formatting around code fence.
Fenced code blocks should have blank lines before and after, and should specify a language (or "text" for ASCII diagrams).
📝 Proposed fix
**Iterator state machine:**
+
-```
+```text
start → snap_ver → at_L1 → check1 → read_slot2 → check2 → deliver → at_L3 → done
↓ (fail)
restart</details>
<!-- suggestion_start -->
<details>
<summary>📝 Committable suggestion</summary>
> ‼️ **IMPORTANT**
> Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
```suggestion
**Iterator state machine:**
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 41-41: Fenced code blocks should be surrounded by blank lines
(MD031, blanks-around-fences)
[warning] 41-41: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/iterator-model-plan.md` around lines 40 - 45, The fenced code block
under "Iterator state machine:" is missing blank lines and a language tag;
update the markdown so there is a blank line before and after the fence and
specify a language (use "text") for the diagram code block containing the state
sequence ("start → snap_ver → at_L1 → ... restart") and ensure the closing
triple-backticks are present on their own line.
Comment on lines
+316
to
+324
| \* NoStaleAct: if we're in "advance" or "descend" and acting on a stack entry, | ||
| \* that entry's version must still be current (OLC safety). | ||
| \* Note: This is implicitly enforced by CheckOK guards, but we verify it. | ||
| NoStaleAct == | ||
| (ipc \in {"advance", "descend"} /\ stack /= <<>>) => | ||
| LET top == stack[Len(stack)] IN | ||
| CheckOK(top.node, top.ver) | ||
| \* This is checked by the guards; if violated, we restart. | ||
| \* The real invariant is: we never append to visited[] with stale data. |
Contributor
There was a problem hiding this comment.
NoStaleAct invariant is incomplete.
Line 320 checks ipc \in {"advance", "descend"} but omits "descend_lm". IterDescendLM also manipulates the stack and checks versions (line 241), so the invariant should verify that path too for completeness.
Suggested fix
NoStaleAct ==
- (ipc \in {"advance", "descend"} /\ stack /= <<>>) =>
+ (ipc \in {"advance", "descend", "descend_lm"} /\ stack /= <<>>) =>
LET top == stack[Len(stack)] IN
CheckOK(top.node, top.ver)🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCIterator.tla` around lines 316 - 324, The NoStaleAct invariant
currently only checks ipc \in {"advance", "descend"} but omits the "descend_lm"
action used by IterDescendLM; update NoStaleAct to include "descend_lm" in the
ipc set so it covers the same stack/version checks as IterDescendLM (i.e.,
change the guard to ipc \in {"advance", "descend", "descend_lm"} and keep the
existing LET top == stack[Len(stack)] IN CheckOK(top.node, top.ver) logic).
Comment on lines
+181
to
+192
| NoActOnInvalid == | ||
| \A i \in 1..Len(visited) : visited[i] \in {"L", "N"} | ||
|
|
||
| \* SafeEmpty: if tree is empty when iterator finishes, visited is empty | ||
| \* (iterator correctly detected null and returned end()) | ||
| \* Note: if tree was non-empty when iterator started, it's fine to visit it | ||
| \* even if it was emptied later (snapshot consistency). | ||
|
|
||
| \* The key safety property: iterator never dereferences a stale root pointer | ||
| \* that points to freed memory. In our model, "freed" = garbage value. | ||
| NoGarbage == | ||
| \A i \in 1..Len(visited) : visited[i] /= "freed" |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial | 💤 Low value
Invariants NoActOnInvalid and NoGarbage are logically redundant.
NoActOnInvalid requires visited[i] ∈ {"L", "N"}, which inherently excludes both "null" and "freed". NoGarbage only checks visited[i] ≠ "freed", making it strictly weaker. While maintaining both can serve pedagogical purposes (documenting the specific concern about freed memory separately from null handling), consider whether the duplication adds enough clarity to justify the extra invariant.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/OLCIteratorRoot.tla` around lines 181 - 192, NoActOnInvalid and
NoGarbage are redundant because NoActOnInvalid (visited[i] ∈ {"L","N"}) already
excludes "freed", so remove the weaker invariant NoGarbage or merge their
intent: delete NoGarbage and keep NoActOnInvalid (or replace both with a single
invariant that explicitly states visited[i] ∈ {"L","N"}), and update any
references to NoGarbage to use NoActOnInvalid (or the new combined invariant) so
proofs and uses refer to the single canonical invariant; reference symbols:
NoActOnInvalid, NoGarbage, visited.
| #!/bin/bash | ||
| # Run all TLA+ iterator model specs and verify expected results. | ||
| # Each spec has: correct config (must PASS), bug config (must FAIL), canary config (must FAIL). | ||
| cd "$(dirname "$0")" |
Contributor
There was a problem hiding this comment.
Add error handling for cd command.
If cd fails, the script will continue in the wrong directory, causing all TLC invocations to fail unexpectedly.
🛡️ Proposed fix
-cd "$(dirname "$0")"
+cd "$(dirname "$0")" || exit 1📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| cd "$(dirname "$0")" | |
| cd "$(dirname "$0")" || exit 1 |
🧰 Tools
🪛 Shellcheck (0.11.0)
[warning] 4-4: Use 'cd ... || exit' or 'cd ... || return' in case cd fails.
(SC2164)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/run-iterator-validation.sh` at line 4, The script currently runs cd
"$(dirname "$0")" without checking its result; if that cd fails the rest of the
script runs in the wrong directory. Update the invocation of cd "$(dirname
"$0")" to handle failures (e.g. test the exit status and exit with a non‑zero
code or print an error before exiting) so the script stops immediately when the
directory change fails and does not continue to run TLC commands in the wrong
location.
| cd "$(dirname "$0")" | ||
|
|
||
| RED='\033[0;31m'; GREEN='\033[0;32m'; YELLOW='\033[0;33m'; NC='\033[0m' | ||
| PASS=0; FAIL=0; ERRORS=0 |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial | ⚡ Quick win
Remove unused FAIL variable.
FAIL is declared but never used—only PASS and ERRORS track results.
♻️ Proposed fix
-PASS=0; FAIL=0; ERRORS=0
+PASS=0; ERRORS=0📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| PASS=0; FAIL=0; ERRORS=0 | |
| PASS=0; ERRORS=0 |
🧰 Tools
🪛 Shellcheck (0.11.0)
[warning] 7-7: FAIL appears unused. Verify use (or export if used externally).
(SC2034)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/run-iterator-validation.sh` at line 7, Remove the unused FAIL
variable from the script: replace the current initialization "PASS=0; FAIL=0;
ERRORS=0" with only "PASS=0; ERRORS=0", and ensure there are no remaining
references to FAIL elsewhere in the script (e.g., any checks or increments)
before committing the change.
| if [ "$expect" = "pass" ]; then | ||
| if [ "$found_error" = "false" ] && echo "$output" | grep -q "No error has been found"; then | ||
| local states | ||
| states=$(echo "$output" | grep "distinct states found" | grep -oP "\d+ distinct" | tail -1) |
Contributor
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial | ⚡ Quick win
Match regex escape style with run-all-stages.sh.
Use "\\d+ distinct" instead of "\d+ distinct" for consistency with the existing stage runner script.
♻️ Proposed fix
- states=$(echo "$output" | grep "distinct states found" | grep -oP "\d+ distinct" | tail -1)
+ states=$(echo "$output" | grep "distinct states found" | grep -oP "\\d+ distinct" | tail -1)📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| states=$(echo "$output" | grep "distinct states found" | grep -oP "\d+ distinct" | tail -1) | |
| states=$(echo "$output" | grep "distinct states found" | grep -oP "\\d+ distinct" | tail -1) |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@spec/tla/run-iterator-validation.sh` at line 27, The grep regex string in
run-iterator-validation.sh uses an unescaped backslash ("\\d+ distinct" should
be used) causing inconsistent escape style versus run-all-stages.sh; update the
command that assigns to the variable states (the line using states=$(echo
"$output" | grep "distinct states found" | grep -oP "\d+ distinct" | tail -1))
to use "\\d+ distinct" in the grep -oP argument so the backslash is escaped
consistently with the other stage runner script.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
12-stage TLA+ formal verification suite modeling the concurrency protocol for OLC ART tree operations. Each stage builds incrementally on the previous, from single-slot VIS through multi-level chain cuts.
Stages
Bug discoveries
Testing
bash spec/tla/run-all-stages.sh # All 12 stages passFiles
All changes are in
spec/tla/— no production code changes.Summary by CodeRabbit
New Features
Tests
Documentation