Owen.Async: cancellation atomicity and abandoned-operation safety

[PhysShell]

Context

Rust's cancel safety terminology names a class of bugs where an async operation is interrupted after consuming or mutating external state but before durable progress is committed. The same semantic problem exists in .NET even though cancellation is cooperative rather than implemented by dropping a Future.

This is not merely CancellationToken propagation. A method can pass the token correctly everywhere and still leave a protocol, resource, or state machine inconsistent when cancellation is observed at the wrong boundary.

Canonical example

private readonly List<byte> _buffer = new();

public async Task<Message> ReadMessageBrokenAsync(
    Stream stream,
    CancellationToken cancellationToken)
{
    var local = new List<byte>();

    while (true)
    {
        byte value = await ReadOneByteAsync(stream, cancellationToken);
        local.Add(value);

        if (value == (byte)'\n')
        {
            _buffer.AddRange(local);
            return Parse(_buffer);
        }
    }
}

If several reads complete and a later read observes cancellation, bytes have already been consumed from stream while the partial message exists only in the local async frame. The next call resumes from the middle of the message.

A cancel-safe shape commits each consumed byte to state that survives the current invocation before the next cancellation point:

public async Task<Message> ReadMessageAsync(
    Stream stream,
    CancellationToken cancellationToken)
{
    while (true)
    {
        byte value = await ReadOneByteAsync(stream, cancellationToken);
        _buffer.Add(value);

        if (value == (byte)'\n')
        {
            Message message = Parse(_buffer);
            _buffer.Clear();
            return message;
        }
    }
}

The broader ownership question is:

Who owns partially completed work, and who is obliged to commit it, roll it back, persist a resume cursor, transfer it, or invalidate the surrounding resource?

.NET-specific distinction

Rust select! commonly cancels the losing branch by dropping its Future. In .NET:

• CancellationToken is only a cooperative request;
• abandoning an await does not necessarily stop the underlying Task;
• Task.WhenAny and timeout races leave losing tasks running unless code explicitly cancels, joins, or transfers ownership;
• cancellation may therefore mean either the operation stopped or merely the caller stopped waiting.

That distinction creates a particularly strong Owen target:

Task<Message> operation = ReadMessageAsync(stream, operationToken);
Task winner = await Task.WhenAny(operation, Task.Delay(timeout));

if (winner != operation)
{
    // `operation` may still be reading from `stream`.
    return;
}

If the caller retries, disposes the resource, resets shared state, or starts another operation over the same object, two logical owners now act on one resource.

Relationship to existing Owen work

This research slice complements rather than duplicates existing async/lifecycle work:

• P-021 / Own.Async: token flow, swallowed cancellation, fire-and-forget, and async lifecycle;
• Own.Concurrent: retrofit structured-concurrency contracts onto existing C# async code #282 / Own.Concurrent: a child Task as an owned obligation discharged by await, WhenAll, return, or supervisor transfer;
• P-026 stale async-write: an old continuation mutating state after the logical operation has changed.

Cancellation safety adds the missing question:

What partially changed state remains if cancellation exits at this exact point?

Suggested umbrella name:

Owen.Async: cancellation atomicity and abandoned-operation safety

Candidate diagnostics

1. Abandoned underlying task

Detect a Task that remains potentially live after:

• Task.WhenAny / timeout race;
• Task.WaitAsync(cancellationToken) or equivalent cancellable wait;
• an early return or cancellation path;

when the task is not subsequently:

• cancelled through a token it actually observes;
• awaited/joined;
• returned;
• transferred to an explicit supervisor/owner.

2. Resource reuse while a prior task may still run

After an abandoned wait, detect reuse of the same resource or state:

• a second operation starts on the same Stream, socket, reader, client, transaction, or mutable object;
• the resource is disposed;
• shared state is reset;
• a replacement generation/request is started while the old task can still write.

This is likely the highest-signal MVP because the ownership violation is explicit and consequences are concrete.

3. Cancellation observed after irreversible success

await transaction.CommitAsync(cancellationToken);
cancellationToken.ThrowIfCancellationRequested();
return result;

