observer: when is x counts assignments made inside unobserved: (#908) - #910
Merged
Merged
Conversation
) Two counters answered "how many times has x been assigned" and disagreed. `when is x` read env->assign_counts, bumped only under g_unobserved_depth == 0; `when is x at L` and the #868 occurrence ring read the history's own recorded-assignment counter (trace.c), which has no such gate. They diverged by exactly the number of assignments made inside `unobserved:` blocks — while the unobserved assignment's VALUE was recorded and readable the whole time. Only the count omitted it. #868 made that load-bearing: `<kw> is x when <n>` indexes the history's counter, because it is the only counter that can address a stored entry. So `when is x` — the natural way to discover how many assignments there are to ask about — was short by one per unobserved assignment, and every ordinal computed from it was off. Matching downward was worse: the write happens and its value is retained, so dropping it from the ordinal space would leave an addressable-looking hole. The count comes up to the history instead. `unobserved:` suppresses OBSERVATION (entropy/dH), which is all it ever documented; it never meant the assignment did not happen. Same principle as #871's raising predicate — a performance annotation must not change an answer. Sites: 9 gates in vm.c, 4 + 2 first-binding sites in eigenscript.c, and the emitted sequence in the JIT's inline SET_NAME fast path, which re-read EigsThread.unobserved_depth through the VM.owner back-pointer and skipped the bump. The JIT bump is now unconditional behind its NULL check, and emit_cmpl_0_disp32_rax goes with it (last user). Tests: test_unobserved.eigs gains the count/ordinal agreement, an in-block interrogation, and a fn-local case. test_jit_paths.eigs section 9 covers the emitter — a 20k-iteration unobserved loop, which the interpreter counts correctly for its first 5000 iterations before OSR takes over, so a stale gate in the emitter is invisible to any interpreted test. Validated by planting the old emitted sequence back: the check reports 5001 instead of 20001 while EIGS_JIT_OFF=1 still reports 20001. Release suite 3860/3860; ASan+UBSan detect_leaks=1 3852/3852, leak tally 0. Consumer preflight for the next pin bump: EigenGauntlet's observer_lab asserts the old behavior ("unobserved age unchanged") — filed as InauguralSystems/EigenGauntlet#26. Its CI is pinned to v0.38.0 and stays green until the bump.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #908.
The divergence
when is xandwhen is x at Lanswer the same question — "how many times hasxbeen assigned" — from two different counters:when is xreadsenv->assign_counts, bumped only underg_unobserved_depth == 0.when is x at Land the temporal:what is x at L/state_at of Lcollapse a loop body to its last execution, so no iteration but the final one is addressable #868 occurrence ring read the history's ownrecorded-assignment counter (
lc_bump,trace.c), which has no such gate.They disagreed by exactly the number of assignments made inside
unobserved:blocks — while the unobserved assignment's value was recorded and readable
the whole time (
what is x at Lanswers it). Only the count omitted it.Why up and not down
#868 made the divergence load-bearing:
<kw> is x when <n>indexes thehistory's counter, because that is the only counter that can address a stored
entry. So
when is x— the natural way to discover how many assignments thereare to ask about — was short by one per unobserved assignment, and every
ordinal computed from it was off.
Matching the history downward would have been worse than the inconsistency: the
write happens and its value is retained, so dropping it from the ordinal space
leaves an addressable-looking hole. The count comes up to the history instead —
the direction recorded on #908 when #909 landed.
unobserved:suppresses observation (entropy/dH), which is all it everdocumented; it never meant the assignment did not happen. Same principle as
#871's raising predicate: a performance annotation must not change an answer.
Sites
Nine gates in
vm.c, four plus two first-binding sites ineigenscript.c, andthe emitted sequence in the JIT's inline
SET_NAMEfast path — which re-readEigsThread.unobserved_depththrough theVM.ownerback-pointer and skippedthe bump, mirroring the interpreter. The JIT bump is now unconditional behind
its NULL check;
emit_cmpl_0_disp32_raxgoes with it (last user).Tests
test_unobserved.eigsgains the count/ordinal agreement, an in-blockinterrogation, and a fn-local case (whose interrogation forces the slow env
path).
test_jit_paths.eigssection 9 covers the emitter with a 20k-iterationunobserved loop: the interpreter counts it correctly for the first 5000
iterations and only the OSR thunk can get it wrong, so a stale gate in the
emitter is invisible to any interpreted test.
Planted-fault validation of that check — restoring the old emitted sequence
in
jit.calone:so the new check fails on exactly the fault it exists for.
Gates
detect_leaks=13852/3852, leak tally 0 (floor)TRACE.md's recorded divergence note replaced with the agreement requirement.
Consumer preflight
EigenGauntlet/src/observer_lab.eigsasserts the old behavior(
"unobserved age unchanged") — filed as InauguralSystems/EigenGauntlet#26.Its CI is pinned to
v0.38.0and stays green until the pin bump past thischange; the issue carries the replacement assertion. No other consumer combines
unobserved:withwhen is. The AOT calls the same runtime env write paths andneeds no change.
Closes #908.