An abstraction for enforcing a mutual-exclusion invariant