TLA+ verification suite for OLC ART tree maintenance#3
Open
thompsonbry wants to merge 14 commits into
Open
Conversation
Owner
Author
Trident Review: TLA+ OLC ART Verification SuiteThree expert reviewers evaluated this specification suite. Summary below. TLA+ Expert Review2 Critical, 4 Major, 5 Minor findings.
Concurrency Expert ReviewNo algorithm bugs found. 3 medium verification gaps identified.
Stage 6 QSBR finding confirmed correct: Iterator acting on disconnected node is safe under QSBR contract. Four conditions for unsafety identified — all prevented by protocol or are user-contract violations. ART Domain Expert Review2 medium-priority gaps, 3 confirmed adequate.
Consolidated Action Items (Priority Order)
VerdictThe specification suite correctly identifies and verifies the critical safety hazards. The staged approach is sound. The models need strengthening (items 1-5 above) before they provide full confidence, but no algorithm bugs were found — all findings are model-quality improvements, not flaws in the OLC ART algorithm itself. |
thompsonbry
force-pushed
the
feat/tla-olc-art-verification
branch
2 times, most recently
from
May 6, 2026 21:25
5e98e7d to
1ae4b39
Compare
Owner
Author
Review Iteration CompleteAll findings from the trident review have been addressed:
All 8 stages pass. Total: 21,980 distinct states, <5s. |
Owner
Author
Second Review Pass — CorrectionThe second-pass reviewers read stale files from the working tree rather than the committed branch. The fixes ARE present in the committed code (verified by
All 8 stages pass with the committed code. Valid Finding from ART Domain ReviewerPotential live bug at olc_art.hpp:3417 — the OLC |
Owner
Author
Incremental Expansion: Stage 6Added a normal writer process to Stage 6 (OLCIterRemove). This exercises the scenario where a concurrent INSERT bumps a node's version without obsoleting it — the iterator must detect this via version mismatch and restart. Before: 96 distinct states (only remover/obsoleter)
Stage 8 (OLCDoubleCut) already has cycling in the committed version (8 states is correct for the minimal domain — the node can only be cut once, so the second remover always fails). To expand Stage 8 meaningfully would require modeling 2 separate chain nodes, which is a different hazard (already covered by Stage 5's parent+chain structure). |
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
thompsonbry
force-pushed
the
feat/tla-olc-art-verification
branch
from
June 11, 2026 14:42
5c1aff5 to
f235f54
Compare
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).
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.
8 staged TLA+ models verifying OLC ART correctness under concurrent insert/remove/scan. All pass (21,598 states, <5s).
Hazards verified: VIS value=0 bug (H1), chain membership race (H2), node obsolescence (H3), double-cut (H4), insert race (H5), transient VIS (H6), shrink during scan (H7).
Key finding: Stage 6 reveals the QSBR window — iterator can act on disconnected node. Safe by design (QSBR prevents reclamation).
Context: Supports VIS 64-bit clean fix (PR unodb-dev#845 item unodb-dev#9). Validates bitmask-only encoding before implementation.
Run:
bash spec/tla/run-all-stages.sh(requires tla2tools.jar)