RFC-0038 — Deferred dispatch: `@@[cast]` interface methods, addressing, and a bring-your-own executor

Status: Draft. The design is captured; the post/drain pattern this generalizes has been validated by a hand-rolled native implementation in a no_std kernel (an in-core scheduler driven as an actor — workers post retire messages, a single drain loop dispatches them), but the framec language primitive (@@[cast] + the drain hook) is unimplemented.
Author: Mark Truluck
Created: 2026-05-22
Builds on: RFC-0020 (runtime reference architecture), RFC-0025 (typed event payload)
Companion to: RFC-0036 (no-allocation dispatch — a deferred mailbox wants pooled event storage), RFC-0026 (the calculus — deferred dispatch must preserve the run-to-completion step)

Summary

Today every Frame interface call is a synchronous dispatch: calling system.event(args) runs the matching handler — including its transition and the exit/enter handlers that follow — to completion before the call returns, and the call may return a value. This RFC adds a second dispatch mode: a deferred (asynchronous) interface method, marked @@[cast], whose call does not run the handler. It enqueues the event onto the target instance’s mailbox and returns immediately. A later drain — driven by a host-supplied executor — dequeues the event and dispatches it under normal run-to-completion rules.

A @@[cast] method MUST have no return value, because at the call site the handler has not run and there is nothing to return. A result, where one is needed, comes back as a separate deferred event (a reply), correlated through the recipient’s state. The model is the actor-system distinction between a synchronous call (returns a reply) and an asynchronous cast (fire-and-forget) — the same split Erlang’s gen_statem draws, which Frame’s Erlang backend already compiles onto.

Motivation

Frame’s runtime is specified as synchronous run-to-completion (RTC): an event is fully processed — handler body, then the staged transition’s exit and enter handlers — before the next event is dispatched. RTC is what makes a Frame system analyzable: at every quiescent point the machine is in exactly one well-defined state. This RFC does not change that. It adds a way to schedule an event for a future RTC step instead of running it now.

Three problems make synchronous-only dispatch insufficient.

1. You cannot dispatch from a context that must not run a handler now

Some callers are structurally forbidden from running a handler synchronously:

An interrupt / signal context that has preempted the owner mid-dispatch. Re-entering the same instance corrupts it (RTC assumes one dispatch at a time); and if dispatch allocates (see RFC-0036), allocating in that context can deadlock against a held allocator lock.
A different thread or core that does not own the instance. Frame’s generated code is single-owner (non-shareable across threads by construction); the only safe cross-context interaction is to hand the owner data, not to call into its instance.

The only correct action in these contexts is to enqueue an event for the owner to process later. Frame has no construct for this, so every such site is written by hand in the host language: a queue, a producer that pushes a tagged record, and a consumer loop that pattern-matches the record back into an interface call. The Frame system at the center is unaware that its events arrive through a queue.

2. Deferring work past the current handler is hand-rolled

A handler sometimes needs to cause an effect that must happen after the current RTC step settles — e.g. block, terminate, or hand off — because doing it inside the handler would observe or corrupt a machine that is still mid-transition. Today this is expressed with an out-of-band flag the handler sets and the caller checks after dispatch returns (“pending” flags). That is a manual re-encoding of “send myself this event, but later.” A self-directed deferred send expresses it directly and keeps the intent in the state graph.

3. Request/response has no idiom, so it is reinvented per call

When a caller needs a result from a system whose work completes asynchronously (a device command, an I/O request), the synchronous return value is the wrong shape — the result is not available when the call returns. Implementers reinvent the correlation by hand: issue the request, record “who asked / what is in flight,” and when the completion arrives, look up the originator and resume it. This is exactly the actor-model request/reply pattern, and the recipient’s state is the natural correlation token — but Frame gives no language support for the reply leg, so it lives entirely in host code.

What a fix needs to achieve: a first-class way to (a) enqueue an event to an instance rather than call it, (b) express that a reply will arrive later as another event, and (c) leave the executor — the loop that drains mailboxes — under host control, because embedded and kernel hosts must own when dispatch runs (interrupt state, idle, scheduling).

The mechanism already half-exists

Frame’s transition machinery is already a bounded, deferred event sequence: a handler’s -> $S does not change state mid-body. The runtime stages it, lets the handler run to completion, then dispatches the old state’s <$ and the new state’s $> (the latter carrying its enter arguments as a synthesized event). So the runtime already defers and sequences events it generates itself. This RFC generalizes that existing capability from “the runtime’s own exit/enter events, same instance, depth-one” to “an explicitly enqueued event, possibly to another instance, drained by the executor.”

The contract

The key words MUST, MUST NOT, SHOULD, SHOULD NOT, and MAY are to be interpreted as in RFC 2119.

Cast methods

An interface method MAY be annotated @@[cast]. Such a method is a deferred (asynchronous) event:

A @@[cast] interface method MUST be declared with no return type. The compiler MUST reject a @@[cast] method that declares one.
A handler for a @@[cast] method MUST NOT return a value (@@:(expr) is rejected by the validator with a dedicated diagnostic). It MAY transition, run actions, and itself cast events.
Calling a @@[cast] method MUST NOT run the handler. It enqueues the event (message tag + arguments) onto the target instance’s mailbox and returns immediately.
A queued event’s arguments MUST be owned by the queued message (it outlives the call), and carried as a typed payload per RFC-0025.

A method without the annotation keeps today’s semantics exactly: synchronous dispatch, optional return value (a call).

The mailbox and the executor

