"Tackling Concurrency Bugs with TLA+" by Hillel Wayne

Hillel Wayne introduces TLAPlus and PlusCal, demonstrating how to write specifications to catch complex concurrency bugs in system designs.

Concurrency is hard. How do you test your system when it's spread across three services and four languages? Unit testing and type systems only take us so far. At some point we need new tools. Enter TLA+. TLA+ is a specification language that describes your system and the properties you want. This makes it a fantastic complement to testing: not only can you check your code, you can check your design, too! TLA+ is especially effective for testing concurrency problems, like stalling, race conditions, and dropped messages. This talk will introduce the ideas behind TLA+ and how it works, with a focus on practical examples. We'll also show how it caught complex bugs in our systems, as well as how you can start applying it to your own work. Hillel Wayne ESPARK LEARNING Hillel is a senior software engineer at eSpark Learning. He enjoys technical writing and is the author of Learn TLA+ (learntla.com). In his free time he juggles and makes chocolates. He _probably_ brought enough for everyone.