Opening this issue so we can refer to it later: It may be advantageous to use a HoareSet for MayLocksets instead of our naive set representation for which the operations are quadratic in the size of the sets.

Independently of this, we need to rethink our approach to MayLocks as it pertains to deadlock detection in general.