Effects: heap operation mailbox and typed handler arms (fixes #182, #185); truthful file IO errors - #210
Merged
Merged
Conversation
Spec 0004 [TYPE-ANY] had grown 45 lines of implementation-defect prose: an ARC use-after-free, the narrative of a repair that was tried and reverted, and a SIGSEGV reproduction. A spec states what the language is; open defects belong in a plan. The section is restored to what it says on main. The analysis moves to docs/plans/0027-any-erasure-and-recovery.md, which also carries the two findings the spec never had: recovery is positional (a `let` annotation does not drive the coercion a declared return type does, so the heap address prints as a decimal integer on every backend), and un-erasure is unchecked (SIGSEGV, rc 139). All three reproduce identically on a clean origin/main worktree in both flavors, so they are filed as #208 and #209 rather than fixed here. Comment pointers in lower.rs, effects.rs, lib.rs and both `any` corpus twins now name the plan instead of the spec section. Goldens unchanged on all three backends; zero live ARC objects.
Moving read_file/write_file into file_runtime.c took ~50 well-covered lines out of system_runtime.c's denominator, so the remainder fell from 70.24% to 67.35% on Linux and the C ratchet failed at its 68% floor. The threshold is correct; the coverage was missing. Three paths that nothing exercised now have tests: - A child killed by a SIGNAL must report -1. WEXITSTATUS of a signalled status is the signal number, so an unchecked read makes SIGKILL indistinguishable from `exit 9`. The command signals the tracked process itself (`kill -9 $$`): the runtime execs `/bin/sh -c`, so a nested `sh -c` would only work where the outer shell exec's the inner one -- bash does, dash does not, and on Linux the tracked shell exits NORMALLY with 137. - pipe() and popen() denied a descriptor, via an RLIMIT_NOFILE capped at the lowest free fd. No argument can provoke these branches, and they are the ones that run when a long-lived program exhausts its table. - The MAX_PROCESSES ceiling. next_process_id only increments -- cleanup frees the slot but never returns the id -- so a program that has spawned MAX_PROCESSES times can never spawn again with every slot free. Reached without a fork, since the descriptor cap fails each attempt at the pipe. Measured on both platforms the gate runs on: macOS 74.86% -> 79.89%, Linux 73.91% -> 79.50% (gcc 13, same 9 lines). Threshold left at 68 until CI reports its own Linux number, then ratcheted against a measurement rather than a prediction. The file tests move to test_file_runtime.c with the source they cover: test_system_runtime.c was 503 lines, over the size budget, and one suite per translation unit is what the split already implied.
Both platforms the gate runs on are now measured, so the RATCHET rule in this file applies: bump to max(floor, weakest measured - 1) in the same PR, so the gain cannot regress silently. system_runtime macOS 80.85 Linux 72.79 -> 68 becomes 71 file_runtime macOS 81.63 Linux 80.52 -> 78 becomes 79 file_runtime's entry was added earlier in this PR from a macOS number alone, before the split had ever been measured on Linux; 79 is what the weakest platform actually supports. The platform-gap example in _doc is refreshed with the same pair it already used (system_runtime), which had gone stale by ~2.5 points; the every-library to-do list is re-sorted, since fiber at 71 is now the weaker of the two.
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.
Effects: operands travel in a heap mailbox — fixes #182, #185
[EFFECTS-OPERATION-MAILBOX]A resumable operation's arguments now cross into the handler in a mailbox allocated per suspension — a word array sized by the operation — instead of a fixed register window.tests/effects/resume/resume_error_policies.test.{osp,ospml}now performs a 17-argument operation and asserts every position, including the 17th. That was a documented skip; it is an assertion.OSPREY_ARC_DEBUG=1armed and zero live objects.The remaining honest limit is written down rather than papered over: abandoning a region drops the performing frame's own reference along with the stack, so
[EFFECTS-OPERATION-MAILBOX]in spec 0017 quotes the exact program that reports one live object at exit. That is the abort-path frame leak, still open.Effects: a handler arm's value is type-checked —
[EFFECTS-HANDLER-ARMS]An arm's value is checked against whichever of the two answer types it actually produces, so an arm that abandons its region must be able to be the answer, and an arm that resumes must satisfy the operation's result type. Four new must-reject fixtures (
effect_arm_answer_type_mismatchand its ML twin, with.expectedoutput), plus checker tests incrates/osprey-types/src/expr.rs.Files: an
Errorcarries the OS's own reason —[BUILTIN-FILE-ERRMSG]A failed file operation returned a message that discarded why it failed, which makes a missing directory, a permissions denial and a full disk indistinguishable at the point they are handled. Errors now read
writeFile: out/report.txt: No such file or directory. Newcompiler/runtime/file_runtime.candio_error.h; the reason travels on a thread-local channel the caller clears before the call and takes after it.Runtime split
__osprey_coro_*moves out ofeffects_runtime.cintocompiler/runtime/effects_coro.c, with a neweffects_runtime.hheader. All plan and doc references repointed.Build gates
The C coverage inventory check no longer decides what ships by pattern-matching a filename —
C_SHIPPED_UNITSis derived from the archive object lists themselves, so a production unit namedtest_*can no longer slip past the ratchet.C_COV_EXEMPTshrank toterm_runtime test_runtimeaccordingly..gitignorenow covers the files regression programs write into the CWD. Two of them (osprey_http_state_levels.db,test_stale_reason.txt) had been committed in the same change that added the tests writing them; they are untracked here.Reverted on this branch
An
anyownership rule that transferred a reference when erasing and took it over when recovering was written earlier on this branch and is reverted. It balanced only when the word came from apointer -> anyerasure, andLType::I64is equally everyintand every borrowedanyparameter — sofn identity(x: any) -> any = xgained an owner it never received and returned a dangling pointer, andfn intish() -> any = 7would have registered7as a pointer and freed it. It was memory-unsafe, not merely unbalanced.What replaces it is coverage of the case that had none: borrowed-
anyforwarding inany_type_comprehensive.test.{osp,ospml}under every backend with the leak oracle armed, plus an IR-level guard test that fails if an owner is ever entered at that cast again.Book (separable)
Book/adds a 48-file manuscript (~2.8k lines). It is independent of everything above and can be split into its own PR on request — it landed in the same commit as unrelated work, so separating it means history surgery rather than a cherry-pick.Not fixed here
anyreleases it in the producing frame — caller reads a dangling pointer, two calls underflow the live-object counter #208 — returning a heap value asanyreleases it in the producing frame under ARC; two recoveries underflow the ledger to-1.let x: string = <any-typed expr>drops the annotation and prints the pointer as a decimal integer — the same recovery through a function return works #209 — aletannotation does not drive the recovery coercion a declared return type does, so the heap address prints as a decimal integer on every backend.Both were verified against a clean
origin/mainworktree ata57673e2, in both flavors, and reproduce identically there — they are not regressions from this branch. Analysis, reproductions, the repair that must not be retried, and a phased checklist are indocs/plans/0027-any-erasure-and-recovery.md. Spec 0004[TYPE-ANY]is restored to what it says on main: a spec states what the language is, and open defects belong in a plan.#184 (four-argument curried ML functions can silently skip handled effects) remains the outstanding showstopper for plan 0016.
Verification
Every CI job was run locally against this tree:
make testTEST_CORPUS_ARC_LEAKY=0, all C and Rust coverage thresholds met, 267 extension tests,[vscode-extension] 97.25% >= 95%cargo test --workspace, corpus ×3,hawk: 0 finding(s), examples,make bank-test126/126, goldens126/126, 53 skips matchingWASM_UNPORTABLE.txtexactly-D warnings/ deslop / shipwrightwindows-core(ci-windows.yml) needswindows-latestand could not run here. The closest local equivalent — the same corpus in all three memory modes — passed, but the MinGW build and Windows-specific paths are unverified locally and rely on CI.The
wasmjob was found already red on this branch and is fixed here: addingfile_runtime.cto the wasm archive changed which unresolved symbol the linker names first for four programs, so four reason strings intests/WASM_UNPORTABLE.txtwere stale. The skip set itself is unchanged at 53.Correction: the C coverage ratchet was red, and the table above missed it
The row claiming all C thresholds were met was measured on macOS only, and the gate runs on Linux. CI failed at
[c] system_runtime FAIL: 67.35% < 68%.The cause is this PR's own file split: moving
read_file/write_fileintofile_runtime.ctook ~50 well-covered lines out ofsystem_runtime.c's denominator, dropping the remainder from 70.24% to 67.35%. The threshold was right; the coverage was missing. Fixed by testing three paths nothing exercised — a signal-killed child reporting-1,pipe()/popen()denied a descriptor under a cappedRLIMIT_NOFILE, and theMAX_PROCESSESid ceiling — and the file tests moved totest_file_runtime.calongside the source they cover (test_system_runtime.cwas 503 lines, over budget).Measured on both platforms this time, per the standing instruction in
coverage-thresholds.jsonthat a threshold must hold on every platform the gate runs on: macOS 74.86% → 79.89%, Linux 73.91% → 79.50% (gcc 13 container, the same 9 lines). The threshold stays at 68 in this commit and is ratcheted once CI reports its own Linux number, so the bump rests on a measurement rather than a prediction.The first Linux run also caught a portability bug in the new test itself:
sh -c 'kill -9 $$'only reports a signal death where the outer shell exec's the inner one. bash does, dash does not, so on Linux the tracked shell outlived its child and exited normally with 137. The command now signals the tracked process directly.🤖 Generated with Claude Code