[P0] Make pending approval execution handoff cancellation-linearizable #63

New issue

Closed

opened 2026-08-16 23:52:07 +00:00 by lost-rob0t · 1 comment

lost-rob0t commented

2026-08-16 23:52:07 +00:00

(Migrated from github.com)

Problem

PR #62 currently has a narrow but real scheduling race between host approval and owner cancellation.

Current shape in rlm_authority:

rlm_approve/2 moves a record from pending to approved under rlm_authority mutex.
It releases that mutex and calls rlm_async_submit/3 for the trusted continuation.
Only after submission does it reacquire the authority mutex and attach the returned execution Future / move the record to executing.

During the interval between (1) and (3), rlm_pending_cancel_owner/2 can observe an approved record whose control entry still has ExecutionFuture = none. The current cancel_owned/2 branch performs no cancellation in that state. A scheduler worker can therefore cross into the trusted continuation after the owner was cancelled.

This was discovered during the #53/#54 core-hardening audit. Do not paper over it with sleeps or a weaker cancellation test.

Required invariant

Cancellation and the authoritative execution claim must have an explicit linearization point:

approval granted
  -> execution prepared
  -> exactly one of:
       execution claim wins -> operation may execute
       cancellation wins    -> continuation can never mutate target

Human approval must still never occupy an rlm_async worker while waiting.

Acceptance

There is no state in which owner cancellation can win before the authoritative execution claim yet the continuation later runs.
Approval scheduling does not introduce nested Future waits.
The exact trusted continuation remains private host state.
Cancellation before execution claim resolves the pending-resolution Future deterministically and performs zero target mutation.
Cancellation after execution has already crossed the authoritative execution boundary has documented, deterministic semantics.
Duplicate approve/cancel races resolve exactly once.
Runtime/agent teardown uses the same cancellation path.
Add an adversarial concurrent test that actually overlaps approval scheduling and cancellation; do not rely on a serial test.
Add a scheduler-saturation test so the execution task can be held queued while cancellation wins, then prove releasing workers cannot execute the cancelled continuation.
Full canonical deterministic suite remains green.

Constraints

Preserve the canonical direction:

execute ABI
  -> async API -> Future
  -> sync API -> same async operation -> await

Do not add an authority UI/TUI and do not create a second confirmation subsystem.

## Problem PR #62 currently has a narrow but real scheduling race between host approval and owner cancellation. Current shape in `rlm_authority`: 1. `rlm_approve/2` moves a record from `pending` to `approved` under `rlm_authority` mutex. 2. It releases that mutex and calls `rlm_async_submit/3` for the trusted continuation. 3. Only after submission does it reacquire the authority mutex and attach the returned execution Future / move the record to `executing`. During the interval between (1) and (3), `rlm_pending_cancel_owner/2` can observe an `approved` record whose control entry still has `ExecutionFuture = none`. The current `cancel_owned/2` branch performs no cancellation in that state. A scheduler worker can therefore cross into the trusted continuation after the owner was cancelled. This was discovered during the #53/#54 core-hardening audit. Do not paper over it with sleeps or a weaker cancellation test. ## Required invariant Cancellation and the authoritative execution claim must have an explicit linearization point: ```text approval granted -> execution prepared -> exactly one of: execution claim wins -> operation may execute cancellation wins -> continuation can never mutate target ``` Human approval must still never occupy an `rlm_async` worker while waiting. ## Acceptance - [ ] There is no state in which owner cancellation can win before the authoritative execution claim yet the continuation later runs. - [ ] Approval scheduling does not introduce nested Future waits. - [ ] The exact trusted continuation remains private host state. - [ ] Cancellation before execution claim resolves the pending-resolution Future deterministically and performs zero target mutation. - [ ] Cancellation after execution has already crossed the authoritative execution boundary has documented, deterministic semantics. - [ ] Duplicate approve/cancel races resolve exactly once. - [ ] Runtime/agent teardown uses the same cancellation path. - [ ] Add an adversarial concurrent test that actually overlaps approval scheduling and cancellation; do not rely on a serial test. - [ ] Add a scheduler-saturation test so the execution task can be held queued while cancellation wins, then prove releasing workers cannot execute the cancelled continuation. - [ ] Full canonical deterministic suite remains green. ## Constraints Preserve the canonical direction: ```text execute ABI -> async API -> Future -> sync API -> same async operation -> await ``` Do not add an authority UI/TUI and do not create a second confirmation subsystem.

lost-rob0t commented

2026-08-17 05:52:16 +00:00

(Migrated from github.com)

Implemented on PR #62, exact final head 1dddd22e0d4bdd8c862cc06c6a3d609c26c96094.

The approval handoff now uses a private short-lived execution gate. The execution Future is attached to authority control state before the gate is armed; after arming, owner cancellation and execution race a single mutex-protected authoritative execution claim. Cancellation that wins before the claim terminalizes the operation and prevents the trusted continuation from crossing the side-effect boundary. Cancellation after the claim has documented best-effort interruption semantics without pretending to roll back already-performed host effects.

Adversarial coverage includes scheduler saturation with all 8 workers occupied, queued approved execution cancelled before claim with zero later mutation after worker release, and repeated concurrent approve/cancel races with exactly-once terminal resolution / at-most-once mutation. Runtime/agent teardown uses the same owner-cancellation path.

Exact-head validation is green: full deterministic CI, benchmark/conformance, deep-recursion experiment, CLI/trace, fresh-process graph restart, durable artifact handoff, whitespace, and the complete configured REAL OpenRouter suite all passed.

Implemented on PR #62, exact final head `1dddd22e0d4bdd8c862cc06c6a3d609c26c96094`. The approval handoff now uses a private short-lived execution gate. The execution Future is attached to authority control state before the gate is armed; after arming, owner cancellation and execution race a single mutex-protected authoritative execution claim. Cancellation that wins before the claim terminalizes the operation and prevents the trusted continuation from crossing the side-effect boundary. Cancellation after the claim has documented best-effort interruption semantics without pretending to roll back already-performed host effects. Adversarial coverage includes scheduler saturation with all 8 workers occupied, queued approved execution cancelled before claim with zero later mutation after worker release, and repeated concurrent approve/cancel races with exactly-once terminal resolution / at-most-once mutation. Runtime/agent teardown uses the same owner-cancellation path. Exact-head validation is green: full deterministic CI, benchmark/conformance, deep-recursion experiment, CLI/trace, fresh-process graph restart, durable artifact handoff, whitespace, and the complete configured REAL OpenRouter suite all passed.