Use abstract predicates for the ticket lock refinement.

theories/examples/ticket_lock.v

@@ -64,45 +64,48 @@ Class lockPoolG Σ :=
 Section refinement.
   Context `{logrelG Σ, tlockG Σ, lockPoolG Σ}.
 
-  Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ :=
-    (∃ (o n : nat) (b : bool), lo ↦ᵢ #o ∗ ln ↦ᵢ #n
-   ∗ own γ (● GSet (seq_set 0 n)) ∗ l' ↦ₛ #b
-   ∗ if b then own γ (◯ GSet {[ o ]}) else True)%I.
+  (** * Basic abstractions around the concrete RA *)
 
-  Definition lockPoolInv (P : lockPool) : iProp Σ :=
-    ([∗ set] rs ∈ P, match rs with
-                     | ((lo, ln, γ), l') => lockInv lo ln γ l'
-                     end)%I.
+  (** ticket with the id `n` *)
+  Definition ticket (γ : gname) (n : nat) := own γ (◯ GSet {[ n ]}).
+  (** total number of issued tickets is `n` *)
+  Definition issuedTickets (γ : gname) (n : nat) := own γ (● GSet (seq_set 0 n)).
+  (** the locks `(ln, lo)` and `l'` are linked together in the pool `γP` *)
+  Definition inPool (γP : gname) (lo ln : loc) (γ : gname) (l' : loc) := own γP (◯ {[(lo, ln, γ), l']}).
+  (** the set `P` is in fact the lock pool associated with `γP` *)
+  Definition isPool (γP : gname) (P : lockPool) := own γP (● P).
 
