Checking safety in Exactly-once
summary
Exactly-once is a library that implements atomic commit between business state in Azure Cosmos DB and output messages sent from Azure Functions, relying on optimistic concurrency on Cosmos DB and no cross-partition transactions. A PlusCal/TLA+ model checks safety invariants like AtMostOneStateChange and matching state/version for outputs, finds expected and subtle bugs, reproduces failures on tiny models, and runs a larger 2-process 6-message model in about 2.5 hours.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:46At-Least-Once delivery challenge
- 4:45Duplicate message problem
- 7:18Library design goals
- 8:51Azure Cosmos DB approach
- 9:52Algorithm overview
- 11:48TLA+ model validation
- 14:43Model specification
- 17:59Safety invariants
- 20:12Model checking results
- 24:56Conclusion and resources
related talks
18mNoSQL, YesCosmos: Build that Eventually Consistent Application using Azure Cosmos DB
26m“Hit me, baby, just one time” – Building End-to-End Exactly-Once Apps w/ Flink
28mStateful Applications in the Age of Durable Execution
50mAt Least Once
16mExoFlow: A Universal Workflow System for Exactly-Once DAGs
24mStateful Functions: Flexible like a Microservice, Consistent like a Monolith
31mTurning an Incident Report into a Design Issue with TLA+
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D