Add lock interface

@jung looks good?

I like this idea. I have some remarks that I will write down tomorrow.

Firstly, I think we should have a self-contained file with the lock interface, that is then imported by any lock implementation.

Secondly, to make Coq able to automatically infer the instance for each lock implementation, we should probably use type classes or canonical structures for it. I have included an attempt for the interface using canonical structures in this message.

From iris.heap_lang Require Export heap.
From iris.heap_lang Require Import notation.

Structure lock Σ `{!heapG Σ} := Lock {
  newlock : val;
  acquire : val;
  release : val;
  is_lock : namespace → val → iProp Σ → iProp Σ;
  locked : namespace → val → iProp Σ → iProp Σ;
  (* general properties *)
  is_lock_ne N lk n : Proper (dist n ==> dist n) (is_lock N lk);
  locked_ne N lk n : Proper (dist n ==> dist n) (locked N lk);
  is_lock_persistent N lk R : PersistentP (is_lock N lk R);
  locked_is_lock N lk R : locked N lk R ⊢ is_lock N lk R;
  (* operations *)
  newlock_spec N R Φ :
    heapN ⊥ N →
    heap_ctx ★ R ★ (∀ lk, is_lock N lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }};
  acquire_spec N lk R Φ :
    heapN ⊥ N →
    is_lock N lk R ★ (locked N lk R -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
  release_spec N R lk Φ :
    heapN ⊥ N →
    locked N lk R ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
}.

Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
Arguments is_lock {_ _} _ _ _ _.
Arguments locked {_ _} _ _ _ _.

Existing Instances is_lock_ne locked_ne is_lock_persistent.

Instance is_lock_proper `{!heapG Σ} (L : lock Σ) N  lk:
  Proper ((≡) ==> (≡)) (is_lock L N lk) := ne_proper _.
Instance locked_proper `{!heapG Σ} (L : lock Σ) N  lk:
  Proper ((≡) ==> (≡)) (locked L N lk) := ne_proper _.

(Maybe it would be convenient to also have a LockMixin akin to what we have for COFEs and CMRAs).

Furthermore, we should also include properties for non-expansiveness of the lock predicates, as well as persistence of is_lock. I have done this in the excerpt above.

Marked this merge request as a Work In Progress

Added 1 commit:

• e122ad08 - revise

I have revised part of code, basically using Structure and specialize the N and HN to certain members. But is_lock_proper and locked_proper can't compile now. cryptic context problem again.

Also, I have some problems regarding the code in your comment:

• Why the !lockG Σ is dropped? ... and yes, that is a problem how should I provide this lockG: gFunctors Set (or Set? if applied to Σ in some way ...).
• I thought that Mixin is used as a engineering practice towards the "CMRA is also a COFE" and the bundled/unbundled problem. (I heard Ralf explained this to me once but now I forgot 90% of them I believe :P it would be nice if there is some doc on it)
• About where to put the instantiation in, I wrote it in lock.v because it really makes me feel uneasy that the implementation and interface instantiation are exposed by the same file (is there a way to abstract the instantiation without exposing the implementation?) But never mind, it is a minor problem.

I should also try to write an illustrative client example someday.

Why the lockG Σ is dropped?

These type classes lockG are specific to implementations, and do not have much to do with the interface. They should become parameters of the instance, not parameters of the lock interface.

Also, notice that ``{!heapG Σ, !lockG Σ}` is probably not doing what you expect. It expands to:

(Σ : gFunctors) (heapG0 : heapG Σ) (lockG : gFunctors → Type) (lockG0 : lockG Σ)

So, as you see, it it generalizing over some arbitrary lockG and an arbitrary inhabitant lockG0 of it. Moreover, if you look at it the parameters of your mkLock, you see that both are unused, so, you may as well remove them. Your lockG parameters are also the reason that is_lock_proper and locked_proper do not work: they are not connected to anything, so Coq cannot infer them.

I thought that Mixin is used as a engineering practice towards the "CMRA is also a COFE" and the bundled/unbundled problem.

That is so, but they can also be used to save keystrokes, even when you are not doing inheritance. So, in this case, when declaring an instance, you just have to state a lemma corresponding to the mixin (which would contain all the properties of the lock) , instead of having to state a lemma for each individual property.

By the way: we typically let the name of a canonical structure start with a lower case, and used a CamelCased version of the name as the constructor. Also, please align the structure in the same way as done for the COFE and CMRA structures.

By the way 2: I am not sure I very much like it that the premise (HN: heapN ⊥ N) appears before lk R (Φ : val → iProp Σ). I know this was already the case in the earlier lock implementations because we used the section mechanism, but when using the theorems, it usually best to have all forall quantifiers up front because the Coq tactics can deal better with that.

Thanks for comments :)

