Explore a powerful approach to ensuring code quality in concurrent systems through model-checking in this conference talk from NDC Oslo 2020. Learn how to use TLA+, a design and model-checking system, to detect potential concurrency errors at design time and increase confidence in your code. Discover the limitations of conventional practices like unit tests and code reviews when dealing with concurrent systems, and see how model-checking can overcome these challenges. Follow along as the speaker demonstrates the application of TLA+ to various scenarios, including a sort algorithm, a producer/consumer system, and a zero-downtime deployment. Gain insights into boolean logic, state transitions, temporal properties, and how to refactor and improve designs using TLA+. By the end of this talk, acquire valuable tools and techniques to build more robust and reliable concurrent systems.
Building Confidence in Concurrent Code with a Model Checker
Overview
Syllabus
Intro
Why concurrent code in particular?
Tools to improve confidence
A good model is a tool for thinking
What is "model checking"?
Two popular model checkers
Outline of this talk
Here's a spec for a sort algorithm
What is your confidence in the design of this sort algorith
Some approaches to gain confidence • Careful inspection and code review
A concurrent producer/consumer system
A spec for a producer/consumer system Given a bounded queue of items And 1 producer, i consumer running concurrently
What is your confidence in the design of this producerlconsume 28.6%
What is your confidence in the design of this producer consumer
How to gain confidence for concurrency?
Boolean Logic
States and transitions for a chess game
States and transitions for deliveries
Actions are not assignments. Actions are tests
Count to three, refactored
Updated "Count to three"
What is the difference between these two systems!
"Count to three" with stuttering
Useful properties to check
Properties for "count to three" In TLA
Adding properties to the script
If we run the model checker, how many of these proper
Who forgot about stuttering?
How to fix? Refactor #1: change the spec to merge init/next
The complete spec with fairness
Modeling a Producer/Consumer system
States for a Producer
States for a Consumer
Complete TLA* script (2/2)
And if we run this script?
TLA plus... Set theory
Fixing the error
Using TLA* as a tool to improve design
Modeling a zero-downtime deployment
Stop and check
Temporal properties
Running the script
Adding another condition New rule! All online servers must be running the same version
Taught by
NDC Conferences
