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