Each system instance has a mailbox: a FIFO of pending events. The runtime provides the enqueue operation (the cast) and a drain operation that dequeues one event and dispatches it under normal RTC rules. The runtime MUST NOT own the drain loop. The host drives draining — “bring your own executor” — so a host that must control interrupt state, idling, and scheduling keeps that control. The runtime exposes, per instance (names illustrative):

cast — enqueue (the surface form is the annotated interface call);
drain_one() → bool — dispatch the next queued event if any; returns whether one ran;
pending() → count — queue depth, so a host loop can decide when to stop.

A drain dispatch is an ordinary RTC step: it runs the handler, then the staged transition’s exit/enter sequence, to completion, before the next drain_one.

Addressing and reply-to

Casting to another instance requires naming it. Frame’s synchronous calls operate on a reference the caller already holds; deferred sends need an address — an opaque handle to a target instance’s mailbox. A cast MAY carry a reply-to address, so the recipient can cast a result back.

Request/response is then two casts plus state as the correlation token: the requester casts a request (with its own address as reply-to), transitions to a waiting state, and the reply — arriving later as a cast into the requester — drives the next transition. There is no synchronous “return”; the continuation is the requester’s state.

The precise shape of addresses (process-style identity, typed handles, a registry) is the largest open question and MAY be split into a companion sub-RFC; this RFC fixes the semantics (a cast targets a mailbox; a reply is itself a cast) and leaves the handle representation open (see Unresolved questions).

Examples

A device driver lifecycle: issue a command (cast to hardware via a host action), wait, resume on completion. The completion arrives as a cast and the state is the correlation:

@@system DeviceBringup {
    interface:
        @@[cast] start()
        @@[cast] completed()
        @@[cast] failed()

    machine:
        $Idle {
            start() {
                issue_command()   // host action: enqueue a hardware command
                -> $InFlight
            }
        }
        $InFlight {
            completed() { -> $Ready }   // the reply leg; no inline return
            failed()    { -> $Error }
        }
        $Ready  { }
        $Error  { }

    actions:
        issue_command() { }
}

A self-directed deferred send replaces a hand-rolled “pending” flag — schedule the teardown for after this dispatch settles:

$Active {
    shutdown() {
        // Do not tear down mid-dispatch; cast to self, handled on the next drain.
        finalize()      // a @@[cast] interface event on this system
        -> $Draining
    }
}

A synchronous query is unchanged — reads are calls, never casts:

$Active {
    is_busy(): bool { @@:(true) }   // ordinary synchronous call; returns a value
}

Alternatives

Per-call-site choice instead of per-method. Let the caller pick sync vs deferred at each call (s.foo() vs s.post(foo, …)) on the same handler. Rejected as the default: it makes “may this handler return a value?” ambiguous (the same handler would be both a call and a cast), and it scatters the contract across call sites. Declaring cast-ness on the method makes it a checkable contract and matches the call/cast split. A per-call deferred form MAY still be offered as sugar later, but the method annotation is primary.
Return a future/handle from a cast. A cast could return a token the caller later resolves to the handler’s result (the futures model). Rejected as the primary shape: it reintroduces an inline “await” that the single-owner, run-to-completion model cannot honor without blocking, and the reply-as-event form already expresses the result using the machine’s own states as the continuation — more in keeping with Frame.
A Mutex-wrapped shared instance for cross-thread use. Lets multiple threads “call” one instance. Rejected: it serializes every dispatch (no parallelism), and a handler that dispatches into itself under the lock deadlocks. Single-owner + message passing is the model; a lock defeats it.
The runtime owns the executor loop. Simpler for application hosts, but a no_std / interrupt-driven host must own when dispatch runs. Bring-your-own executor keeps the runtime free of a scheduling policy it cannot choose for every host.
No annotation; infer deferral. There is no sound way to infer that a method must be deferred; it is a contract about reentrancy and return, which the author states explicitly.

Drawbacks

Two dispatch modes are more surface area than one, and authors must learn when a method should be a cast (no return, may arrive reentrantly-deferred) vs a call.
Addressing introduces instance identity, which Frame has so far avoided; it must be designed carefully to not become an ambient global registry.
A mailbox is unbounded by default; hosts need a bound or back-pressure policy (interacts with RFC-0036’s fixed-capacity storage).

Migration

Source-additive; no breaking change. Existing interface methods are calls and behave exactly as before. @@[cast] is opt-in. Hosts that never cast never need a drain loop. New glossary entries (cast, mailbox, drain, address, reply-to) accompany acceptance.

Unresolved questions

Address representation. Opaque per-system handle, a process-style identity, or a typed reference? Likely a companion sub-RFC.
Mailbox bound + overflow policy (drop, block, error), and how it composes with RFC-0036 fixed-capacity event storage.
Ordering guarantees across casts from different sources to one mailbox, and whether self-casts are ordered ahead of or behind external casts.
Backend mapping beyond Erlang’s native cast: the synchronous backends need a runtime mailbox + the host drain API.

References

RFC-0020 — runtime reference architecture (the synchronous RTC contract this extends).
RFC-0025 — typed event payload (a queued cast carries a typed payload).
RFC-0026 — the Oceans Model as calculus (deferred dispatch must preserve the RTC step the preservation theorem relies on).
RFC-0036 — no-allocation dispatch (a mailbox wants pooled event storage; the two compose).
Frame language reference
Glossary
CHANGELOG.md

RFC-0038 — Deferred dispatch: @@[cast] interface methods, addressing, and a bring-your-own executor