[tlaplus] Using TLA+ to Fix a Very Difficult glibc Bug - Malte Skarupke - C++Now 2025

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Using TLA+ to Fix a Very Difficult glibc Bug - Malte Skarupke - C++Now 2025

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.

https://www.youtube.com/watch?v=Brgfp7_OP2c

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/3573DF3E-A86E-401A-92C7-6F69A5DA6DCA%40lemmster.de.