3 ms·
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?
by remexre 6y ago
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 6y agoThis 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 6y agoThis 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.