Formal Modeling and Analysis of Distributed Systems

on YouTube ↗39m

" summary

P is a state-machine programming language and open-source framework that models distributed components as communicating state machines, attaches runtime monitors as executable specifications, and runs a prioritized, portfolio-style checker on clusters. It finds surprising design bugs — hundreds in the original USB 3.0 driver work and multiple design faults during S3’s strong-consistency effort — emits reproducible traces and schedules, plugs into CI/CD, and narrows the gap between high-level design and implementation.

AI-written summary · about

" chapters (12)

1. 0:00Intro
2. 1:01Programming Distributed Systems is Challenging!
3. 2:18Not uncommon to find bugs in production after deployment
4. 2:50Formal Methods to the Rescue!
5. 4:04Thinking abstractly, formally, above coding
6. 7:07Challenges with wide spread adoption of Formal Methods!
7. 12:48Formal Reasoning of S3 Strong Consistency Design using P
8. 14:44Two Phase Commit Protocol
9. 24:06P Tutorials and Documentation
10. 24:20Lessons Learned (P as a Thinking Tool)
11. 27:30Model Checking as a search problem
12. 28:13How to find deep bugs?

" related talks

• 45m(...)Distributed SystemsAlvaro Videla · Erlang User Conference 2015
• 14mFormal specifications for Microservices -Francois Royer · DDD Europe 2020
• 31mDesigning Distributed Systems with TLA+Hillel Wayne · Øredev 2018
• 01h 00mThe Secret Life of Distributed SystemsOleksii Petrov · Software Architecture fwdays'25
• 44mCommunication and Transactionality in Distributed SystemsYozhef Hisem · Software Architecture fwdays'24
• 34mThe Holy Grail of Systems Analysis: from What to Where to WhyDaniel Spoonhower · Strange Loop 2017
• 43mBuilding Robust Systems with Weakly Interacting Feedback StructuresPeter Van Roy · Code Mesh 2017
• 36mFlying Spaghetti Monster - Type Systems and MicroservicesChris Ford · Code Mesh 2017