Automated Verification of Idempotence for Stateful Serverless Applications
summary
Flux presents a verifier and advisor that check and fix idempotence for stateful serverless apps by proving a new correctness notion idempotence consistency and a compositional proof rule called idempotence simulation. It instruments each function (f) to model retries, applies failure reduction* to bound crash interleavings, and suggests a minimal set of operations to log. Evaluated on 27 apps (79 functions), Flux finds issues in 12 apps (8 confirmed), verifies apps in <110s, proposes fixes in <90s, and yields up to 6× lower latency and 10× higher peak throughput vs full-operation logging.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:34Idempotence challenges
- 2:39Existing solutions limits
- 3:19CornFlux overview
- 4:02Idempotence definition
- 6:12Consistency model
- 7:14Automated verification
- 8:41Feeding reduction
- 9:43Repairing inconsistencies
- 11:56Evaluation results
- 13:02Conclusion
related talks
40mThe State of Serverless Computing
27mStateful Functions 3.0: Towards a Cross-Platform Stateful Serverless Stack
50mAutomated Serverless Security Testing: Delivering secure apps continuously
34mHands-on Stateful Serverless Applications with Kubernetes and Stateful Functions
35mHands-On Stateful Serverless Applications with K8s and Stateful Functions
38mOne Serverless Principle to Rule Them All: Idempotency
42mHelp! I've created a serverless monolith!
24mServerless powered Low Code