Failure transparency proof
View as MarkdownDex has a computer-checked proof that failures add only one thing you can observe: repeated external effects. The proof holds under the conditions in What the proof assumes.
The claim
The proof covers these failures:
- the server crashes and restarts from its durable log;
- a standby server takes over;
- a Step method attempt fails, for example on a Worker error, a timeout, or a Worker disconnect, and Dex retries it;
- a Worker keeps running an attempt after Dex gave up on it;
- a Worker result arrives twice, or arrives after its attempt was replaced;
- a client sends the same StartFlow request again.
It compares runs with these failures to runs of the same Flow without them, in three parts.
- Remove the repeats, and a sequence without failures remains. Remove every repeated external effect from the events of a run with failures so far. The rest is a sequence that the Flow can produce without failures, for the same requests minus the StartFlow retries.
- Every sequence without failures stays possible. A run in which no failure happens produces it.
- Fair runs end the same way. Take the whole event sequence of a fair run with failures, and remove the repeats. The result is the whole event sequence of a fair run without failures. Both runs complete, both get stuck, or both keep running. The reverse direction is proved for requests without StartFlow retries. A retry advances the server's clock, so it can change which timer is due first.
Each repeated effect is an exact copy of an earlier effect of the same Step method.
Combined with the Expressiveness proof, this covers every well-formed program of its small concurrent language. On Dex, such a program produces the events of a run without failures, except that external effects can repeat. For these programs, each extra effect equals an earlier effect in value.
Why repeats stay simple
A Step method can run in several attempts. Every attempt reads the same snapshot: Dex takes it at the first attempt, and every retry reuses it.
The proof assumes that a Step method's effects depend only on what Dex passes it, and not on which attempt is running. Then every attempt computes the same external effects, in the same order.
An attempt makes its effects one after another, so each effect first appears in list order. The first copy can come from any attempt, including an old one that Dex gave up on. Every later copy is a repeat. No attempt adds a new effect or changes the order of the first copies.
What this means for your code
Make each external call safe to repeat and safe to arrive late. A retry can run a Step method's external calls again. An older attempt can make a call late, after a newer attempt made the same call. The proof does not prevent these repeats.
A common way to do this is an idempotency key that the external system deduplicates on. Build it from the Flow run, the Step execution, the method, and the effect. The Step guarantees say more about keys.
When a client retries a request:
- StartFlow: reuse the request ID of the first start, set the option that returns the existing run on both the first start and the retry, and keep the default ID reuse policy. The proof then covers the retry if the server's log orders it before Dex purges the closed run. Reaching the server first is not enough. See Start options.
- PublishToChannel: a request sent again after a lost response is a second request, and it can publish the message twice. Publishing once through RPC request IDs is planned in issue 1519.
- StopFlow: a retry without a run ID can stop a newer run of the same Flow ID. Passing a run ID is planned in issue 1520.
What the proof assumes
The proof holds under these conditions:
- The scope of the expressiveness proof. One Flow is started once and receives Channel messages. Under failures, RPCs, SubFlows, StopFlow, and Attribute locks are outside the proof.
- SYNC methods only. An ASYNC method can lose its start in a server crash. It then runs again on a new snapshot, so its effects can differ.
- Retries never run out, and every error is retryable. Running out of retries, or a non-retryable error, fails the Flow. Without failures, a Flow fails only when its own code fails it. A long server outage can use up the retry time.
- No failure policy. A policy that proceeds after a failure changes what runs next.
- Code ignores its attempt. Effects and results do not depend on the attempt number, the first attempt time, the last error, or the last heartbeat value. Code that resumes from a heartbeat checkpoint is outside the proof.
- No hard-delete Attributes. Dex reads them again on every attempt.
- Every attempt command names its task. The server tags each command of a started attempt, such as its result, a heartbeat, or its failure, with the task that ran it. Every logged command of this kind carries the tag.
- The clock does not step back. On one server, the clock does not step back between checking that a timer is due and stamping the command that fires it.
- Timers fire in order. Each firing takes the earliest due timers first, ordered by fire time, and timers due at the same time in a fixed order. The real server has a short window in which it can fire a timer while an earlier-due timer still waits. Both proofs leave that window out.
- One server at a time. A standby takeover is covered. Several servers that own the same Flows at once are not.
The ending part of the claim holds for fair runs. A run is fair when:
- Every request of the outcome word gets its final outcome, in order. The outcome word lists the client requests in the order of their final outcomes. A request lost before any outcome is not in it.
- The server's clock grows without bound.
- Failures happen only finitely often, and the server comes back after each crash.
- A timer that stays armed and due eventually fires.
- A Step method that stays ready to start while the server is up eventually starts.
- Every Worker task, including an abandoned one, eventually finishes or is dropped.
- Every finished result eventually commits or is ignored.
- Every attempt that a crash interrupted is eventually handled, or cleared by a later crash.
Server time and real time
The proof measures time in the server's stamps. By those stamps, a timer never fires before its time. A server clock that runs ahead can still fire it early in real time.
How it was checked
- A written failure model. Every failure rule is written down with the server code that implements it. Reviewers checked each rule against that code.
- A computer-checked proof. The proof is written in the Lean proof assistant, which checks every step.
- Tests before the proof. A fuzzer walked random runs with crashes, retries, and late attempts, and checked the argument at every step.
- Examples and counterexamples. The proof assistant checks example runs with a crash, retries, and a late repeated effect, and applies the proof to them. It also checks runs that break an assumption, such as code that reads its attempt number, and shows that the claim then fails.