Formal: literal two-counter sampler reduction + per-line attribution under sampling - #1076
Merged
Conversation
…ine attribution under sampling Follow-up closing the two gaps flagged in the memory-sampler work. (1) §1b MemorySampler.lean — the one-counter model faithfully reduces the LITERAL two-counter C++. Previously the 'faithful to thresholdsampler.hpp' claim rested on collapsing _increments/_decrements into bal = incr - decr in prose. Now proved: St2 models the literal two-counter machine (separate ℕ counters, trigger incr ≥ decr+I / decr ≥ incr+I, reset both to 0); step_bisim / run_bisim prove it bisimilar to the one-counter model under abs(incr,decr)=incr-decr; threshold2_conserves transfers exact conservation to the two-counter machine as written. 'Faithful to the C++' is now a theorem. (2) §10 PerLineAttribution.lean — ties the byte sampler back to §6's per-line fraction story. A profiler reports recorded[ℓ]/Σrecorded, a ratio of unbiased estimators (not exactly unbiased since E[X/Y]≠E[X]/E[Y]). Proved what actually holds: fraction_of_expectations (the window cancels ⇒ no systematic scale bias in the breakdown), recorded_fraction_exact (proportional/large-sample limit ⇒ reported fraction = true fraction exactly, rate-independent), and that the per-line memory breakdown is a probability distribution (sums to 1), like §6. Full formal/lean build clean (8568 jobs); no sorry; standard axioms only. README updated (§1b note, new §10, boundary bullet).
… writeup Adds LeakTrackerAudit.lean: the leak formula 1-(frees+1)/(allocs-frees+2) (scalene_leak_analysis.py:31) divides with NO guard, relying entirely on the implicit invariant frees<=allocs — and allocs/frees are incremented at separate code sites (scalene_memory_profiler.py:236,401), so it's not obvious. We model the raw two-counter increment discipline (single-shot armed trigger) and PROVE frees<=allocs (run_frees_le_allocs), hence allocs-frees+2>=2>0 (denom_pos_reachable). The MetricCorrectness leak model had *assumed* this (unfreed,frees:ℕ with allocs=unfreed+frees), so it could never have caught a violation; this discharges the assumption against the actual dynamics. README gains a 'Bugs the formalization found' section documenting the two real defects the audit surfaced (both fixed in the companion code PR): the leak-velocity ZeroDivisionError and the atol sampling-window=0 case. Full formal/lean build clean (8569 jobs); no sorry; standard axioms only.
LeakTrackerAudit proved frees <= allocs only for a sequential event stream. In the code the two increment sites run on a background sig-queue thread while the shutdown drain runs on the main thread, and the tracker state is duplicated across fork -- the biggest remaining 'assumed not proven' gap (HANDOFF sec 6/7). Add LeakTrackerConcurrency.lean, which models the real discipline and, per the audit method, proves it is *necessary* rather than just present: - interleave_preserves_inv / sigqueue_then_drain_safe: with each process_malloc_free_samples call atomic (the sigqueue RLock), every interleaving of the sig-queue thread's steps with the main-thread drain preserves frees <= allocs -- scheduler order is irrelevant. - torn_free_breaks_inv: the lost-disarm race that dropping the lock would permit double-credits one armed trigger (frees = allocs + 1), so the RLock is load-bearing. - fork_reset_inv / partial_fork_reset_breaks_inv: the full fork reset (clear() zeros leak_score AND last_malloc_triggered together) starts the child safe; a partial reset that left the trigger armed breaks the invariant -- so resetting both fields together is required. No sorry; standard axioms only. Full lake build green. Updates README (new sec 11) and HANDOFF (gap closed).
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
1 participant
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 the two modeling gaps flagged when I explained the threshold-sampler proof.
(1) The one-counter model faithfully reduces the literal two-counter C++ (§1b)
The threshold-sampler conservation proof modeled the C++'s two
uint64_tcounters (_increments,_decrements) as their differencebal = incr − decr. That collapse was argued in prose — the honest caveat I'd flagged. Now it's a theorem:St2/stepThreshold2model the literal two-counter machine (separate ℕ counters, triggerincr ≥ decr + I, reset both to 0), matchingthresholdsampler.hpp:38-73.step_bisim/run_bisim— the two-counter machine is bisimilar to the one-counter model underabs (incr, decr) = incr − decr.threshold2_conserves— exact conservation transferred to the literal machine.So "faithful to the C++" no longer rests on a modeling assumption.
(2) Per-line attribution under sampling (§10 )
§9 proves the sampler unbiased for total bytes per line; this connects it to §6's per-line fraction. A profiler reports
recorded[ℓ] / Σ recorded— a ratio of unbiased estimators, which is not exactly unbiased (E[X/Y] ≠ E[X]/E[Y]). I prove what actually holds and is what users rely on:fraction_of_expectations— the sampling window cancels ⇒ no systematic scale bias in the breakdown.recorded_fraction_exact— in the proportional (deterministic-threshold / large-sample-Poisson) limit, reported fraction = true fraction exactly, independent of sampling rate.trueFraction_sum_one— the per-line memory breakdown is a probability distribution over lines, like the CPU one.Full
formal/leanbuild clean (8568 jobs); nosorry; standard axioms only.