Using TLA+ to Fix a Very Difficult glibc Bug

Explore how formal specification language TLA+ can be used to model, debug, and fix complex concurrency issues in real-world C code through a detailed case study of a subtle glibc condition variable bug. Learn about a years-long bug in glibc's condition variable implementation that affected major programming languages including Python, C#, and OCaml, and discover how TLA+ modeling helped identify the root cause when traditional debugging approaches failed. Follow the systematic process of translating complex C code into TLA+ specifications, using TLA+'s "run all interleavings of all threads" model to reproduce the bug and evaluate various proposed patches. Understand how formal verification techniques can distinguish between working and non-working fixes, and see how TLA+ modeling enabled the simplification and cleanup of the final patch. Gain practical insights into applying formal methods to concurrent programming challenges, with demonstrations of straightforward translation techniques from C code to TLA+ specifications. The presentation includes real-world examples of how formal verification can solve problems that stumped experienced developers for years, making TLA+ accessible for debugging complex multithreaded code.