Repository navigation
javascript engine under -j8 on darwin-arm64: segfault in a varying rule under memory-pressure load #1869
Description
Activity
Closes #1869 — the parallel-solve crash is root-caused, captured, fixed and validated against a live reproduction.
The capture (lldb, java
-j8, darwin-arm64, under asouffle -gmemory-load loop — the missing repro ingredient):thread #5, EXC_BAD_ACCESS (code=1, address=0x8) frame #0: souffle::detail::btree<...>::insert(...) + 704 -> ldapr w8, [x8] ; acquire-load of a seqlock version at null+8insert's descent readsnext = cur->getChild(idx)under a still-unvalidated optimistic lease and immediately dereferences it (next->lock.start_read()). A concurrent split can expose a null child slot; x86's ordering keeps the window closed, arm64 under memory pressure opens it. This explains every observation: javascript 3/10 and java 2/4 crash rates, a different rule each time, arm64-only, pressure-gated, serial always clean.The fix (overlay
seqlock-fix-4, engine-id salted): a null child is treated as a failed validation and the insert restarts — the same contract the descent already follows for torn reads. Applied toBTree.handBTreeDelete.h. Defense in depth in the same overlay: the flyweightfetchtolerates speculative indices (static empty value) and generic recordunpackreturns zeroed storage rather than an empty record's nulldata().Validation, 1.2M-LOC java subject, interleaved runs under the identical load loop:
engine segfaults fix-3 (unfixed), -j88/10 fix-4, -j80/10 and fix-4 serial AND parallel outputs are sorted-identical to the fix-3 serial reference across every relation. The engine-package stub test carries the new anchors (green), and build-engines.yml applies the same awk-extracted patch with per-file assertions — its awk anchor is also repaired (the heredoc's import line had drifted under it, which would have failed the next release build loudly).
With this in, the parallel-by-default gate from #1861 stands safely for 0.1.9.
Symptom
The javascript engine built with OpenMP and run
-j8on darwin-arm64 exits ~3/10 with(observed in rules from three different files across three failures). The varying location means a shared data structure is being corrupted, not a rule defect. Exit code 1; Soufflé's own signal handler reports the rule, so no crash dump is produced.
Conditions
Why javascript specifically
Among the five engines, only the javascript program creates new symbols during the solve (
substr/catchains in its module-resolution rules). The other four mostly probe symbols that already exist in the facts. That makes concurrent symbol-table insertion (ConcurrentInsertOnlyHashMap/ the symbol table's publication path) the prime suspect: the seqlock/publication-fence overlay applied for the earlier arm64 crashes fences the BTree only.Repro
On an arm64 Mac, stage a large javascript subject's facts, build the
-parflavor (AXIOM_SOLVE_PARALLEL=1 run-souffle.sh --language javascript --prepare), then run the engine-j 8in a loop while twoclang++ -O1 -fsyntax-onlycompiles of a ~9MB generated C++ file loop beside it. Expect a failure within ~10 runs.Impact
Parallel default was flipped to opt-in (serial default everywhere) until this is fenced; measured opt-in value on quiet arm64 hardware is 1.5–3x on top of the current rules, so the fix is worth having.