-  Definition moduleInv γp : iProp Σ :=
-    (∃ (P : lockPool), own γp (● P) ∗ lockPoolInv P)%I.
-
-  Program Definition lockInt (γp : gname) := λne vv,
-    (∃ (lo ln : loc) (γ : gname) (l' : loc),
-        ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝
-      ∗ own γp (◯ {[(lo, ln, γ), l']}))%I.
-  Next Obligation. solve_proper. Qed.
+  Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
+  Proof.
+    iIntros "Ht1 Ht2".
+    iDestruct (own_valid_2 with "Ht1 Ht2") as %?%gset_disj_valid_op.
+    set_solver.
+  Qed.
 
-  Instance lockInt_persistent γp ww : Persistent (lockInt γp ww).
-  Proof. apply _. Qed.
+  Lemma newIssuedTickets : (|==> ∃ γ, issuedTickets γ 0)%I.
+  Proof. iMod (own_alloc (● (GSet ∅))) as (γ) "Hγ"; [done|eauto]. Qed.
 
-  Lemma lockPool_open_later (P : lockPool) (lo ln : loc) (γ : gname) (l' : loc) :
-    (lo, ln, γ, l') ∈ P →
-    ▷ lockPoolInv P -∗
-    (▷ lockInv lo ln γ l') ∗ ▷ (lockInv lo ln γ l' -∗ lockPoolInv P).
+  Lemma issueNewTicket γ m :
+    issuedTickets γ m ==∗
+    issuedTickets γ (S m) ∗ ticket γ m.
   Proof.
-    iIntros (Hrin) "Hreg".
-    rewrite /lockPoolInv.
-    iDestruct (big_sepS_elem_of_acc _ P _ with "Hreg") as "[Hrs Hreg]"; first apply Hrin.
+    iIntros "Hseq".
+    iMod (own_update with "Hseq") as "[Hseq Hticket]".
+    { eapply auth_update_alloc.
+      eapply (gset_disj_alloc_empty_local_update _ {[ m ]}).
+      apply (seq_set_S_disjoint 0). }
+    rewrite -(seq_set_S_union_L 0).
     by iFrame.
   Qed.
 
-  Lemma lockPool_lookup γp (P : lockPool) x :
-    own γp (● P) -∗
-    own γp (◯ {[ x ]}) -∗
-    ⌜x ∈ P⌝.
+  Instance inPool_persistent γP lo ln γ l' : Persistent (inPool γP lo ln γ l').
+  Proof. apply _. Qed.
+
+  Lemma inPool_lookup γP lo ln γ l' P :
+    inPool γP lo ln γ l' -∗ isPool γP P -∗
+    ⌜(lo, ln, γ, l') ∈ P⌝.
   Proof.
-    iIntros "Ho Hrs".
+    iIntros "Hrs Ho".
     iDestruct (own_valid_2 with "Ho Hrs") as %Hfoo.
     iPureIntro.
     apply auth_valid_discrete in Hfoo.
@@ -111,24 +114,120 @@ Section refinement.
     by rewrite gset_included elem_of_subseteq_singleton.
   Qed.
 
-  Lemma lockPool_excl (P : lockPool) (lo ln : loc) γ l' (v : val) :
-    lockPoolInv P -∗ lo ↦ᵢ v -∗ ⌜(lo, ln, γ, l') ∉ P⌝.
+  Lemma isPool_insert γP lo ln γ l' P :
+    isPool γP P ==∗
+    inPool γP lo ln γ l' ∗ isPool γP ({[(lo, ln, γ, l')]} ∪ P).
+  Proof.
+    iIntros "HP".
+    iMod (own_update with "HP") as "[HP Hls]".
+    { eapply auth_update_alloc.
+      eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} ∪ P)).
+      apply union_subseteq_r. }
+    iFrame "HP".
+    rewrite -gset_op_union.
+    by iDestruct "Hls" as "[#Hls _]".
+  Qed.
+
+  Lemma newIsPool (P : lockPool) : (|==> ∃ γP, isPool γP P)%I.
   Proof.
+    apply (own_alloc (● (P : lockPoolR))).
+    by apply auth_auth_valid.
+  Qed.
+
+  Instance isPool_timeless γP P : Timeless (isPool γP P).
+  Proof. apply _. Qed.
+  Instance inPool_timeless γP lo ln γ l' : Timeless (inPool γP lo ln γ l').
+  Proof. apply _. Qed.
+  Instance ticket_timeless γ n : Timeless (ticket γ n).
+  Proof. apply _. Qed.
+  Instance issuedTickets_timeless γ n : Timeless (issuedTickets γ n).
+  Proof. apply _. Qed.
+
+  Opaque ticket issuedTickets inPool isPool.
+
+  (** * Invariants and abstracts for them *)
+  Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ :=
+    (∃ (o n : nat) (b : bool), lo ↦ᵢ #o ∗ ln ↦ᵢ #n
+   ∗ issuedTickets γ n ∗ l' ↦ₛ #b
+   ∗ if b then ticket γ o else True)%I.
+
+  Instance ifticket_timeless (b : bool) γ o : Timeless (if b then ticket γ o else True%I).
+  Proof. destruct b; apply _. Qed.
+  Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l').
+  Proof. apply _. Qed.
+
+  Definition lockPoolInv (P : lockPool) : iProp Σ :=
+    ([∗ set] rs ∈ P, match rs with
+                     | ((lo, ln, γ), l') => lockInv lo ln γ l'
+                     end)%I.
+
+  Instance lockPoolInv_timeless P : Timeless (lockPoolInv P).
+  Proof.
+    apply big_sepS_timeless.
+    intros [[[? ?] ?] ?]. apply _.
+  Qed.
+
+  Lemma lockPoolInv_empty : lockPoolInv ∅.
+  Proof. by rewrite /lockPoolInv big_sepS_empty. Qed.
+
+  Lemma lockPool_open γP (P : lockPool) (lo ln : loc) (γ : gname) (l' : loc) :
+    isPool γP P -∗
+    inPool γP lo ln γ l' -∗
+    lockPoolInv P -∗
+    isPool γP P ∗ (lockInv lo ln γ l') ∗ (lockInv lo ln γ l' -∗ lockPoolInv P).
+  Proof.
+    iIntros "HP #Hin HPinv".
+    iDestruct (inPool_lookup with "Hin HP") as %Hin.
     rewrite /lockPoolInv.
-    iIntros "HP Hlo".
+    iDestruct (big_sepS_elem_of_acc _ P _ with "HPinv") as "[Hrs Hreg]"; first apply Hin.
+    by iFrame.
+  Qed.
+
+  Lemma lockPool_insert γP (P : lockPool) (lo ln : loc) γ l' :
+    isPool γP P -∗
+    lockPoolInv P -∗
+    lockInv lo ln γ l' ==∗
+    isPool γP ({[(lo, ln, γ, l')]} ∪ P)
+    ∗ lockPoolInv ({[(lo, ln, γ, l')]} ∪ P)
+    ∗ inPool γP lo ln γ l'.
+  Proof.
+    iIntros "HP HPinv".
+    iDestruct 1 as (n o b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    iMod (isPool_insert γP lo ln γ l' P with "HP") as "[$ $]".
+    rewrite /lockInv.
     iAssert (⌜(lo, ln, γ, l') ∈ P⌝ → False)%I as %Hbaz.
-    {
-      iIntros (HP).
+    { iIntros (HP).
+      rewrite /lockPoolInv.
       rewrite (big_sepS_elem_of _ P _ HP).
-      iDestruct "HP" as (a b c) "(Hlo' & Hln & ?)".
-      iDestruct (mapsto_valid_2 with "Hlo' Hlo") as %Hfoo;
-      compute in Hfoo; contradiction.
-    }
-    iPureIntro. eauto.
+      iDestruct "HPinv" as (? ? ?) "(Hlo' & Hln' & ?)".
+      iDestruct (mapsto_valid_2 with "Hlo' Hlo") as %Hfoo.
+      compute in Hfoo; contradiction. }
+    rewrite /lockPoolInv.
+    rewrite big_sepS_insert; last assumption.
+    iFrame. iExists _,_,_. by iFrame.
   Qed.
 
+  Opaque lockPoolInv.
+
+  Definition moduleInv γp : iProp Σ :=
+    (∃ (P : lockPool), isPool γp P ∗ lockPoolInv P)%I.
+
+  Program Definition lockInt (γp : gname) := λne vv,
+    (∃ (lo ln : loc) (γ : gname) (l' : loc),
+        ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝
+      ∗ inPool γp lo ln γ l')%I.
+  Next Obligation. solve_proper. Qed.
+
+  Instance lockInt_persistent γp ww : Persistent (lockInt γp ww).
+  Proof. apply _. Qed.
+
+  (** * Refinement proofs *)  
   Definition N := logrelN.@"locked".
 
+  Local Ltac openI N := iInv N as (P) ">[HP HPinv]" "Hcl".
+  Local Ltac closeI := iMod ("Hcl" with "[-]") as "_";
+    first by (iNext; iExists _; iFrame).
+
   (* Allocating a new lock *)
   Lemma newlock_refinement Δ Γ γp:
     inv N (moduleInv γp) -∗
@@ -139,72 +238,62 @@ Section refinement.
     iApply bin_log_related_arrow_val; eauto.
     { by unlock lock.newlock. }
     iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
+    (* Reducing to a value on the LHS *)
     rel_let_l.
     rel_alloc_l as lo "Hlo".
+    rel_alloc_l as ln "Hln".
+    (* Reducing to a value on the RHS *)
     rel_apply_r bin_log_related_newlock_r.
     { solve_ndisj. }
     iIntros (l') "Hl'".
-    rel_alloc_l_atomic.
-    iInv N as (P) "[>HP Hpool]" "Hcl".
-    iModIntro. iNext.
-    iIntros (ln) "Hln".
-    iMod (own_alloc (● (GSet ∅) ⋅ ◯ (GSet ∅))) as (γ) "[Hγ Hγ']".
-    { by rewrite -auth_both_op. }
-    iMod (own_update with "HP") as "[HP Hls]".
-    { eapply auth_update_alloc.
-      eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} ∪ P)).
-      apply union_subseteq_r. }
-    iDestruct (lockPool_excl _ lo ln γ l' with "Hpool Hlo") as %Hnew.
-    iMod ("Hcl" with "[-Hls]") as "_".
-    { iNext. iExists _; iFrame.
-      rewrite /lockPoolInv.
-      rewrite big_sepS_insert; last assumption.
-      iFrame. iExists _,_,_. iFrame. simpl. iFrame. }
-    rel_vals. iModIntro.
-    rewrite -gset_op_union.
-    iDestruct "Hls" as "[#Hls _]".
-    iAlways. iExists _,_,_,_. iFrame "Hls". eauto.
+    (* Establishing the invariant *)
+    openI N.
+    iMod newIssuedTickets as (γ) "Hγ".
+    iMod (lockPool_insert _ _ lo ln with "HP HPinv [Hlo Hln Hl' Hγ]") as "(HP & HPinv & #Hin)".
+    { iExists _,_,_; by iFrame. }
+    closeI.
+    rel_vals; iModIntro; iAlways.
+    iExists _,_,_,_. by iFrame "Hin".
   Qed.
 
   (* Acquiring a lock *)
+  (* helper lemma *)
   Lemma wait_loop_refinement Δ Γ γp (lo ln : loc) γ (l' : loc) (m : nat) :
     inv N (moduleInv γp) -∗
-    own γp (◯ {[(lo, ln), γ, l']}) -∗ (* two locks are linked *)
-    own γ (◯ GSet {[m]}) -∗ (* the ticket *)
+    inPool γp lo ln γ l' -∗ (* two locks are linked *)
+    ticket γ m -∗
     {(lockInt γp :: Δ); ⤉Γ} ⊨
       wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit.
   Proof.
-    iIntros "#Hinv #Hls Hticket".
-    unlock wait_loop.
+    iIntros "#Hinv #Hin Hticket".
     rel_rec_l.
     iLöb as "IH".
+    unlock {2}wait_loop. simpl.
     rel_let_l. rel_proj_l.
     rel_load_l_atomic.
-    iInv N as (P) "[>HP Hpool]" "Hcl".
-    iDestruct (lockPool_lookup with "HP Hls") as %Hls.
-    iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
+    openI N.
+    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
     rewrite {1}/lockInv.
-    iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
+    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hrest)".
     iModIntro. iExists _; iFrame; iNext.
     iIntros "Hlo".
     rel_op_l.
     case_decide; subst; rel_if_l.
     (* Whether the ticket is called out *)
     - destruct b.
-      { iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
-        set_solver. }
+      { iDestruct (ticket_nondup with "Hticket Hrest") as %[]. }
       rel_apply_r (bin_log_related_acquire_r with "Hl'").
       { solve_ndisj. }
       iIntros "Hl'".
-      iMod ("Hcl" with "[-]") as "_".
-      { iNext. iExists P; iFrame.
-        iApply "Hpool". iExists _,_,_; iFrame. }
+      iSpecialize ("HPinv" with "[Hlo Hln Hl' Hissued Hticket]").
+      { iExists _,_,_. by iFrame. }
+      closeI.
       iApply bin_log_related_unit.
     - iMod ("Hcl" with "[-Hticket]") as "_".
       { iNext. iExists P; iFrame.
-        iApply "Hpool". iExists _,_,_; by iFrame. }
+        iApply "HPinv". iExists _,_,_; by iFrame. }
       rel_rec_l.
-      by iApply "IH".
+      unlock wait_loop. simpl_subst/=. by iApply "IH".
   Qed.
 
   Lemma acquire_refinement Δ Γ γp :
@@ -216,34 +305,29 @@ Section refinement.
     iApply bin_log_related_arrow_val; eauto.
     { by unlock lock.acquire. }
     iAlways. iIntros (? ?) "/= #Hl".
-    iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
+    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
     rel_let_l. repeat rel_proj_l.
     (* rel_rec_l. (* TODO: cannot find the reduct *) *)
     rel_bind_l (FG_increment _ #()).
     rel_rec_l.
-    rel_apply_l (bin_log_FG_increment_logatomic _ (fun n => own γ (● GSet (seq_set 0 n)))%I True%I); first done.
+    rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done.
     iAlways.
-    iInv N as (P) "[>HP Hpool]" "Hcl".
-    iDestruct (lockPool_lookup with "HP Hls") as %Hls.
-    iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
+    openI N.
+    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
     rewrite {1}/lockInv.
-    iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & >Hseq & Hl' & Hrest)".
+    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
     iModIntro. iExists _; iFrame.
     iSplit.
     - iDestruct 1 as (m) "[Hln ?]".
       iApply ("Hcl" with "[-]").
       iNext. iExists P; iFrame.
-      iApply "Hpool". iExists _,_,_; by iFrame.
-    - iIntros (m) "[Hln Hseq] _".
-      iMod (own_update with "Hseq") as "[Hseq Hticket]".
-      { eapply auth_update_alloc.
-        eapply (gset_disj_alloc_empty_local_update _ {[ m ]}).
-        apply (seq_set_S_disjoint 0). }
-      rewrite -(seq_set_S_union_L 0).
-      iMod ("Hcl" with "[-Hticket]") as "_".
+      iApply "HPinv". iExists _,_,_; by iFrame.
+    - iIntros (m) "[Hln Hissued] _".
+      iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
+      iMod ("Hcl" with "[-Hm]") as "_".
       { iNext. iExists P; iFrame.
-        iApply "Hpool". iExists _,_,_; by iFrame. }
-      simpl. rel_let_l.
+        iApply "HPinv". iExists _,_,_; by iFrame. }
+      rel_let_l.
       by iApply wait_loop_refinement.
   Qed.
 
@@ -257,34 +341,33 @@ Section refinement.
     iApply bin_log_related_arrow_val; eauto.
     { by unlock lock.release. }
     iAlways. iIntros (? ?) "/= #Hl".
-    iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
+    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
     rel_let_l. repeat rel_proj_l.
     rel_load_l_atomic.
-    iInv N as (P) "[>HP Hpool]" "Hcl".
-    iDestruct (lockPool_lookup with "HP Hls") as %Hls.
-    iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
+    openI N.
+    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
     rewrite {1}/lockInv.
-    iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
-    iModIntro. iExists _; iFrame; iNext.
-    iIntros "Hlo".
+    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    iModIntro. iExists _; iFrame.
+    iNext. iIntros "Hlo".
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists P; iFrame.
-      iApply "Hpool". iExists _,_,_; iFrame. }
+      iApply "HPinv". iExists _,_,_; by iFrame. }
     rel_op_l.
-    rel_store_l_atomic. clear Hls n b P.
-    iInv N as (P) "[>HP Hpool]" "Hcl".
-    iDestruct (lockPool_lookup with "HP Hls") as %Hls.
-    iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
+    rel_store_l_atomic. clear n b P.
+    openI N.
+    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
     rewrite {1}/lockInv.
-    iDestruct "Hlk" as (o' n b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
-    iModIntro. iExists _; iFrame; iNext.
-    iIntros "Hlo".
+    iDestruct "Hls" as (o' n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    iModIntro. iExists _; iFrame.
+    iNext. iIntros "Hlo".
+
     rel_apply_r (bin_log_related_release_r with "Hl'").
     { solve_ndisj. }
     iIntros "Hl'".
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists P; iFrame.
-      iApply "Hpool". iExists _,_,_. by iFrame. }
+      iApply "HPinv". iExists _,_,_. by iFrame. }
     iApply bin_log_related_unit.
   Qed.
 
@@ -294,9 +377,9 @@ Section refinement.
         Pack (lock.newlock, lock.acquire, lock.release) : lockT.
   Proof.
     iIntros (Δ).
-    iMod (own_alloc (● (∅ : lockPoolR))) as (γp) "HP"; first done.
+    iMod (newIsPool ∅) as (γp) "HP".
     iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv".
-    { iNext. iExists ∅. iFrame. by rewrite /lockPoolInv big_sepS_empty. }
+    { iNext. iExists _; iFrame. iApply lockPoolInv_empty. }
     iApply (bin_log_related_pack _ (lockInt γp)).
     repeat iApply bin_log_related_pair.
     - by iApply newlock_refinement.