Merge branch 'lock-iface' into 'master'

Add lock interface

@jung looks good?

See merge request !3

_CoqProject

@@ -97,6 +97,7 @@ heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v
 heap_lang/lib/lock.v
+heap_lang/lib/spin_lock.v
 heap_lang/lib/ticket_lock.v
 heap_lang/lib/counter.v
 heap_lang/lib/barrier/barrier.v

heap_lang/lib/lock.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl.
+(** Abstract Lock Interface **)
+
+From iris.heap_lang Require Import heap notation.
+
+Structure lock Σ `{!heapG Σ} :=
+  Lock {
+      (* -- operations -- *)
+      newlock : val;
+      acquire : val;
+      release : val;
+      (* -- predicates -- *)
+      (* name is used to associate locked with is_lock *)
+      name: Type;
+      is_lock (N: namespace) (γ: name) (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 γ);
+      locked_exclusive γ : locked γ ★ locked γ ⊢ False;
+      (* -- 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 Σ) :
+        is_lock N γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
+      release_spec N γ lk R (Φ : val → iProp Σ) :
+        is_lock N γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
+    }.
+
+Arguments newlock {_ _} _.
+Arguments acquire {_ _} _.
+Arguments release {_ _} _.
+Arguments is_lock {_ _} _ _ _ _ _.
+Arguments locked {_ _} _ _.
+
+Existing Instances is_lock_ne is_lock_persistent locked_timeless.
+
+Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N lk R:
+  Proper ((≡) ==> (≡)) (is_lock L N lk R) := ne_proper _.
 
-Definition newlock : val := λ: <>, ref #false.
-Definition acquire : val :=
-  rec: "acquire" "l" :=
-    if: CAS "l" #false #true then #() else "acquire" "l".
-Definition release : val := λ: "l", "l" <- #false.
-Global Opaque newlock acquire release.
-
-(** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
-
-Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
-
-Section proof.
-Context `{!heapG Σ, !lockG Σ} (N : namespace).
-
-Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
-  (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
-
-Definition is_lock (l : loc) (R : iProp Σ) : iProp Σ :=
-  (∃ γ, heapN ⊥ N ∧ heap_ctx ∧ inv N (lock_inv γ l R))%I.
-
-Definition locked (l : loc) (R : iProp Σ) : iProp Σ :=
-  (∃ γ, heapN ⊥ N ∧ heap_ctx ∧
-        inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I.
-
-Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
-Proof. solve_proper. Qed.
-Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock l).
-Proof. solve_proper. Qed.
-Global Instance locked_ne n l : Proper (dist n ==> dist n) (locked l).
-Proof. solve_proper. Qed.
-
-(** The main proofs. *)
-Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
-Proof. apply _. Qed.
-
-Lemma locked_is_lock l R : locked l R ⊢ is_lock l R.
-Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&?&_)"; eauto. Qed.
-
-Lemma newlock_spec (R : iProp Σ) Φ :
-  heapN ⊥ N →
-  heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
-Proof.
-  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
-  wp_seq. wp_alloc l as "Hl".
-  iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-  iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
-  { iIntros "!>". iExists false. by iFrame. }
-  iVsIntro. iApply "HΦ". iExists γ; eauto.
-Qed.
-
-Lemma acquire_spec l R (Φ : val → iProp Σ) :
-  is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}.
-Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "(%&#?&#?)".
-  iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
-  iInv N as ([]) "[Hl HR]" "Hclose".
-  - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-    iVsIntro. wp_if. by iApply "IH".
-  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
-    iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-    iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto.
-Qed.
-
-Lemma release_spec R l (Φ : val → iProp Σ) :
-  locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}.
-Proof.
-  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)".
-  rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
-  wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
-Qed.
-End proof.

