Executing Microservice Applications on Serverless, Correctly
summary
mu2sls is a Python framework that instruments service classes with transactions and asynchronous calls and emits serverless functions plus a logging and concurrency-control runtime. It proves that generated implementations observationally match an ideal specification under crashes and re‑execution, and the prototype runs real microservice apps with fault tolerance while achieving roughly 3–5× throughput over a sequential design and performance comparable to prior manual serverless implementations.
AI-written summary · about
chapters (15)
- 0:00Intro
- 1:40Microservices
- 3:06Microservice Deployment is hard
- 4:21Serverless Benefits
- 4:53Serverless Programmability
- 6:45Contributions
- 8:35Service Specifications
- 11:06mu2sls: Implementation Generation
- 11:46Proof Overview
- 12:30Correctness Theorem
- 13:14Specification and Implementation state
- 14:22Transitions
- 15:12Simulation relation
- 16:14Proof for standard request step
- 17:46Call to action
related talks
01h 00mMicroservices and Serverless
21mHarnessing Microservices for Scalable, Fault-Tolerant ML Systems
28mServerless - the way microservices should be
39mBuilding Highly Scalable Microservices with Serverless
04mServerless applications, Microservices, AWS
41mYou Don’t Want to Build a Serverless Monolith
27mSimplifying Building and Managing Microservices with Micro
30mHow To Build a Python Microservice Without Losing a Job