Building confidence in concurrent code with a model checker - Scott Wlaschin - NDC London 2023

Verifying the correctness of concurrent code with a model checker using TLA+, a technique to build confidence in complex systems with concurrent producers and consumers.

Key takeaways

Model checking is a technique to verify the correctness of concurrent code.
The speaker uses TLA+ (Temporal Logic and Actions Plus) to model and verifying a system with concurrent producers and consumers.
The system has two versions, V1 and V2, and a load balancer is used to manage the transitions between them.
The speaker uses a poll question to illustrate the benefits of model checking in concurrent systems.
The system has properties such as zero downtime and eventually true that X equals three.
The speaker demonstrates how to use TLA+ to model the system and verify its correctness using a model checker.
The speaker also discusses the importance of confidence in concurrent code and how model checking can help achieve that confidence.

Building confidence in concurrent code with a model checker - Scott Wlaschin - NDC London 2023

More talks