Skip to content

Fix optimistic locking under weak memory ordering - #2581

Open
quentin wants to merge 3 commits into
souffle-lang:masterfrom
quentin:weak-mem-ordering
Open

Fix optimistic locking under weak memory ordering#2581
quentin wants to merge 3 commits into
souffle-lang:masterfrom
quentin:weak-mem-ordering

Conversation

@quentin

@quentin quentin commented May 10, 2026

Copy link
Copy Markdown
Member

Reproduced the crash described in #2476 on Apple Mac mini M2 on macOS Sequoia 15.6.

Test cprog4 only use b-tree, no symbol table nor record table, so the issue is definitely not in ConcurrentFlyweight as proposed in the issue description.

I built souffle and cprog4 in RelWithDebugInfo mode. Then run cprog4 in a loop until it crashed and created a core dump:

# enable core dumps
ulimit -c unlimited
sudo sysctl -w kern.coredump=1
sudo sysctl -w kern.corefile="$PWD/core.%P"

# build cprog4
souffle "-D" "." "-F" "tests/evaluation/cprog4/facts" "tests/evaluation/cprog4/cprog4.dl" -o cprog4 -j 8 -v

# rerun the g++ command printed by the previous command, adding '-g' at the end
/opt/homebrew/bin/g++-15 ... -g

# sign with debugging entitlement
/usr/libexec/PlistBuddy -c \
  "Add :com.apple.security.get-task-allow bool true" \
  debug.entitlements
codesign -s - -f --entitlements debug.entitlements ./cprog4

# SOUFFLE_ALLOW_SIGNALS=1 prevents souffle from handling signals 
while SOUFFLE_ALLOW_SIGNALS=1 ./cprog4 -j 16 "-D" "-" "-F" tests/evaluation/cprog4 ; do
  date
done

# after a core.PID file is produced:
lldb cprog4 -core core.PID

With lldb pointing to the crashing location in BTree.h I used gpt-5.5 to investigate possible concurrency issues in Souffle's b-tree and optimistic RW lock implementations, under the assumption of aarch64 weak memory consistency. It created a first fix.

Then I found a similar sporadic crash in test_binary_relation, again lldb helped me pinpointing the exact location of the crash in the btree::find function and gpt-5.5 created a second fix.

Both fixes were validated on the same Apple Mac mini M2.

Fix #2476

quentin added 3 commits May 10, 2026 08:19
- `BTree.h:1246` dereferences `next` before the parent lease is validated.
- During concurrent insert/split, the reader can compute `idx` from one
  snapshot and read `children[idx]` from a partially
  visible later snapshot.
- On aarch64, weaker store visibility makes this much more
  plausible: `numElements` can become observable before the
  matching child slot is safely observable to a stale optimistic
  reader.
- `OptimisticReadWriteLock` is also too weak for this
  seqlock-style usage, especially around validation
  and writer publication.
- takes a root lease before reading root
- takes a node lease before reading keys, numElements, and children
- validates the node lease before returning found/not-found
- validates the parent after taking the child lease
- restarts if a child pointer is null from an invalidated snapshot
@codecov

codecov Bot commented May 10, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 75.75758% with 16 lines in your changes missing coverage. Please review.
✅ Project coverage is 81.23%. Comparing base (c3861e0) to head (85e5fd0).

Files with missing lines Patch % Lines
src/include/souffle/datastructure/BTree.h 80.76% 10 Missing ⚠️
src/include/souffle/datastructure/BTreeDelete.h 25.00% 3 Missing ⚠️
src/include/souffle/datastructure/LambdaBTree.h 25.00% 3 Missing ⚠️
Additional details and impacted files

Impacted file tree graph

@@            Coverage Diff             @@
##           master    #2581      +/-   ##
==========================================
- Coverage   81.25%   81.23%   -0.02%     
==========================================
  Files         492      492              
  Lines       31009    31047      +38     
==========================================
+ Hits        25195    25222      +27     
- Misses       5814     5825      +11     
Files with missing lines Coverage Δ
src/include/souffle/utility/ParallelUtil.h 84.82% <100.00%> (ø)
src/include/souffle/datastructure/BTreeDelete.h 53.01% <25.00%> (-0.16%) ⬇️
src/include/souffle/datastructure/LambdaBTree.h 80.00% <25.00%> (-0.92%) ⬇️
src/include/souffle/datastructure/BTree.h 87.95% <80.76%> (-1.82%) ⬇️

... and 3 files with indirect coverage changes

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@quentin
quentin force-pushed the weak-mem-ordering branch from 85e5fd0 to ecb775c Compare May 10, 2026 17:50
@quentin
quentin marked this pull request as ready for review May 11, 2026 19:03
* referencing its position. If not found, an end-iterator will be returned.
*/
iterator find(const Key& k, operation_hints& hints) const {
#ifdef IS_PARALLEL

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this method is not intended to be thread-safe. It is used when no write operations are in progress, or at least was intended to be. EqRel uses BTree out of the expected environment, and is not protecting it from modification.

I think it would be better to modify EqRel instead, and leave Btree.find() as is - not thread-safe, but fast. I explored this with mmcgr@47e8558
which seems to work.

Comment on lines +1298 to +1300
if (cur->lock.validate(cur_lease)) {
assert(false && "B-tree inner node has null child");
}

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe simplify these to

Suggested change
if (cur->lock.validate(cur_lease)) {
assert(false && "B-tree inner node has null child");
}
assert(!cur->lock.validate(cur_lease) && "B-tree inner node has null child");


// set last bit => make it odd
auto v = version.fetch_or(0x1, std::memory_order_acquire);
auto v = version.fetch_or(0x1, std::memory_order_acq_rel);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are the memory order changes necessary? They would have protected against the missing nullptr check in BTree, but that wasn't a problem with the lock itself. Adding the nullptr check is enough to avoid the crashes.

I'm not entirely confident that I've understood the necessary ordering when we're doing optimistic writing, so I'm also fine with the change as it makes it easier to be clear on the order of the operations.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

concurrency-related sporadic crashes on ARM architecture

2 participants