Cancelable locks
It would be really useful to have a version of cancelable locks, where the is_lock
predicate is equipped with a fraction. That way, we could have a couple of things:
- A Hoare triple for the physical free operation
{{ is_lock lk 1 R }} free lk {{ R }}
- A rule
is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')
that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be DfracDiscarded
.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip
is_lock
with a fraction, or do we want to add a tokenlock_own
(which would be timeless). - If we equip
is_lock
with a fraction, we won't break backwards compatibility that much. One just needs to addDfracDiscarded
everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course defineis_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded
or something like that.
Any thoughts?