The glibc condition variable (meaning std::condition_variable) was subtly broken for years, breaking Python, C#, OCaml and countless programs. There were various attempted fixes but nobody seemed to fully understand this complex implementation of condition variables. I used the formal specification language TLA+ to model glibc condition variables and to reproduce the bug, figure out which of the patches actually worked (not the one everyone was using) and then used my TLA+ implementation to reason about the working patch, allowing me to clean it up and simplify it. I will show how you can take complex real world C code and do a straightforward translation into TLA+. It really is quite a pleasure to use since it has a simple model of "just run all interleavings of all threads" that makes it easy to translate code and to reason about what simplifications are necessary.
View Slides
I do formal verification of glibc for fun, or write a new sorting algorithm. At home I like working on algorithms, at work I tend to work on testing or performance.
I have 12 years of industry experience. For the last five years I have worked in finance, writing Ocaml, Python and CUDA. Before that I wrote C++ for 7 years in video games.
I gave two previous talks, one on generalized radix sorting in 2017 and one on fast hash tables in 2018. I blog at www.probablydance.com