After a successful irreversible commit, reporting cancellation can cause callers to retry an operation that already happened.

Candidate rule: cancellation is observed after a known commit/effect boundary without an idempotency or result-recovery contract.

4. Cleanup/rollback uses an already-cancelled token

try
{
    await ApplyChangesAsync(cancellationToken);
}
catch (OperationCanceledException)
{
    await RollbackAsync(cancellationToken);
    throw;
}

The cleanup may immediately cancel and leave the state inconsistent. Critical cleanup generally needs a distinct bounded token or a non-cancellable region.

Candidate rule: a token proven cancelled on the handler path is passed to a cleanup, rollback, release, or compensation operation.

5. External progress consumed before commit across a cancellable boundary

Path shape:

consume or mutate external state
    -> store progress only in local async-frame state
    -> cancellable await / explicit cancellation throw
    -> cancellation exit
    -> no commit, rollback, resume-state persistence, or resource invalidation

Examples:

• bytes consumed from a stream;
• an item removed from a queue/channel;
• a sequence number advanced;
• a file partially written;
• a lease/resource acquired;
• a remote mutation made before local bookkeeping commits.

This is valuable but should follow the abandoned-task vertical because it needs effect summaries and stronger interprocedural reasoning.

Proposed OwnIR facts

The C# extractor should emit facts, not contain a second checker.

effect:
  consumes(source, value)
  mutates(resource)
  commits(operation)
  compensates(operation)
  invalidates(resource)

cancellation:
  cancellable_await
  explicit_throw_if_cancelled
  cancellation_handler
  wait_abandoned

task:
  created
  awaited
  cancellation_requested
  ownership_transferred
  possibly_running_on_exit

storage:
  local_async_frame
  receiver_field
  durable_state
  returned_to_caller

The core can then prove a path such as:

irreversible_effect
    -> cancellation_exit
    -> no commit
    -> no compensation
    -> no resource invalidation
    -> partial progress not externally owned

Required API/effect summaries

Avoid a useless rule like “local variable lives across await”. That would generate SARIF compost rather than findings.

Start with a small model vocabulary:

consumes
restartable
transactional
idempotent
cancel_closes_resource
cancel_preserves_progress
wait_only_cancellation
commit
rollback
cleanup

Initial summaries should live in Owen models/sidecar contracts rather than requiring users to annotate every method.

Runtime witness opportunity

A later runtime slice could inject cancellation at successive real cancellation points and verify:

• retry/resume remains valid;
• no orphan task remains live;
• the resource is not concurrently reused;
• commit/rollback invariants hold;
• late writes do not mutate a replacement generation.

This would pair naturally with OwnAudit runtime correlation and 007 replay evidence.

Suggested implementation order

1. Abandoned underlying task after WhenAny / timeout / cancellable wait.
2. Reuse or disposal of a resource while the prior task may still run.
3. Cancelled token reused for cleanup/rollback.
4. Cancellation observed after irreversible success.
5. Consume-before-commit across cancellable boundaries using effect summaries.
6. Runtime cancellation-point witness and static/runtime correlation.

Non-goals and suppressions

Not every non-restartable operation is a bug. Cancellation may intentionally invalidate and close the entire connection/session, making partial progress irrelevant.

Suppress or prove safe when:

• cancellation closes/invalidates the containing resource;
• the operation is explicitly non-restartable and cannot be retried;
• progress is stored durably or returned to another owner;
• the API guarantees transactional cancellation;
• the effect is idempotent and retry is explicitly modelled;
• application shutdown makes continuation/retry impossible.

Acceptance target for the first vertical

A useful first diagnostic should demonstrate all of the following:

• positive: WhenAny timeout leaves a task reading a resource and caller starts a second read;
• positive: caller disposes/reset state while the task is potentially live;
• negative: losing task is cancelled through an observed token and then joined;
• negative: task ownership is returned or transferred to a supervisor;
• negative: distinct resources are used;
• finding includes the ownership path from task creation through abandoned wait to conflicting resource use.

This keeps the first slice narrow, high-signal, and aligned with Owen's existing ownership-obligation architecture rather than attempting universal side-effect inference immediately.