feat: true cancellation for the fiber Io layer (PLAN-IO-UNIFY Phase 3)
A cancelled async worker now abandons its body at its next suspend instead
of running to completion.
- Cancel-flag back-ref (D4): SpawnOpts.cancel_flag (core.sx) + Fiber.cancel_flag
(sched.sx), set from opts.cancel_flag in Scheduler.spawn_raw; async passes
xx @f.canceled (the Future.canceled Atomic(bool) erased to *void).
- Delivery: Scheduler.suspend_raw consults fiber_canceled(self.current) PRE-park
(raise without parking — no deadlock if cancel landed before the worker ran)
and POST-resume (cancel landed while parked), raising error.Canceled.
cancel(f) flips the sticky flag, marks .canceled, and wakes the worker.
- async worker is failable Closure() -> ($R, !); the completion closure
f.value = worker() catch {…} marks .canceled/.failed and wakes the awaiter,
so post-suspend side effects never run. New failable io.sleep(ms) is the
cancellation point.
- Compiler: a -> ! fn whose only error source is try-ing a protocol method
(io.suspend_raw) was wrongly flagged 'declared ! but never errors';
collectErrorSites now marks a try of a non-identifier callee as a dynamic
(opaque) error source, suppressing the warning.
- Two UAFs found by adversarial review and fixed: (1) cancel-before-park
orphaned io.sleep's armed timer — suspend_raw's pre-park raise now evicts the
current fiber's timer/waiter first; (2) cancel(f) could wake a reaped worker —
now only wakes when was_pending.
Migrated 1805/1806/1824 to failable workers. Lock: example 1825 (seq: 1 -99,
post-suspend line never runs); byte-identical on aarch64-macOS + aarch64-linux.
.ir churn is the SpawnOpts layout change (type-table string renumbering).
This commit is contained in:
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -12,16 +12,18 @@
|
||||
#import "modules/std.sx";
|
||||
|
||||
main :: () {
|
||||
// Inputs captured at the call site.
|
||||
s := context.io.async(() -> i64 => 40 + 2);
|
||||
// Inputs captured at the call site. The worker is FAILABLE
|
||||
// (`Closure() -> ($R, !)`) — the unified Phase 3 shape; a body that never
|
||||
// raises is a degenerate failable that always succeeds.
|
||||
s := context.io.async(() -> (i64, !) => 40 + 2);
|
||||
print("sum: {}\n", s.await() or { -1 });
|
||||
|
||||
d := context.io.async(() -> i64 => 21 * 2);
|
||||
d := context.io.async(() -> (i64, !) => 21 * 2);
|
||||
print("double: {}\n", d.await() or { -1 });
|
||||
|
||||
// A worker that closes over a local.
|
||||
base := 42;
|
||||
n := context.io.async(() -> i64 => base);
|
||||
n := context.io.async(() -> (i64, !) => base);
|
||||
print("nullary: {}\n", n.await() or { -1 });
|
||||
|
||||
// The Io capability also carries a clock.
|
||||
|
||||
@@ -6,12 +6,13 @@
|
||||
#import "modules/std.sx";
|
||||
|
||||
main :: () {
|
||||
// Not canceled → await yields the value.
|
||||
ok := context.io.async(() -> i64 => 7);
|
||||
// Not canceled → await yields the value. The worker is FAILABLE
|
||||
// (`Closure() -> ($R, !)`) — the unified Phase 3 shape.
|
||||
ok := context.io.async(() -> (i64, !) => 7);
|
||||
print("ok: {}\n", ok.await() or { -1 });
|
||||
|
||||
// Canceled → await raises .Canceled → the `or` default is taken.
|
||||
c := context.io.async(() -> i64 => 7);
|
||||
c := context.io.async(() -> (i64, !) => 7);
|
||||
c.cancel();
|
||||
print("canceled: {}\n", c.await() or { -99 });
|
||||
}
|
||||
|
||||
@@ -25,8 +25,8 @@ main :: () -> i64 {
|
||||
push .{ io = xx s } {
|
||||
ps.spawn(() => {
|
||||
rec(pl, 1); // coordinator starts
|
||||
a := context.io.async(() -> i64 => { rec(pl, 10); 100 }); // worker A — deferred
|
||||
b := context.io.async(() -> i64 => { rec(pl, 20); 23 }); // worker B — deferred
|
||||
a := context.io.async(() -> (i64, !) => { rec(pl, 10); 100 }); // worker A — deferred
|
||||
b := context.io.async(() -> (i64, !) => { rec(pl, 20); 23 }); // worker B — deferred
|
||||
rec(pl, 2); // both spawned, neither has run
|
||||
va := a.await() or { -1 }; // park; A runs, wakes us
|
||||
vb := b.await() or { -1 };
|
||||
|
||||
@@ -0,0 +1,49 @@
|
||||
// Stream B2 — TRUE cancellation (PLAN-IO-UNIFY Phase 3). A `cancel` delivered to
|
||||
// a worker that is PARKED at a suspend point makes the worker ABANDON its body:
|
||||
// the worker's next `suspend_raw` raises `IoErr.Canceled`, which unwinds out
|
||||
// through `try context.io.sleep(..)` and the failable worker, so every line AFTER
|
||||
// the suspend never runs. This is "true cancellation, model (a)" — cancel rides
|
||||
// the `!` channel and stops in-flight work at the next suspend, not merely flags
|
||||
// a result.
|
||||
//
|
||||
// Flow (deterministic, virtual clock): the worker records 1 and parks in
|
||||
// `sleep`; the coordinator (a fiber, so it can `yield`) lets the worker reach its
|
||||
// park, then `cancel`s it. The worker's parked `suspend_raw` is woken and raises
|
||||
// `Canceled` → the post-sleep `rec(pl, 2)` and the `42` return NEVER execute. The
|
||||
// coordinator's `await` raises `Canceled` (sticky flag) → `or` default -99.
|
||||
// Sequence: `1 -99` — the absence of `2` is the proof that the post-suspend work
|
||||
// was truly cancelled.
|
||||
//
|
||||
// aarch64-pinned (the scheduler's per-arch asm): runs end-to-end on a matching
|
||||
// host (macOS + linux, byte-identical under the deterministic virtual clock).
|
||||
#import "modules/std.sx";
|
||||
sched :: #import "modules/std/sched.sx";
|
||||
|
||||
Log :: struct { seq: [8]i64; n: i64; }
|
||||
rec :: (l: *Log, v: i64) { l.seq[l.n] = v; l.n = l.n + 1; }
|
||||
|
||||
main :: () -> i64 {
|
||||
lg : Log = .{ n = 0 };
|
||||
s := sched.Scheduler.init();
|
||||
ps := @s; pl := @lg;
|
||||
push .{ io = xx s } {
|
||||
ps.spawn(() => {
|
||||
w := context.io.async(() -> (i64, !) => {
|
||||
rec(pl, 1); // worker started
|
||||
try context.io.sleep(10); // park; cancel delivers Canceled HERE
|
||||
rec(pl, 2); // POST-SUSPEND — must NEVER run
|
||||
42
|
||||
});
|
||||
ps.yield_now(); // let the worker run & park in sleep
|
||||
w.cancel(); // cancel while parked → wakes + raises
|
||||
r := w.await() or { -99 }; // await raises Canceled → -99
|
||||
rec(pl, r);
|
||||
});
|
||||
ps.run();
|
||||
}
|
||||
print("seq:");
|
||||
i := 0;
|
||||
while i < lg.n { print(" {}", lg.seq[i]); i = i + 1; }
|
||||
print("\n");
|
||||
return 0;
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1 @@
|
||||
{ "target": "macos" }
|
||||
@@ -0,0 +1 @@
|
||||
0
|
||||
@@ -0,0 +1 @@
|
||||
|
||||
@@ -0,0 +1 @@
|
||||
seq: 1 -99
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because one or more lines are too long
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user