Building confidence in concurrent code with a model checker

on YouTube ↗01h 04m

" summary

Demonstrates using TLA+ and the TLC model checker to find real concurrency bugs: a queue model with max size 2 checks 1 producer/1 consumer (8 states) and shows the producer/consumer with 2 producers 2 consumers fails invariant (38 states, counterexample trace where bounds are violated). Shows subtle stuttering/fairness issues when counting to three, models a zero‑downtime deployment, finds a downtime counterexample, and fixes it with a one‑at‑a‑time rule plus a load‑balancer model; checks succeed.

AI-written summary · about

" chapters (43)

1. 0:00Intro
2. 1:01Why concurrent code in particular?
3. 2:23Tools to improve confidence
4. 3:34A good model is a tool for thinking
5. 4:14What is "model checking"?
6. 4:53Two popular model checkers
7. 7:27Outline of this talk
8. 8:00Here's a spec for a sort algorithm
9. 9:11What is your confidence in the design of this sort algorith
10. 9:59Some approaches to gain confidence • Careful inspection and code review
11. 11:06A concurrent producer/consumer system
12. 11:37A spec for a producer/consumer system Given a bounded queue of items And 1 producer, i consumer running concurrently
13. 12:43What is your confidence in the design of this producerlconsume 28.6%
14. 14:00What is your confidence in the design of this producer consumer
15. 15:06How to gain confidence for concurrency?
16. 17:34Boolean Logic
17. 19:31States and transitions for a chess game
18. 19:44States and transitions for deliveries
19. 21:27Actions are not assignments. Actions are tests
20. 24:31Count to three, refactored
21. 27:29Updated "Count to three"
22. 28:22What is the difference between these two systems!
23. 29:16"Count to three" with stuttering
24. 30:51Useful properties to check
25. 32:11Properties for "count to three" In TLA
26. 33:28Adding properties to the script
27. 34:59If we run the model checker, how many of these proper
28. 35:58Who forgot about stuttering?
29. 37:40How to fix? Refactor #1: change the spec to merge init/next
30. 39:19The complete spec with fairness
31. 40:31Modeling a Producer/Consumer system
32. 40:49States for a Producer
33. 43:31States for a Consumer
34. 44:13Complete TLA* script (2/2)
35. 46:50And if we run this script?
36. 47:33TLA plus... Set theory
37. 52:21Fixing the error
38. 53:39Using TLA* as a tool to improve design
39. 54:18Modeling a zero-downtime deployment
40. 56:30Stop and check
41. 56:49Temporal properties
42. 57:45Running the script
43. 59:21Adding another condition New rule! All online servers must be running the same version

" related talks

• 01h 07mBuilding confidence in concurrent code with a model checkerScott Wlaschin · NDC London 2023
• 49mThinking in a Highly Concurrent, Mostly-functional LanguageFrancesco Cesarini · ElixirConf 2014
• 38mAccidentally ConcurrentEvan Czaplicki · Code Mesh 2015
• 22mConcurrency Models DemystifiedHarish Kandala · DevWorld 2024
• 58mDesign and Implementation of Highly Scalable Quantifiable Data Structures in C++Christina Peterson, Victor Cook, Zachary Painter · CppCon 2021
• 42mHistory of ConcurrencyMichael Schurter · Open Source Bridge 2014
• 55mBehavioral Modeling in HW/SW Co-design Using C++ CoroutinesJeffrey Erickson, Sebastian Schoenberg · CppCon 2023
• 55mC++ Concurrency TS 2 Use Cases and Future DirectionMichael S Wong, Maged M. Michael, Paul E. McKenney · CppCon 2022