Building Confidence in Concurrent Code with a Model Checker

Building Confidence in Concurrent Code with a Model Checker

NDC Conferences via YouTube Direct link

Running the script

42 of 43

42 of 43

Running the script

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

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.