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 … Continue reading Using TLA+ to Fix a Very Difficult glibc Bug