Repository navigation
Docs/occupancy typed reading - #134
Closed
hyperpolymath wants to merge 3 commits into
Closed
hyperpolymath wants to merge 3 commits into
hyperpolymath wants to merge 3 commits into
Conversation
…wo-thread disagreement test The vsearch stage runs its ASV and OTU searches concurrently in the full pipeline and one after the other in a single-stage re-run. Nothing measured what either shape occupies. The searches run as child processes, so Sys.maxrss() of the Julia process never sees them. MemoryProbe (src/core/memory_probe.jl), off unless a pipeline.yml sets occupancy_probe.enabled: true, records per attested stage: - julia_allocated_bytes, the Base.gc_num() delta (cost); - per task, the largest sampled VmRSS of the children it started, and their kernel VmHWM; - child_peak_rss_kib, the largest sum of the stage's children's VmRSS at one sampling instant. It samples /proc every 10 ms (interval_ms) with preallocated buffers, so the sampling adds next to nothing to the allocation figure it reports. _run_killable registers each child. _attest stores the record under the stage's new optional `occupancy` key. Both vsearch call sites label their searches vsearch:asv and vsearch:otu. With the flag off, start() returns nothing and every hook passes straight through, so a stage record has exactly the keys it had before. The key is not added to the defaults because the run config is embedded in attestation.yml; it is documented there as a comment. The probe never throws into the stage it measures, and getpid is read once, while the child is alive. test/occupancy_disagreement_test.jl (run with the full suite) runs the two searches in three orders on a generated fixture: 1000 reference sequences, the smallest of a calibrated ladder that keeps both resident together for 15 or more samples. Assertions: - the cost agrees within 1% (measured: 0.04%), and the hits are byte-identical in every order; - the peaks are recorded in the log, not asserted. Locally: serial 9204 and 9192 KiB, concurrent 18380 KiB. The test runs vsearch with --threads 1. With several threads its output order varies, and _sort_hits_by_query!, whose key splits each line on every comparison, then moved the stage's allocation by up to 12% between repeats of the same order. This commit does not change that. The test file also covers: - the flag off and on, through the real _attest; - a failed stage, which keeps its occupancy and still rethrows; - old records, which still parse and merge; - a 64 MiB child against a sleep control; - chained commands and an instantly exiting child. Checks, run locally with Julia 1.12.5 -t 2 and vsearch 2.30.5: - the test file passes, 46/46; - test_provenance, test_tools, test_routes, test_jobs and test_config_hashing pass 547. One error is the live R probe, which needs the dada2 R package that CI installs and this machine lacks. - Five planted mutants are each caught: children ignored, flag ignored, key always written, stage peak computed as a sum, and extra work in one order (spread 0.249). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015pMjy981ie74uCttyYDanC
A dated record of what the occupancy probe found on 2026-10-14, and the typed reading checked against it, as MMW-01 asks. - docs/occupancy-2026-10.adoc: the table per order, with each search's peak, the measured stage peak, Session IR's counted bytes, the HWM typed peak and the Julia allocation. It also has a status ledger (MMW-01.1-4 TESTED, the general v0 to typed bridge still OPEN), the limits, and what the next proofs would change. - docs/occupancy/vsearch-*.sir: the stage as occupancy-types Session IR, one buffer per search, in each order. The stepper counts 9204, 9192 and 18380 KiB. - docs/occupancy/TypedPeak.agda: the typed peak computed by refl with occupancy-types' Timeline over resource-algebra's HWM grade. A search alone exits holding nothing; the concurrent first search is still resident. Results: 9204, 9192, 18380. docs/occupancy/reject holds two claims that must be refused: concurrent = serial, and serial = sum (occupancy read as cost). - scripts/fetch-siblings.sh pins occupancy-types af95728 and resource-algebra cf9235c into _build/dependencies. Their definitions are consumed, never copied. - scripts/check-occupancy.sh is the gate: Session IR check and run --trace, TypedPeak, the rejections at their own declarations, and counted bytes against typed peak per order. The occupancy workflow runs it whenever these files change, on any base branch, so this stacked PR is checked too. It uses the digest-pinned Debian trixie image with Agda 2.6.4.3, as upstream's proof job does, and setup-julia 1.12.5. - docs/occupancy/results-2026-10-14.yml: the raw probe records behind the table. - .gitignore: unignore exactly these docs (docs/* is otherwise kept local), and ignore _build/ and *.agdai. Checks run locally: - scripts/check-occupancy.sh exits 0 (Agda 2.6.4.3 wheel, Julia 1.12.5). - Its negative controls fail it: one SIR byte off (18381 != 18380), a true claim planted as a rejection, and a rejection failing for a scope error. - zizmor finds nothing in the workflow. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015pMjy981ie74uCttyYDanC
… test here Both runs ended in startup_failure. This account allows only GitHub's own actions and its own, SHA-pinned, and julia-actions/setup-julia is neither. The same policy has kept ci.yml (julia-actions, setup-bun, codecov) from starting on this fork since at least 2026-10-02, so the three-order test in its full suite never runs here. The workflow now uses no third-party action: - Julia 1.12.5 from julialang's tarball, checked against julialang's published SHA256, as the official Docker image records it; - vsearch from its tool_versions.yml pin, checked against the pinned SHA256, as ci.yml installs it. It has two jobs: - disagreement: Julia, R (RCall builds against it), the project environment, then test/occupancy_disagreement_test.jl with -t 2; - typed-peak: scripts/check-occupancy.sh, as before. The paths also cover the probe's sources and the test. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015pMjy981ie74uCttyYDanC
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 42 minutes. View limit details
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 |
|
Owner
Author
|
Resolved by inspection rather than rebase: this branch's three commits are the pre-squash originals of work already on main. Verified -- 4a6e26e (occupancy probe + two-thread disagreement test) merged as #106 ( The branch can be deleted; the record stays in its commits and in #106/#107/#108. |
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.
Summary
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers