Exploring and improving the design of Abaco
summary
They build a TLA+ spec and run the TLC model checker to expose a race that lets new executions start with stale container images on Abaco, a production FaaS with ~50,000 actors and two+ years live. Fixes: add a monotonic image revision per actor, start workers with a revision, block creating new workers when idle workers exist, delete idle workers with stale revisions, and have workers check revisions before pulling messages. The revised model satisfies the worker-image invariant; implementation and TLA+ proofs are next. TLA+ spec TLC model checker
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:18Talk Outline
- 1:17Introductions
- 2:02Texas Advanced Computing Center (TACC)
- 4:20Cloud Software for Research and TLA.
- 6:23Abaco Functions-as-a-service
- 8:04Abaco: Basic Usage
- 9:34Abaco Architecture
- 11:28Observed Issues at Scale
- 13:40Spec Overview (1)
- 16:41Finding A Problem in the Design (1)
- 19:48Initial Outcomes: Insights and Design Changes (1)
- 23:56Next Steps
related talks
24mTLA+: Your Secret Weapon Against Concurrency Hell
39mWeeks of Debugging Can Save You Hours of TLA+
41mDesigning software with complex configurations
27mSimple Abstractions for the Challenge of Complexity
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
01h 02mTools for simplified large scale systems
24mContaining Agent Chaos
44mAI Architecture Thinking: From Idea to Impact