Skip to content

Fix #504: lazy hash and inferred assumptions are race-free on shared nodes - #511

Open
petlenz wants to merge 2 commits into
fix-490-491-assumption-consistencyfrom
fix-504-shared-node-races
Open

petlenz wants to merge 2 commits into
fix-490-491-assumption-consistencyfrom
fix-504-shared-node-races

Conversation

@petlenz

@petlenz petlenz commented Sep 19, 2026

Copy link
Copy Markdown
Member

Closes #504. Stacks on #508 (fix-490-491-assumption-consistency) and builds on its epoch stamp rather than replacing it.

Two const-looking read paths mutated shared node state, so a shared expression could not be read from two threads.

Mechanisms, and the measurements that chose them

Lazy hash — compute-once publication. hash_value() runs a three-state machine (unset → computing → ready): the winner of a CAS computes, everyone else waits for ready rather than reading a half-written value. A throw during computation resets to unset so a waiter takes over instead of spinning forever. Alternatives measured on a 400-node chain, Release, mean of two runs:

construct (µs) first hash (µs) warm read (ns)
base 31.9 4.4 1.95
this PR 26.0 10.1 1.93

The cold path costs one CAS per node (≈14 ns), so first-hash roughly doubles; the warm path is unchanged (one acquire load) and construction got faster, because the assumption change below drops a std::set per node. Net build-then-hash is a wash: 36.3 µs → 36.1 µs. Eager hashing at construction was rejected — it pays the cost for every node whether or not it is ever hashed, and #415 wants laziness kept.

Derived assumptions — bitmask in two atomic words. Every numeric_assumption alternative is an empty tag, so a fact set is a bitmask. facts_ holds asserted/intrinsic facts, derived_ holds (epoch << 16) | mask published in one store. A reader sees the previous snapshot or the new one, never a partially rebuilt container. This deletes the std::_Rb_tree corruption outright rather than guarding it; a per-node mutex was the alternative and costs more memory per node than the whole manager now uses. #508's epoch semantics are preserved exactly: asserted facts bump the epoch and clear the derived word, replace_derived wipes prior derived facts the way set_ = facts.set_ did, and set_inferred() still pins intrinsic facts so they never go stale.

invalidate_hash() now clears the publication state too — otherwise a mutated n-ary node kept a ready flag over a zeroed hash. That is what three existing tests (MutatedCopyDropsStaleCachedHash, SubCancelInvalidatesAndCollapses, PythagoreanBranchHygiene) caught when the first draft missed it.

Thread-safety contract this implies

  • Safe: concurrent reads of a shared expression — hashing, printing, evaluating with per-thread evaluators, querying assumptions — including the first such read, which is where the lazy caches are filled.
  • Safe: concurrent construction of new expressions sharing leaves.
  • Unsafe, by design: mutating a node while another thread reads it — assume() / .assumption() / clear() on a symbol, or the construction-time invalidate_hash() / insert_hash() paths. Same rule as a standard container: concurrent readers are fine, a concurrent writer is not. The epoch is atomic, so an assertion racing a reader yields the old or new fact set, but the surrounding set-up is still a user-side race.
  • Canonical form depends on annotation time: folds run at construction, assumptions are written afterwards #482 unchanged: folds already taken at construction are not revisited.

Verification

TSan, gcc-14, ASLR disabled via setarch -R (TSan otherwise aborts with "unexpected memory mapping" on this kernel — an environment issue, not the code; test discovery also had to move to PRE_TEST so the build-time run does not trip it).

  • Negative control, same tests against unfixed sources: 7 data races — 2 in expression::hash_value(), 5 in the assumption path including std::_Rb_tree insert/rebalance and numeric_assumption_manager::{inferred,stale}.
  • With the fix: 0, and the full suite under TSan is 1608/1608 with 0 warnings.
  • Debug suite 2419/2419; clang-format and clang-tidy (--warnings-as-errors='*') clean.

ThreadSafetyTest.h adds five tests. The two hash tests and the assumption test reproduce the races; the assumption one deliberately builds its reference from a separate tree so the shared one reaches the threads with its facts still underived — an earlier draft computed the reference first, which pre-filled the cache and silently stopped reproducing the race. The tensor-query and per-thread-evaluator tests are lock-ins: they pass on the unfixed base too, since tensor annotations are computed at construction.

Assertions compare against a single-threaded reference rather than pinning a particular inference result, so the test does not depend on how strong the assumption rules happen to be.

Two const read paths wrote node state without synchronisation, so a shared
expression could not be read from two threads. hash_value() now publishes
through a small state machine: one thread computes, others wait for the
value rather than reading it half-written. Derived assumptions move from a
std::set into two atomic words - every fact is an empty tag, so a whole set
is a bitmask - which removes the tree a concurrent reader could corrupt and
keeps the epoch stamp that decides staleness.

Asserted facts stay authoritative and still bump the epoch; a snapshot is
published in one store, so a reader sees the previous set or the new one.

Signed-off-by: petlenz <[email protected]>
The rebase onto #508 met its review fixes: derived facts stamped with an
epoch, stale ones discarded on read, scratch copies that do not claim a
node, and the tensor manager bumping the epoch so det's positivity follows
its operand. effective() reads the mask through the same staleness gate.

Signed-off-by: petlenz <[email protected]>
@petlenz
petlenz force-pushed the fix-504-shared-node-races branch from b5d1b8a to 9ed96c2 Compare September 20, 2026 20:12
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.

1 participant