Correctness and expressiveness
View as MarkdownThis section answers two questions about Dex.
- Expressiveness: can Dex express the programs you need?
- Correctness: does Dex stay correct when processes, machines, or networks fail?
Expressiveness
The Expressiveness proof shows that any program in a small concurrent language, with threads, locks, timers, and cancellation, can be written as a Dex Flow that behaves the same. A computer checks every step of the proof. The paper has the full argument.
The Workflow Patterns evaluation rates Dex against the 43 control-flow Workflow Patterns. Researchers use these patterns to compare workflow languages and engines. Each rating comes with a runnable example and an integration test.
Correctness
The Step guarantees state what Dex promises when a Step method fails or runs again.
The Failure transparency proof covers server crashes, standby takeovers, retries, Workers that keep running after Dex gave up on them, and duplicate results. These failures add only repeated external effects: remove them, and the rest is a sequence the Flow can produce without failures. For fair runs, the ending stays the same too. The proof's page lists its conditions, such as SYNC methods only and retries that never run out. This proof is also computer-checked, and the same paper has the full argument.
Combined, the two proofs cover every well-formed program of the small concurrent language. On Dex, such a program produces the events of a run without failures, except that external effects can repeat, and a repeat can come late. What this means for your code says how to make repeats safe.