Repository navigation
docs(occupancy): the page still described the pre-expiry drift; pin the reviewer's example (stacked on #117) - #118
Merged
Conversation
) Fork issue #105: the probe recorded what a stage reached (`peak_rss_kib`, `child_peak_rss_kib`) but nothing read an *occupancy* out of it, so a peak could only be compared against a cost. This grades the samples with the algebra the reading is stated in — `ResourceAlgebra.Instances.HWM`, whose reclamation laws `OccupancyTypes.Reclaim` proves — and checks the peak the algebra predicts against the one the samples measured. ## The grade, read from the samples Two sample windows are now recorded per task (`first_sample`, `last_sample`, set in `watch!`/`unwatch!`), and `finish!` attaches the grades read from them as the record's `grades` key: - `Grade(peak, drift)` with `drift ≤ peak`, `release = peak − drift`; - `seq` — the suffix starts from the previous grade's drift, `max (peak a) (drift a + peak b)` (Reclaim.reclaim-law); `alt` is the componentwise join, kept for the pair of laws; - `task_grades`, `stage_grade`, `predicted_peak_rss_kib`, `cost_bound_rss_kib`, `reclaimed_kib`, `disagreement`, `graded`. Tasks are read in sampled order (first sample, ties by record order); a task's drift is its peak when the next task started at or before its last sample, and the last task keeps its peak only if it was still resident. A record carrying no windows is left UNGRADED — `nothing`, skipped — never graded on an assumed order. (The 2026-10-14 record itself carries none: its windows come from `docs/occupancy/schedules.yml`, the file the gate and the unit test both read.) ## What it reads out of the recorded run `predicted_peak_rss_kib` reproduces the recorded stage peak in all three orders — 9204, 9192 and 18380 KiB — and the slack against the cost bound is what the cuts reclaimed: 9180, 9152 and 0 KiB. The prediction is an upper bound (at a handover the task still live holds at most its peak), so `disagreement` reports only what that bound forbids: a measured peak above the prediction. `scripts/check-occupancy-grades.jl` checks the equality, occupancy≤cost and non-negative reclamation against the record, and `test/unit/test_occupancy_grade.jl` (plus the two-thread test's per-order assertions) covers the laws, the two stage shapes and `finish!` itself. ## The same numbers, as theorems `docs/occupancy/GradedStages.agda` consumes the pinned siblings (occupancy-types `af95728`, resource-algebra `cf9235c`) and instantiates three of `Reclaim`'s laws at the measured grades: `no-reclaim` on the concurrent stage (drift = peak, so the peak is the sum), `reclaimed` on the serial one (drift < peak with a non-empty suffix, so strictly below cost), and `occupancy-at-cut` over the stage's timeline, plus `protocol-occupancy≤cost` at every cut. Nothing is re-declared; the Timeline names are Reclaim's own instance. `docs/occupancy/ reject/ConcurrentDriftIsZero.agda` is the negative control — grading the concurrent stage's drift as 0 is refused — checked by `scripts/check-occupancy.sh` beside TypedPeak. ## No ungraded readings `scripts/lint-occupancy-readings.sh` fails if production code outside `src/core/memory_probe.jl` names the `peak_rss_kib` key. It passes on this tree; from here a stage's occupancy figure has to come from the helpers. ## Verification No Julia or Agda in this environment, so the recorded arithmetic above was emulated exactly (three orders, plus each fixture in the unit test) and the Agda was written against the siblings' own checked sources, following the import and proof style of `OccupancyTypes.Witness`, which `occupancy-types/scripts/check-agda.sh` checks with the same flags. CI is the verifier: ci.yml's unit run, and the occupancy workflow's new graded reading and lint steps. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…ate CI failures The occupancy workflow's typed-peak job failed on the first push (it passes on main, so the failure is this change's). Its logs are served from blob storage, which this environment cannot reach, so two things: - `docs/occupancy/GradedStages.agda` now stands on its own names, the way `docs/occupancy/TypedPeak.agda` does: its own `module TH = OccupancyTypes.Timeline HWM` for every Timeline name, and the two protocol-level statements proved in that instance from the sibling's own halves — `Reclaim.cut-factor` over `reclaim-law`, and `occupancy≤cost` along `cut-factor` for `protocol-occupancy≤cost`, each proof the one `OccupancyTypes.Reclaim` gives for the same statement. The Grade-level laws (`no-reclaim`, `reclaimed`, `occupancy≤cost`) were already cited as they stand. Nothing re-declared, nothing borrowed across instances. - `scripts/check-occupancy.sh` now emits a `::error` annotation on every failure it diagnoses (each module, both rejection failure modes, the counted-bytes comparison), with the prover's own last lines escaped as the workflow-command syntax requires. Annotations, unlike job logs, can be read back through the API, so a failure that happens only in CI is visible from a machine that cannot download the log. Silent outside Actions, so local runs are unchanged. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
A draft placeholder survived into the checked proof, and Agda refuses it at the parse: `Could not parse the application gone 9180 TH.∷ TH.[_]` — read back from the run's annotations, which the script now emits (the job log itself is served from storage this environment cannot reach). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Resolved conflicts in: - docs/occupancy/GradedStages.agda (unmerged) Co-authored-by: CodeRabbit <noreply@coderabbit.ai> CodeRabbit-Task-Id: 984f5b46-e342-4efa-a2b8-35a9c14b5ee7
…ld sample boundary
…2e253f-metamanifold-webui
… example The three CodeRabbit findings on #117 are addressed by 05e56e7. What that fix left behind is the published description of the rule it replaced, and the reviewer's own example as a test. Verified before touching anything: the fixed fold reads the largest simultaneous peak sum. Emulated the branch head's `_grades_and_labels` against an independent reading of the windows (a task is live at instant t when t ∈ [first, last], or t ≥ first while last = 0): exhaustively over n ≤ 3 tasks with peaks 0–3 (219,660 cases) and over 300,000 random records up to six tasks, the fold equals that maximum whenever the record is one the probe can write, never falls below it otherwise (so `disagreement` still means "measured above anything the windows allow"), every task keeps drift ≤ peak, and the folded drift stays ≥ 0. - docs/occupancy-2026-10.adoc: the grading paragraph said "a task's drift is its peak when the next task still held it, and 0 when it had exited" — the rule the fix replaced. It now states the boundary rule: each handover keeps only the tasks still live at it; `drift_kib` is the change in that live sum (negative when the boundary also releases an earlier task); `release_kib` is everything freed between its start and the next boundary, and can exceed the task's own peak; the folded drift is the peaks still live at the stage's end. The signed per-task delta is named as the extension `Instances/HWM`'s header records as H-2 — the instance's own drift is the non-negative live sum. The `first_sample`/`last_sample` description is pinned to the probe's own wording (first sample after the first child started; last sample before the last was waited for; 0 for never). - test/unit/test_occupancy_grade.jl: the reviewer's exact example — windows [1,3], [2,10], [4,5] with peaks 100, 1, 100 KiB. Drifts [100, −99, −1], predicted 101 (not 201), cost 201, reclaimed 100: the 100 KiB that never coexist. And the sharpened bound is pinned too: 201 KiB resident at once is now the disagreement, where before the fix it was the prediction. - src/core/memory_probe.jl: the grading comment's two bullets and `release`'s docstring say the same, so the code's own description matches the page. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 3
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
|
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.
Stacked on #117 (base is that branch, so this diff is the delta only, not #117's work). #117 is the right fix; this is what its fix left behind. If you would rather have these three files folded into #117 itself, ask CodeRabbit to apply them there — this session can only push its own branch.
The audit of CodeRabbit's guidance on #117 (all three findings)
isempty(t.live) && (t.first_sample = …)re-stamped the window on every later child that foundliveemptyt.processes == 1 && (t.first_sample = p.samples + 1), set once per task_sample!both gotfirst_sample == 0, which_overlapsreads as never startedp.samples + 1(≥ 1), and_overlapsnow also requiresprev[1] != 0. The pid push and the boundary are set under the same lock acquisition that precedes the first sample that can see the child, sofirst_sampleis exactly the first sample that could count it — no off-by-one remains to chase201vs101example)Verification of #3 — the branch head's
_grades_and_labelsemulated against an independent reading of the windows (a task is live at instanttwhent ∈ [first, last], ort ≥ firstwhilelast = 0):[1,3] [2,10] [4,5], peaks100, 1, 100: drifts[100, −99, −1], predicted 101, cost 201, reclaimed 100 — the201is gone;disagreementstill means "measured above anything the windows allow";drift ≤ peak(noArgumentErrorpath), the folded drift stays ≥ 0, and the recorded run's figures are unchanged: 9204 / 9192 / 18380 KiB, reclaimed 9180 / 9152 / 0 — soscripts/check-occupancy-grades.jland the two-thread test's per-order assertions still hold.What is still wrong after that fix (this PR)
docs/occupancy-2026-10.adocdocumented the replaced rule: "a task's drift is its peak when the next task still held it, and 0 when it had exited". It now states the boundary rule — each handover keeps only the tasks still live at it;drift_kibis the change in that live sum, negative when the boundary also releases an earlier task;release_kibis everything freed between its start and the next boundary and can exceed the task's own peak; the folded drift is the peaks still live at the stage's end. The signed per-task delta is named as the extensionResourceAlgebra.Instances.HWM's header records as H-2; the instance's owndriftis the non-negative live sum. Thefirst_sample/last_samplebullet is pinned to the probe's own wording.[100, −99, −1], predicted 101, cost 201, reclaimed 100, and — the sharpened bound — 201 KiB resident at once is asserted to be the disagreement, where before the fix it was the prediction.src/core/memory_probe.jl's own grading comment said drift was "the net change …" andreleasewas "what the frontier reclaims"; both now say precisely what the arithmetic does.Comment-and-docstring changes only in
src/; no behaviour change. The occupancy workflow re-runs the recorded study on this branch anyway (the path filter matches).