heap_lang/lib/spin_lock.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import invariants tactics.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import excl.
+From iris.heap_lang.lib Require Import lock.
+
+Definition newlock : val := λ: <>, ref #false.
+Definition acquire : val :=
+  rec: "acquire" "l" :=
+    if: CAS "l" #false #true then #() else "acquire" "l".
+Definition release : val := λ: "l", "l" <- #false.
+Global Opaque newlock acquire release.
+
+(** The CMRA we need. *)
+(* Not bundling heapG, as it may be shared with other users. *)
+Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
+Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+
+Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+
+Section proof.
+Context `{!heapG Σ, !lockG Σ} (N : namespace).
+
+Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
+  (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
+
+Definition is_lock (γ: gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+  (∃ (l: loc), heapN ⊥ N ∧ heap_ctx ∧ lk = #l ∧ inv N (lock_inv γ l R))%I.
+
+Definition locked (γ: gname): iProp Σ := own γ (Excl ())%I.
+
+Lemma locked_exclusive (γ: gname): (locked γ ★ locked γ ⊢ False)%I.
+Proof.
+  iIntros "[Hl Hl']". iCombine "Hl" "Hl'" as "Hl". by iDestruct (own_valid with "Hl") as %[].
+Qed.
+
+Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
+Proof. solve_proper. Qed.
+Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
+Proof. solve_proper. Qed.
+(* Global Instance locked_ne n γ : Proper (dist n ==> dist n) (locked γ). *)
+(* Proof. solve_proper. Qed. *)
+
+(** The main proofs. *)
+Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+Proof. apply _. Qed.
+
+(* Lemma locked_is_lock lk R : locked lk R ⊢ is_lock lk R. *)
+(* Proof. rewrite /is_lock. iDestruct 1 as (γ l) "(?&?&?&?&_)". iExists γ, l. auto. Qed. *)
+
+Global Instance locked_timeless γ : TimelessP (locked γ).
+Proof. apply _. Qed.
+
+Lemma newlock_spec (R : iProp Σ) Φ :
+  heapN ⊥ N →
+  heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+Proof.
+  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
+  wp_seq. wp_alloc l as "Hl".
+  iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+  iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
+  { iIntros "!>". iExists false. by iFrame. }
+  iVsIntro. iApply "HΦ". iExists l. eauto.
+Qed.
+
+Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
+  is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
+Proof.
+  iIntros "[Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
+  iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
+  iInv N as ([]) "[Hl HR]" "Hclose".
+  - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+    iVsIntro. wp_if. by iApply "IH".
+  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
+    iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+    iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). by iFrame.
+Qed.
+
+Lemma release_spec γ lk R (Φ : val → iProp Σ) :
+  is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
+Proof.
+  iIntros "(Hlock & Hlocked & HR & HΦ)". iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
+  rewrite /release. wp_let. iInv N as (b) "[Hl _]" "Hclose".
+  wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+Qed.
+End proof.
+
+Definition spin_lock `{!heapG Σ, !lockG Σ} :=
+  Lock _ _ newlock acquire release gname is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.

heap_lang/lib/ticket_lock.v

@@ -4,6 +4,7 @@ From iris.program_logic Require Import auth.
 From iris.proofmode Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import gset.
+From iris.heap_lang.lib Require Import lock.
 Import uPred.
 
 Definition wait_loop: val :=
@@ -43,65 +44,70 @@ Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
 
 Section proof.
-Context `{!heapG Σ, !tlockG Σ} (N : namespace) (HN: heapN ⊥ N).
+  Context `{!heapG Σ, !tlockG Σ} (N : namespace).
 
-Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
-  (gs = GSet (seq_set 0 n))%I.
+  Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
+    (gs = GSet (seq_set 0 n))%I.
 
-Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
-  (∃ (o n: nat),
+  Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
+    (∃ (o n: nat),
        lo ↦ #o ★ ln ↦ #n ★
        auth_inv γ1 (tickets_inv n) ★
        ((own γ2 (Excl ()) ★  R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
 
-Definition is_lock (l: val) (R: iProp Σ) : iProp Σ :=
-  (∃ γ1 γ2 (lo ln: loc), heap_ctx ∧ l = (#lo, #ln)%V ∧ inv N (lock_inv γ1 γ2 lo ln R))%I.
-
-Definition issued (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
-  (∃ γ1 γ2 (lo ln: loc), heap_ctx ∧ l = (#lo, #ln)%V ∧ inv N (lock_inv γ1 γ2 lo ln R) ∧
-                         auth_own γ1 (GSet {[ x ]}))%I.
-
-Definition locked (l : val) (R : iProp Σ) : iProp Σ :=
-  (∃ γ1 γ2 (lo ln: loc), heap_ctx ∧ l = (#lo, #ln)%V ∧ inv N (lock_inv γ1 γ2 lo ln R) ∧
-                         own γ2 (Excl ()))%I.
-
-Global Instance lock_inv_ne n γ1 γ2 lo ln: Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
-Proof. solve_proper. Qed.
-Global Instance is_lock_ne n l: Proper (dist n ==> dist n) (is_lock l).
-Proof. solve_proper. Qed.
-Global Instance locked_ne n l: Proper (dist n ==> dist n) (locked l).
-Proof. solve_proper. Qed.
-
-Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
-Proof. apply _. Qed.
-
-Lemma newlock_spec (R : iProp Σ) Φ :
-  heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ l) ⊢ WP newlock #() {{ Φ }}.
+  Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
+    (∃ (lo ln: loc),
+       heapN ⊥ N ∧ heap_ctx ∧
+       l = (#lo, #ln)%V ∧ inv N (lock_inv (fst γs) (snd γs) lo ln R))%I.
+
+  Definition issued (γs: gname * gname) (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
+    (∃ (lo ln: loc),
+       heapN ⊥ N ∧ heap_ctx ∧
+       l = (#lo, #ln)%V ∧ inv N (lock_inv (fst γs) (snd γs) lo ln R) ∧
+       auth_own (fst γs) (GSet {[ x ]}))%I.
+
+  Definition locked (γs: gname * gname) : iProp Σ := own (snd γs) (Excl ())%I.
+
+  Global Instance lock_inv_ne n γ1 γ2 lo ln : Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
+  Proof. solve_proper. Qed.
+  Global Instance is_lock_ne γs n l : Proper (dist n ==> dist n) (is_lock γs l).
+  Proof. solve_proper. Qed.
+  Global Instance is_lock_persistent γs l R : PersistentP (is_lock γs l R).
+  Proof. apply _. Qed.
+  Global Instance locked_timeless γs : TimelessP (locked γs).
+  Proof. apply _. Qed.
+
+  Lemma locked_exclusive (γs: gname * gname) : (locked γs ★ locked γs ⊢ False)%I.
+  Proof.
+    iIntros "[Hl Hl']". iCombine "Hl" "Hl'" as "Hl". by iDestruct (own_valid with "Hl") as %[].
+  Qed.
+
+  Lemma newlock_spec (R : iProp Σ) Φ :
+    heapN ⊥ N → heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+  Proof.
+    iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock.
+    wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
+    iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
+    iVs (own_alloc_strong (Auth (Excl' ∅) ∅) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
+    iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
+    - iNext. rewrite /lock_inv.
+      iExists 0%nat, 0%nat.
+      iFrame.
+      iSplitL "Hγ1".
+      + rewrite /auth_inv.
+        iExists (GSet ∅).
+        by iFrame.
+      + iLeft. by iFrame.
+    - iVsIntro.
+      iSpecialize ("HΦ" $! (#lo, #ln)%V (γ1, γ2)). iApply "HΦ".
+      iExists lo, ln.
+      iSplit; by eauto.
+  Qed.
+
+Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
+  issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
 Proof.
-  iIntros "(#Hh & HR & HΦ)". rewrite /newlock /=.
-  wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
-  iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
-  iVs (own_alloc_strong (Auth (Excl' ∅) ∅) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
-  iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
-  { iNext. rewrite /lock_inv.
-    iExists 0%nat, 0%nat.
-    iFrame.
-    iSplitL "Hγ1".
-    { rewrite /auth_inv.
-      iExists (GSet ∅).
-      by iFrame. }
-    iLeft.
-    by iFrame. }
-  iVsIntro.
-  iApply "HΦ".
-  iExists γ1, γ2, lo, ln.
-  iSplit; by auto.
-Qed.
-
-Lemma wait_loop_spec l x R (Φ : val → iProp Σ) :
-  issued l x R ★ (∀ l, locked l R -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
-Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Ht)".
+  iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
   iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
   iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
   wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -110,7 +116,7 @@ Proof.
       { iNext. iExists o, n. iFrame. eauto. }
       iVsIntro. wp_let. wp_op=>[_|[]] //.
       wp_if. iVsIntro.
-      iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2, lo, ln; eauto.
+      iApply ("HΦ" with "[-HR] HR"). eauto.
     + iExFalso. iCombine "Ht" "Haown" as "Haown".
       iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
       set_solver.
@@ -120,10 +126,10 @@ Proof.
     wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
 Qed.
 
-Lemma acquire_spec l R (Φ : val → iProp Σ) :
-  is_lock l R ★ (∀ l, locked l R -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
+Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
+  is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
 Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #?)".
+  iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
   iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
   wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
@@ -145,8 +151,8 @@ Proof.
       rewrite Nat2Z.inj_succ -Z.add_1_r.
       iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
     iVsIntro. wp_if.
-    iApply (wait_loop_spec (#lo, #ln)).
-    iSplitR "HΦ"; last by done.
+    iApply (wait_loop_spec γs (#lo, #ln)).
+    iSplitR "HΦ"; last by auto.
     rewrite /issued /auth_own; eauto 10.
   - wp_cas_fail.
     iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
@@ -154,10 +160,10 @@ Proof.
     iVsIntro. wp_if. by iApply "IH".
 Qed.
 
-Lemma release_spec R l (Φ : val → iProp Σ):
-  locked l R ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
+Lemma release_spec γs l R (Φ : val → iProp Σ):
+  is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
 Proof.
-  iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Hγ)".
+  iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
   iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
   iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
   wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
@@ -182,3 +188,6 @@ Qed.
 End proof.
 
 Typeclasses Opaque is_lock issued locked.
+
+Definition ticket_lock `{!heapG Σ, !tlockG Σ} :=
+  Lock _ _ newlock acquire release (gname * gname) is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.