Executable Models of Async/Await🔗ℹ

1 The Tower🔗ℹ

Each language model is the top floor of a small tower, and only the top floor differs between languages:

• oopsla26-async-await/lc — a call-by-value λ-calculus with state, lists, structs, and delimited control. The control operators (reset/shift) are how tasks suspend; everything else is furniture.

• oopsla26-async-await/exn — exceptions: throw, catch, and throw-in, which raises inside a suspended coroutine. Cancellation will want that.

• "platform.rkt" — the machine. A configuration is (t σ Q T P): a logical clock, a store, a ready queue, a timer table, and a pool of threads. The platform supplies blocking (os/block), timed I/O (os/io), the scheduler rules, and the define-extended-ev-system form that each language instantiates. Time is logical: os/io promises at least its delay, and the clock jumps to pending deadlines.

• one module per language — the surface forms (async/lambda, await, and whichever of spawn, cancel, or timeout the language actually offers) and their reduction rules.

The payoff of the layering: when two models disagree about a program, the disagreement lives in one file, and it is a semantic decision, not plumbing.

2 Module Reference🔗ℹ

Every language module exports exactly three identifiers, consistently named. For a language L: the language itself; –>L, the relation that runs programs (deterministic scheduler spines are collapsed into single steps, so test-->> converges quickly); and –>>L, the non-collapsing variant that exposes every successor state — use it when you want the whole interleaving space, not just an execution.

3 Core calculus🔗ℹ

The grammar, abridged (arithmetic, comparison, and string forms elided):

Two features earn their keep. reset/shift are delimited control — every async language above builds task suspension out of them: a task body runs inside a reset, and awaiting captures the rest of the body with shift as a continuation to park. And the store σ maps names to values through (ptr x) references, so tasks, boxes, and structs are heap objects that survive across suspensions.

4 Exceptions🔗ℹ

The grammar extension:

A throw unwinds — through a dedicated propagation context, G — to the nearest enclosing catch, whose handler receives the payload. throw-in is the asynchronous variant: it arms a suspended coroutine so that the exception raises inside it when it next resumes. The async languages implement cancellation with it — a cancelled task is one that wakes up to an exception it never threw.

5 Platform🔗ℹ

The machine every async language runs on. A configuration is (t σ Q T P):

a logical clock, the store, a ready queue of labeled thunks, a timer table of thunks due at a deadline, and a pool of threads, each a stack of labeled frames. The platform also extends the expression grammar with the os/* hooks a language’s rules schedule work through:

os/block parks the root thread on an awaitable (this is how a program’s main runs); os/io performs I/O that takes at least e_delay logical steps — time is logical, and the clock jumps to pending deadlines rather than ticking.

#:single-threaded makes synchronous code run unbounded on one thread (an infinite loop blocks the runtime, as in a real event loop); #:serial-dispatch selects run-to-completion event-loop dispatch, microtasks before timers. They are independent — Trio uses the first without the second.

The form also injects (deliberately unhygienically) the vocabulary your rules will use: async/main (wraps a surface program into an initial machine state, (async/main #:threads n e)); make-big-step (collapses deterministic scheduler spines); program-output and prog/equiv (observation and equivalence for tests); queue operations Q:push/Q:pop and T:push/T:pop; and the task:* family — task:allocate, task:set-done!, task:set-failed!, task:set-cancelled!, task:is-completed?, task:continue-with, task:add-self-as-dependent!, task:get-dependents, and friends.

6 Python asyncio🔗ℹ

7 Python Trio🔗ℹ

8 JavaScript🔗ℹ

9 C#🔗ℹ

10 Swift🔗ℹ

11 Rust tokio🔗ℹ

12 Rust smol🔗ℹ

13 Python substrate🔗ℹ

14 Rust substrate🔗ℹ

15 Type checker🔗ℹ

16 Writing Your Own🔗ℹ

Suppose your language isn’t here. Resist the urge to start from nothing.

1. Pick the nearest neighbor and copy it. Eager task start? Read oopsla26-async-await/csharp or oopsla26-async-await/swift. Lazy? Read oopsla26-async-await/aio or oopsla26-async-await/tokio.

2. Decide the semantics before writing rules. Four questions do most of the work: Does calling an async function run it (eager) or build a value (lazy)? Does awaiting a completed task suspend anyway? What keeps an unawaited task alive — a handle, the runtime, a scope? And who dies at cancellation — a task, or a tree of them? Every pair of answers you can observe with a three-line program; the models exist because runtimes answer differently.

3. Extend the machine. define-extended-ev-system takes your new expression forms and their evaluation-context holes (E, M, G). Forgetting the holes is the classic mistake: your form will parse and then silently never reduce.

4. Write the scheduler interaction as rules. Dispatch (what runs next) and delivery (what a due or cancelled timer does) are where languages hide their personality. Keep each rule small; name it after the runtime behavior it mimics.

5. Test with test-->>. Start with the three-line observation programs from step 2, and run them against the real language too — by hand is fine. That comparison is where our models’ bugs were found, and yours will be too.

17 Testing🔗ℹ

Each model’s test submodule is pure Redex — no external toolchains required. The full validation against the real runtimes is part of the paper’s artifact, not this package.