How do you statically guarantee the order of lock acquisition for a thread? I think either you have simple enough control flow that it is somehow entirely visible to the compiler or you need to embed the order into the type system like this approach does.