Building Confidence in Concurrent Code with a Model Checker
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.