These type classes lockG are specific to implementations, and do not have much to do with the interface. They should become parameters of the instance, not parameters of the lock interface.

Oh, I get it. I was thinking that the interface has to offer what particular gFunctors the implementation is using, so client can put it inside its context, thus justify the use of lemmas. But well, looks like there is some auto-magic going on here? I will make up some example to observe how it works later.

(HN: heapN ⊥ N) appears before lk R (Φ : val → iProp Σ)

I actually tried to solve this funny problem by rewriting the argument in a way like (fun A B C => f C A B), but it looks too funny to me thus I just gave it up :/ Will it be better to modify the section context or to doing interfacing hacks like the one above?

Will it be better to modify the section context or to doing interfacing hacks like the one above?

Yes, I think that is right. Just take HN: heapN ⊥ N out of the section parameters, and put it as a premise of the lemmas.

Added 1 commit:

• 3f3ead35 - Add lock interface

Revised

Unmarked this merge request as a Work In Progress

Nice :)

The interface matches how we wrote locks in the Coq sources, but on paper, we usually worked slightly differently. In particular, we made locked timeless so that it can easily be put into invariants -- the current interface is not very well suited to put further abstractions on top of it.

In order to achieve this, we would typically expose the fact that there is a "name" of some sort that logically identifies the lock, like this:

Structure lock Σ `{!heapG Σ} :=
   Lock {
       (* operations *)
       newlock : val;
       acquire : val;
       release : val;
       (* predicates *)
       name: Type;
       is_lock (η: name) (N: namespace) (lock: val) (R: iProp Σ) : iProp Σ;
       locked (η : name) : iProp Σ;
       (* general properties *)
       is_lock_ne η N lk n : Proper (dist n ==> dist n) (is_lock η N lk);
       is_lock_persistent η N  lk R : PersistentP (is_lock η N lk R);
       locked_timeless η : TimelessP (locked η);
       (* operation specs *)
       newlock_spec N (R : iProp Σ) Φ :
         heapN ⊥ N →
         heap_ctx ★ R ★ (∀ η l, is_lock η N l R -★ Φ l) ⊢ WP newlock #() {{ Φ }};
       acquire_spec N η lk R (Φ : val → iProp Σ) :
         heapN ⊥ N →
         is_lock η N lk R ★ (locked η -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
       release_spec η N R lk (Φ : val → iProp Σ) :
         heapN ⊥ N →
         is_lock η N lk R ★ locked η ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
    }.

Of course, this name is rather ugly. It would be nicer if we could somehow tie the is_lock and the locked together via the lk. That's actually possible, but it would need some more general infrastructure: When allocating a location, one could also allocate ghost fields associated with that location. In our case, we could need agreement ghost fields tied to to the name of the ghost state of the lock. Because this is only "legal" when allocating a new location, this kind of ghost heap would have to be tied to heap.v, which is... not pretty. For that reason, on paper, we typically follow this pattern of every library having a "logical name" η for its instances.

@robbertkrebbers @jjourdan we briefly mentioned this yesterday in the call. Did we reach a consensus on how the interface should look?

There needs to be at least something like locked η ★ locked η => False, otherwise the locked predicate is useless. In fact, there is some redundancy here : the fact that we are using R as an invariant and the locked predicate seem to be redundant (we can encode the one using the other).

Right, I forgot to add that law about locked.

In fact, there is some redundancy here

Well, true, we could get entirely rid of the locked predicate if we don't care that a user calling release actually holds the lock.

However, I don't think the two are inter-encodable. Imagine an implementation relying on release only being called when the lock is held (e.g., a spinlock with an assert (!x == 1) in release). If the user picks an R that is duplicable, then release could be called without the lock held. Hence this lock satisfies the above spec, but it doesn't satisfy the spec obtained by removing locked.

Oh, right. But still, the higher order thing is useless and can be derived from the locked token game. You just need an invariant stating something like R ★ tok ∨ locked for some unique token tok.

True. But the spec is more useful if it already encodes the ownership transfer - I'd argue it's the spec people want to use. We could have another spec that doesn't involve the R and show that one implies the other, and make that other spec the one people implement. However, considering how little effort the R is in the proofs of the two locks we have, I am not sure if that's worth it.

Agreed with Ralf, a more useful spec is better than a minimalistic spec.

Well, this is just that the handling of the invariant R is essentially the same reasoning that is going to be repeated in every implementation.

This is maybe a bit far fetched, but another option would be to drop locked, but enforce that R is exclusive. From a user point of view, this is more or less equivalent (if R is not naturally exclusive, one can carry around an exclusive CMRA, which is more or less the same thing as carrying around locked). From an implementor's point of view, this might be a little simpler.

Marked this merge request as a Work In Progress