On: Is there a known recent Linux locking bug that affects the OCaml runtime?

[remexre]

I'm kinda surprised none of the model-checking people have tried verifying glibc's NPTL implementation; I guess it might be hard to formalize futex's behavior?

[javert → remexre]

This sounds to me like a good PhD project and/or series of research papers.

Disclaimer: I'm not in the model-checking community.

If it's hard to formalize futex's behavior, all the better for academics, though it's unfortunate for the rest of us.

[mbac32768 → remexre]

This bug is really, really subtle. The repro that was posted that just tries to stress this bug can take hours to deadlock on some machines. Confirming that you've fixed it properly is a bit harrowing.

Even as an OCaml snob I haven't a clue how you would verify the behavior of this C library formally.