Building confidence in concurrent code with a model checker

on YouTube ↗01h 07m

" summary

Demonstrates using TLA+ / TLC to model-check concurrency: a count-to-three model reveals a deadlock reached until a loop (stuttering) and weak fairness are added; a producer/consumer model shows one-producer/one-consumer passes but two-producer/two-consumer fails (the model explores ~38 interleavings); a zero‑downtime deployment model is built with server-state maps and a load balancer and evolves through counterexamples to a working design. Models are compact (≈50 lines) and the checker gives concrete failing traces to guide fixes.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 1:04Why focus on concurrency
3. 3:57Model checking and TLA Plus
4. 9:57Confidence in concurrency
5. 15:12TLA Plus syntax and concepts
6. 22:16Model counting to three
7. 29:37Temporal properties and fairness
8. 38:46Producer-consumer basics
9. 46:49Multiple producer-consumer
10. 53:08Zero downtime deployment
11. 1:03:17Summary

" related talks

• 01h 04mBuilding confidence in concurrent code with a model checkerScott Wlaschin · NDC Oslo 2020
• 22mConcurrency Models DemystifiedHarish Kandala · DevWorld 2024
• 38mAccidentally ConcurrentEvan Czaplicki · Code Mesh 2015
• 49mThinking in a Highly Concurrent, Mostly-functional LanguageFrancesco Cesarini · ElixirConf 2014
• 42mHistory of ConcurrencyMichael Schurter · Open Source Bridge 2014
• 55mBehavioral Modeling in HW/SW Co-design Using C++ CoroutinesJeffrey Erickson, Sebastian Schoenberg · CppCon 2023
• 40mDistributed, Eventually Consistent ComputationsChristopher S. Meiklejohn · Strange Loop 2015
• 01h 04mA Pattern Language for Expressing Concurrency in CppLucian Radu Teodorescu · CppCon 2022