Testing-depth release. Closes the FoundationDB-parity gaps in the Deterministic Simulation Testing (DST) fault-class taxonomy and adds a formal-verification tier. The single-node transactional core is now exercised by unit + DST + PBT + fuzz + malloc-injection + static/ABI + CBMC.
New DST fault classes
All zero-overhead when --enable-dst is off (CI enforces 0 __db_sim_* symbols in a normal build).
- Buggify — 9 legal-but-pessimal points at real library sites (FoundationDB's signature technique) so rare/slow paths run constantly; 0 invariant violations with all forced on.
- Clock-skew / time-jump at the
__os_gettimeseam — 3 scenarios (forward, backward, jitter); proved BDB's timers tolerate a non-monotonic clock. - Crash-during-recovery — 4 scenarios incl. a reboot-loop convergence capstone; recovery proven idempotent + convergent across every interruption point.
- Multi-process process-death + failchk pilot (BDB's differentiator) — a killed process's locks/txn are recovered by a survivor.
DST surface: 41 single-process scenarios + a multi-process pilot, 9 planted bugs (all caught at K=1), 9 buggify points, 7 fault classes.
Formal verification
6 CBMC harnesses over the algorithmic cores (varint codec, byte-swaps, hash4, getlong, deadlock cycle-detection, okitem) — proved a real hash OOB read (the HPAGE_PTYPE macro missing parens around its argument, now fixed).
Property-based testing
Converted 64 toothless hegel_assume filters to real PBT_CHECK assertions across 9 files; +17 properties.
Bugs
- Fixed: the
HPAGE_PTYPEhash out-of-page read (found by CBMC). - Documented for focused follow-up:
failchkreturningEBUSY(a dead process's DB-handle mutex left unrecovered via a clobberedTHREAD_FAILCHKmarker); a deadCLOCK_MONOTONICbranch inos_clock.c.
North star intact
Embedded, no server, ACID + WAL + recovery, all four access methods (B-tree/Hash/Queue/Recno), multi-process shared regions, on-disk/log/ABI format stability, tiny footprint.
CI
Green across the full matrix (Linux/macOS × gcc/clang × 6 configs, 32-bit, ASan/UBSan, TSan, all mutex backends, meson, nix flake, TCL, fuzz, PBT, Coccinelle+ABI, faultinject). The best-effort windows msbuild job (legacy VS solution) is non-gating.