I unfortunately didn't have time to go through:
- compiling glibc from source
- converting my code to C
- trying to reduce multithreaded synchronization code to a minimal example given how non-deterministic any of those bugs are
- do a write-up
That said, it seems like people went through the motions 4 months after me in this bug:
- https://sourceware.org/bugzilla/show_bug.cgi?id=25847 which affects C#, OCaml, Python
Someone also fully reimplemented Glibc condition variable in TLA+ to prove that the glibc code was buggy:
- https://probablydance.com/2020/10/31/using-tla-in-the-real-w... (at the bottom)