Skip to content

Hold a rewrite recording per flow instead of per thread - #863

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
fix/rewriterecording-asynclocal
Aug 10, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
fix/rewriterecording-asynclocal

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Closes #859.

RewriteRecording held its ambient scope in a [ThreadStatic] field, and documented the consequence rather than fixing it:

A synchronous scope, and it has to be. Do not await inside one.

It no longer has to be. The scope is an AsyncLocal, as MathS.Settings now is (#857) and as the cancellation token in MathS.Multithreading already was.

Why this is more than a field swap

The trap #857 ran into applies directly here. An AsyncLocal flows the reference, so once the pointer reaches child tasks, two of them can report to one recording at the same time — and the steps were accumulating into a List<RewriteStep>. That is a torn write, not a merged list.

So alongside the field:

  • the store is a ConcurrentQueue<RewriteStep>;
  • closed is volatile, since it is now read from flows other than the one that set it;
  • Steps copies out rather than handing back a live view.

Behaviour

was is
a recording across an await lost, and the thread could collect a stranger's rewrites kept
work started under a recording, on another thread not collected collected
two flows each with their own recording separate separate
a recording opened inside a task, seen after it ends no no

One existing test is rewritten, not deleted

ARecordingOnOneThreadDoesNotSeeAnother started a thread inside an open recording and asserted its work was not collected. ExecutionContext flows to a manually started thread, so that work is now collected — which is the point of the change rather than a regression of it.

It becomes WorkStartedUnderARecordingIsCollectedWhereverItRuns, and the isolation it was really reaching for — that a parallel caller records its own work and nobody else's — is covered properly by SiblingRecordingsDoNotSeeEachOther, with a barrier forcing both recordings open before either does any work.

Also new: ARecordingSurvivesAnAwait (the regression) and ARecordingOpenedInsideATaskDoesNotEscapeIt.

AClosedRecordingIgnoresWhateverItIsStillHanded passes unchanged.

Off is still free

RewriteAllocationTest passes untouched: no recording open still costs one ambient read per rule set and allocates nothing, which is what #746 asks of every layer above the tree.

Verification

  • 6064 C# tests pass, 0 failed
  • 130 F# wrapper tests pass

Breaking, so it wants the 2.0 window; recorded in BREAKING-CHANGES.md with the migration, the Steps-is-now-a-snapshot note, and the fact that step order across parallel work is not defined.

Note on merge order: this touches BREAKING-CHANGES.md at the same anchors as #853 and #857. Whichever merges later needs a trivial "keep both" resolution in that file.

🤖 Generated with Claude Code

@Rafael-SOWNet
Rafael-SOWNet force-pushed the fix/rewriterecording-asynclocal branch from c402607 to 48160f2 Compare August 10, 2026 02:22
Closes #859.

RewriteRecording kept its ambient scope in a [ThreadStatic] field and documented the
consequence rather than fixing it -- "A synchronous scope, and it has to be. Do not
await inside one." It no longer has to be. The scope is an AsyncLocal, as MathS.Settings
now is and as the cancellation token in MathS.Multithreading already was.

The trap #857 flagged applies here and is why this is more than a field swap. An
AsyncLocal flows the reference, so once the pointer reaches child tasks two of them can
report to one recording at once, and the steps were accumulating into a List. That is a
torn write, not a merged list. The store is a ConcurrentQueue, `closed` is volatile
since it is now read from flows other than the one that set it, and Steps copies out
rather than handing back a live view.

One existing test encoded the old semantics and is rewritten rather than deleted:
ARecordingOnOneThreadDoesNotSeeAnother started a thread inside an open recording and
asserted its work was not collected. ExecutionContext flows to a manually started thread,
so that work is now collected -- which is the point of the change, not a regression of
it. It becomes WorkStartedUnderARecordingIsCollectedWhereverItRuns, and the isolation it
was really reaching for is covered by SiblingRecordingsDoNotSeeEachOther.

RewriteAllocationTest still passes untouched, so being off is still free: one ambient
read per rule set, nothing allocated, which is what #746 asks of every layer above the
tree.

Verified: 6064 C# tests and 130 F# tests pass.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@Rafael-SOWNet
Rafael-SOWNet force-pushed the fix/rewriterecording-asynclocal branch from 48160f2 to 5a5ef43 Compare August 10, 2026 02:48
@Rafael-SOWNet
Rafael-SOWNet merged commit bb75230 into master Aug 10, 2026
25 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the fix/rewriterecording-asynclocal branch August 10, 2026 16:37
Rafael-SOWNet added a commit that referenced this pull request Aug 23, 2026
…1012)

* Make the derivation a path from the input to the answer (#28, #273)

A recording held every rewrite that fired, across every candidate the simplifier generated
including the ones that lost, each on the subexpression it matched. Read in order that does not
walk from the input to the answer, and the type's own documentation said so in three places.

`RewriteRecording.PathFrom(input, result)` walks it. Every step is a whole expression turning
into another: `Steps[i].After` is `Steps[i + 1].Before`, the first starts at the input, and the
last lands on what `Simplify` returned. `DerivationPath.OfSimplifying(expression)` is the same
in one call, and prints as the stages with the identity that produced each one beside it.

Two grains in two types, because a rewrite pass walks bottom-up and no partly-rewritten whole
expression exists inside one: `DerivationStep` is the pass, and its `Rewrites` are the
`RewriteStep`s that fired in it, each naming the rule that did it.

What was missing was attribution. A rule-set pass now records what it turned into as well as
what it matched, and `Simplificator` records the stages that are not rewrite passes -- inner
simplification, the boolean minimiser, the polynomial rearrangement, expansion, factoring --
since the chain otherwise has a hole wherever the simplifier tidies up. Losing candidates are
absent rather than marked: nothing leads from one to the answer, so none can be on a path to
it, and what the search produced and did not keep is reported as `ExpressionsExplored`.

Free when nobody is recording, which is what #746 requires of anything above the tree: one
ambient read per stage against a tree walk per stage, and no allocation. `RewriteAllocationTest`
guards the new fast path the way it already guarded `ApplyOnce`.

`Simplify` returns what it returned before, and the raw recording is unchanged -- 270 rewrites
on `x^(-1)/(y/z)`, 251 of them normalisation, measured on both builds.

Corrected in passing, each re-measured: `Common` has 100 arms and not 103; `Derivation` on that
expression is 5 rewrites and not 6; and `Transformations.md` said a source generator over the
switch bodies was still for #746 item 50 to decide, which #951 shipped.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011emtnRT6EWTrxXNtqDVK3e

* Say per flow and ambient read, which is what the recording has been since #863

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011emtnRT6EWTrxXNtqDVK3e

---------

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.

RewriteRecording's ambient scope is per-thread, so it does not survive an await

1 participant