Completed
Adding another condition New rule! All online servers must be running the same version
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
