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 fut

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.