§9 · Durability semantics

Status: DRAFT. The classification, its lattice, and where the compiler places a durable step are probed — the first two through osy model --json, the third read from the resolver that performs the lowering. What a crash actually does is runtime behaviour and is UNVERIFIED here; §9.7 names the guards.

§11.1 and §11.2 both refuse a C# construct "because a call can suspend and resume in a different process". This section is that claim, stated properly. It is the reason the language has no out parameter and no async.

9.1 The premise

Normative. A call MUST NOT assume that the process which began it is the process which finishes it.

Everything below follows from that one sentence. An Osy# call may suspend — for a timer, for a human, for a child workflow — and resume later, elsewhere. So the stack frame is not a durable place: nothing may be written back into it (§11.1), and nothing may be scheduled against it (§11.2).

⭐ The interesting consequence is that a re-run is normal, not exceptional. A continuation-based engine replays nothing wholesale, but it does re-execute in two places: a statement is replayed after an in-process sub-call returns, and a statement that suspended is re-entered on resume. So "what does it cost to run this leaf twice" is a question the engine must be able to ask of every leaf in the program — which is what §9.2 is.

9.2 The durability classification

Every leaf the language provides carries one of three values.

Source: StdlibDurability, Platform.Core/Dsl/OsySharp/Stdlib/OsySharpStdlib.cs.

Normative. The three values form a total order — Deterministic < Nondeterministic < External — and the durability of a construct MUST be the maximum over its parts. That is what makes the classification usable as a lattice over whole programs rather than only over the leaves it was defined on.

⚠ External is about whose system rolls back, not about I/O. A commit to the application's own database is Nondeterministic: the platform owns the transaction. File.WriteAllText is External: the filesystem does not roll back because a later segment failed.

9.3 Asking a program what it costs

Normative. An implementation MUST report the classification, and MUST report a witness for it.

⚑ Probed 2026-08-27. For a function whose body is Security.RandomId() and then File.WriteAllText(path, id) — a Nondeterministic leaf written first and an External leaf written second — osy model --json reports:

Archive   direct: External   durabilityVia = File.WriteAllText
Wrapper   direct: Deterministic          via = (none)
          trans : External   durabilityVia = Archive → File.WriteAllText

Three separable facts, each of which a reader would plausibly guess wrong:

1. The lattice wins over source order. External is reported although the nondeterministic call is written first. The value is a max, not a last-writer.
2. durabilityVia is a path, not a name. Through a call graph it reads Archive → File.WriteAllText — the route by which a plain-looking call reaches an egress. This is the field that makes the classification actionable rather than merely present.
3. effects and transitive are different answers and both are given. Wrapper calls nothing but Archive: it is Deterministic directly and External transitively. A reader who consults only one of them will be wrong about half the functions in any real program.

9.4 Where a durable step goes — the leaf, never the function

Normative. An implementation MUST place the exactly-once boundary at the egress leaf, not at the enclosing function.

⭐ This is the load-bearing design decision of the whole section. If Notify(u) makes external calls A and then B, and the whole of Notify is one coarse step, a crash between A and B re-runs A on resume — a double send. Each egress is therefore its own step, and the deterministic orchestration between them re-runs freely, being a pure function of the memoized results.

It is automatic. The resolver wraps every External leaf in a durable step during lowering. An author writes Http.Get(url) and gets exactly-once without naming it. Workflow.Once("key", …) remains available for a step the author wants to name or key, and an already-stepped leaf is not wrapped twice.

⚠ So the transitive lattice of §9.3 does not decide anything. It is an author-facing signal — "this plain-looking call reaches an egress". Step placement is a purely local decision at each leaf. Reading the lattice as the mechanism gets the model backwards, and is the likeliest misreading of this section.

A nondeterministic leaf gets no step, deliberately. DateTime.UtcNow and Guid.NewGuid ride the per-statement node memo, which already serialises into the continuation. Giving each one its own out-of-band database write would be a real cost for a guarantee they already hold. Only egress — where the second execution reaches someone else's system — earns one.

⚑ An unclassified target defaults to External. A leaf missing from the durability table is treated as egress, so an omission over-protects rather than under-protects. Informative: the platform has been bitten by the resulting symptom more than once, which is itself the argument for the default being this way round.

9.5 A step wraps one thing

int Charge(int amount) { return Workflow.Once("charge", () => amount * 2); }

int Charge(int amount) { return Workflow.Once("charge", () => { var a = amount; return a; }); }

A step body is an expression. Statements go in a function, which the step then calls.

⚠ Informative, and honest about a rough edge: the refusal above is real and stable, but its diagnostic explains itself in terms of query lambdas ("a block can't lower to SQL in a query predicate") because block-bodied lambdas are refused language-wide from one site. At a durable-step call site that reason is not the applicable one. The refusal is right; the explanation is aimed elsewhere. Recorded as a §12 diagnostics concern.

9.6 await means park

Restating §11.2 from this side, because it only makes sense here: await Workflow.Run(…) does not yield a thread. It parks the run durably — possibly for days — and resumes it in whatever process next picks it up. The keyword is reused because the English reading is right; the mechanism is this engine, not a task scheduler.

9.7 What this section does NOT establish

UNVERIFIED, deliberately. Every claim above is about what the compiler classifies and lowers. None of it establishes what a crash does. Specifically unproven here:

• that a step's result survives a process restart and is not re-executed on resume;
• that a memoized nondeterministic value is the same value after resume;
• that a durable step commits out-of-band, so a crash before the enclosing segment commits still finds it.

Those need runtime tests. The guards that exist are AutoDurableLoweringTests (the leaf-level wrap), WorkflowOnceDurableStepTests and WorkflowStepMemoIdentityTests (memo identity across a resume), DurableFunctionRunnerTests (resume itself), and FunctionEffectsDurabilityTests with OsySharpStdlibDurabilityTests (the classification and its rollup). A future revision MUST cite which of them proves which of the three claims above, or drop the claim.

Next: §8 Security as a language rule — the other declaration-time rule, and the one with the most surface. Not started.