Ticket lock refinement using HOCAP-style specs

_CoqProject

@@ -63,3 +63,4 @@ theories/experimental/helping/offers.v
 theories/experimental/helping/helping_stack.v
 
 theories/experimental/hocap/counter.v
+theories/experimental/hocap/ticket_lock.v

theories/examples/ticket_lock.v

@@ -4,7 +4,7 @@ From stdpp Require Import sets.
 From iris.algebra Require Export auth gset excl.
 From iris.base_logic Require Import auth.
 From reloc Require Import reloc lib.lock lib.counter.
-From iris.heap_lang.lib Require Import ticket_lock.
+From iris.heap_lang.lib Require Export ticket_lock.
 
 (* A different `acquire` funciton to showcase the atomic rule for FG_increment *)
 Definition acquire : val := λ: "lk",
@@ -13,6 +13,8 @@ Definition acquire : val := λ: "lk",
 (* A different `release` function to showcase the rule for wkincr *)
 Definition release : val := λ: "lk", wkincr (Fst "lk").
 
+Definition newlock : val := ticket_lock.newlock.
+
 Definition lrel_lock `{relocG Σ} : lrel Σ :=
   ∃ A, (() → A) * (A → ()) * (A → ()).
 

theories/experimental/hocap/counter.v

 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** HOCAP-style specifications for the concurrent counter *)
 From reloc Require Export reloc.
-From reloc.lib Require Export counter.
+From reloc.lib Require Export counter lock.
 From iris.algebra Require Export auth frac excl.
 From iris.bi.lib Require Export fractional.
 From iris.base_logic.lib Require Export auth.
 
-Definition wk_incr : val := λ: "c", "c" <- !"c" + #1.
-
 Class cnt_hocapG Σ := CntG {
     cnt_hocapG_inG :> authG Σ (optionUR (prodR fracR (agreeR natO)));
 }.
@@ -107,13 +105,62 @@ Section cnt_spec.
     iModIntro. iExists _; iFrame. iExists _; iSplit; eauto with iFrame.
   Qed.
 
-  Lemma wk_incr_l E c γ K e A q n :
+
+  Lemma wkincr_l_2 E c γ K e A :
+    E ## ↑ N →
+    Cnt c γ -∗
+    (∀ n, cnt_auth γ n ={⊤∖↑N}=∗ cnt_auth γ n ∗ ∀ m,
+       (cnt_auth γ m ={⊤∖↑N, ⊤∖↑N∖E}=∗
+          cnt_auth γ (n+1) ∗ REL fill K (of_val #()) << e @ (⊤∖E): A)) -∗
+    REL fill K (wkincr c) << e : A.
+  Proof.
+    iIntros (?).
+    iDestruct 1 as (l ->) "#Hcnt". iIntros "Hvs".
+    rel_rec_l. rel_load_l_atomic.
+    iInv N as (n1) ">[Hl Ha]" "Hcl". iModIntro.
+    iExists #n1. iFrame "Hl"; iIntros "!> Hl".
+    iMod ("Hvs" with "Ha") as "[Ha Hvs]".
+    iMod ("Hcl" with "[Hl Ha]") as "_".
+    { iNext. iExists _; by iFrame. }
+    rel_pures_l. rel_store_l_atomic.
+    iMod (inv_acc_strong with "Hcnt") as "[>Hcnt' Hcl]"; first by solve_ndisj.
+    iDestruct "Hcnt'" as (n2) "[Hl Ha]".
+    iModIntro. iExists _. iFrame "Hl". iIntros "!> Hl".
+    (* iDestruct (cnt_agree_2 with "Ha Hc") as %->. *)
+    iMod ("Hvs" with "Ha") as "(Ha & Href)".
+    iMod ("Hcl" with "[Ha Hl]") as "_".
+    { iNext. assert ((Z.of_nat n1 + 1)%Z = Z.of_nat (n1 + 1)) as -> by lia.
+      iExists _. by iFrame. }
+    assert (⊤ ∖ ↑N ∖ E = ⊤ ∖ E ∖ ↑N) as -> by set_solver.
+    rewrite -union_difference_L; last set_solver.
+    done.
+  Qed.
+
+  Lemma wkincr_l E c γ K e A q n :
+    E ## ↑ N →
+    Cnt c γ -∗
+    cnt γ q n -∗
+    (cnt_auth γ n ∗ cnt γ q n ={⊤∖↑N, ⊤∖↑N∖E}=∗
+     cnt_auth γ (n+1) ∗ REL fill K (of_val #()) << e @ (⊤∖E): A) -∗
+    REL fill K (wkincr c) << e : A.
+  Proof.
+    iIntros (?) "#Hcnt Hn Hvs".
+    iApply wkincr_l_2; try done.
+    iIntros (n1) "Ha".
+    iDestruct (cnt_agree_2 with "Ha Hn") as %->.
+    iModIntro. iFrame "Ha". iIntros (m) "Ha".
+    iDestruct (cnt_agree_2 with "Ha Hn") as %->.
+    iMod ("Hvs" with "[$Ha $Hn]") as "(Ha & Hvs)".
+    iModIntro. by iFrame.
+  Qed.
+
+  Lemma wkincr_l_alt E c γ K e A q n :
     E ## ↑ N →
     Cnt c γ -∗
     cnt γ q n -∗
     (cnt_auth γ n ∗ cnt γ q n ={⊤∖↑N, ⊤∖↑N∖E}=∗
-     cnt_auth γ (n+1) ∗ cnt γ q (n+1) ∗ REL fill K (of_val #()) << e @ (⊤∖E): A) -∗
-    REL fill K (wk_incr c) << e : A.
+     cnt_auth γ (n+1) ∗ REL fill K (of_val #()) << e @ (⊤∖E): A) -∗
+    REL fill K (wkincr c) << e : A.
   Proof.
     iIntros (?).
     iDestruct 1 as (l ->) "#Hcnt". iIntros "Hc Hvs".
@@ -128,7 +175,7 @@ Section cnt_spec.
     iDestruct "Hcnt'" as (m) "[Hl Ha]".
     iDestruct (cnt_agree_2 with "Ha Hc") as %->.
     iModIntro. iExists _. iFrame "Hl". iIntros "!> Hl".
-    iMod ("Hvs" with "[$Ha $Hc]") as "(Ha & Hc & Href)".
+    iMod ("Hvs" with "[$Ha $Hc]") as "(Ha & Href)".
     iMod ("Hcl" with "[Ha Hl]") as "_".
     { iNext. assert ((Z.of_nat n + 1)%Z = Z.of_nat (n + 1)) as -> by lia.
       iExists _. by iFrame. }
@@ -218,7 +265,7 @@ Section refinement.
 
   Lemma incr_refinement c γ lk l :
     Cnt N c γ -∗
-    inv N2 (∃ m, lock.is_locked_r lk false ∗ cnt γ 1 m ∗ l ↦ₛ #m)%I -∗
+    inv N2 (∃ m, is_locked_r lk false ∗ cnt γ 1 m ∗ l ↦ₛ #m)%I -∗
     REL FG_increment c << CG_increment #l lk : interp TNat [].
   Proof.
     iIntros "#HCnt #HI".
@@ -240,7 +287,7 @@ Section refinement.
 
   Lemma read_refinement c γ lk l :
     Cnt N c γ -∗
-    inv N2 (∃ m, lock.is_locked_r lk false ∗ cnt γ 1 m ∗ l ↦ₛ #m)%I -∗
+    inv N2 (∃ m, is_locked_r lk false ∗ cnt γ 1 m ∗ l ↦ₛ #m)%I -∗
     REL counter_read c << counter_read #l : interp TNat [].
   Proof.
     iIntros "#HCnt #HI".
@@ -264,7 +311,7 @@ Section refinement.
     iApply refines_arrow_val.
     iAlways. iIntros (? ?) "_"; simplify_eq/=.
     rel_rec_l. rel_rec_r.
-    rel_apply_r lock.refines_newlock_r; auto.
+    rel_apply_r refines_newlock_r; auto.
     iIntros (lk) "Hlk".
     repeat rel_pure_r.
     rel_alloc_r c' as "Hcnt'".
@@ -273,7 +320,7 @@ Section refinement.
     iMod (Cnt_alloc N _ 0%nat with "Hcnt") as (γ) "[#HCnt Hc]".
 
     (* establishing the invariant *)
-    iMod (inv_alloc N2 _ (∃ m, lock.is_locked_r lk false ∗ cnt γ 1 m ∗ c' ↦ₛ #m)%I
+    iMod (inv_alloc N2 _ (∃ m, is_locked_r lk false ∗ cnt γ 1 m ∗ c' ↦ₛ #m)%I
          with "[-]") as "#Hinv".
     { iNext. iExists 0%nat. by iFrame. }
     (* TODO: here we have to do /exactly/ 4 steps.

theories/experimental/hocap/ticket_lock.v

+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Ticket lock ≼ spin lock refinement using HOCAP-style specs for the counter *)
+From reloc Require Export reloc.
+From reloc.experimental Require Export hocap.counter.
+From reloc.lib Require Import lock.
+From reloc.examples Require Import ticket_lock.
+Module spin_lock := reloc.lib.lock.
+
+Section refinement.
+  Context `{!relocG Σ, !tlockG Σ, !cnt_hocapG Σ}.
+
+  (** * Invariants and abstracts for them *)
+  Definition lockInv (γlo γln : gname) (γ : gname) (l' : val) : iProp Σ :=
+    (∃ (o n : nat) (b : bool), cnt γlo 1 o ∗ cnt γln 1 n
+   ∗ issuedTickets γ n ∗ is_locked_r 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 N := nroot.@"locked".
+
+  Definition lockInt : lrel Σ := LRel (λ v1 v2,
+    (∃ (γln γlo : gname) (co cn : val) (γ : gname),
+        ⌜v1 = (co, cn)%V⌝
+      ∗ Cnt (N.@"cnt1") cn γln
+      ∗ Cnt (N.@"cnt2") co γlo
+      ∗ inv (N.@"lock") (lockInv γlo γln γ v2)))%I.
+
+  Local Instance lockInt_persistent w1 w2 : Persistent (lockInt w1 w2).
+  Proof. apply _. Qed.
+
+  Lemma wait_loop_refinement (co cn : val) (γlo γln γ : gname) (l' : val) (m : nat) :
+    inv (N.@"lock") (lockInv γlo γln γ l') -∗
+    Cnt (N.@"cnt1") cn γln -∗
+    Cnt (N.@"cnt2") co γlo -∗
+    ticket γ m -∗
+    REL wait_loop #m (co, cn)%V << spin_lock.acquire l' : ().
+  Proof.
+    iIntros "#Hinv #Hcntn #Hcnto Hticket".
+    iLöb as "IH". rel_rec_l.
+    rel_pures_l.
+    rel_apply_l (cnt_read_l _ (↑N.@"lock") with "Hcnto"); first by solve_ndisj.
+    iIntros (o) "Hlo".
+    iMod (inv_acc_strong with "Hinv") as "[HH Hcl]"; first solve_ndisj.
+    iDestruct "HH" as (o' n b) "(>Hlo' & >Hln & >Hissued & >[Hl' Hbticket])".
+    iDestruct (cnt_agree_2 with "Hlo Hlo'") as %<-.
+    iModIntro. iFrame. rel_pures_l.
+    case_decide; simplify_eq/=; rel_pures_l; last first.
+    (* Whether the ticket is called out *)
+    - iMod ("Hcl" with "[-Hticket]") as "_".
+      { iNext. iExists _,_,_; by iFrame. }
+      rewrite -union_difference_L; last done.
+      by iApply "IH".
+    - destruct b.
+      { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. }
+      rel_apply_r (refines_acquire_r with "Hl'").
+      iIntros "Hl'".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext; iExists _,_,_; iFrame. }
+      rewrite -union_difference_L; last done.
+      rel_values.
+  Qed.
+
+  Lemma acquire_refinement :
+    ⊢ REL acquire << spin_lock.acquire : (lockInt → ()).
+  Proof.
+    rel_arrow_val.
+    iIntros (? l') "/= #Hl".
+    iDestruct "Hl" as (γln γlo lo ln γ) "(-> & Hcntn & Hcnto & Hin)".
+    rel_rec_l. rel_pures_l.
+    rel_apply_l (cnt_increment_l _ ∅ with "Hcntn"); first by set_solver.
+    (* the viewshift *)
+    iIntros (n) "Hln".
+    iInv (N.@"lock") as (o n' b) "(Hlo & >Hln' & >Hissued & >Hb)" "Hcl".
+    iDestruct (cnt_agree_2 with "Hln Hln'") as %<-.
+    iMod (issueNewTicket with "Hissued") as "[Hissued Hticket]".
+    iMod (cnt_update (n+1) with "Hln Hln'") as "[Hln Hln']".
+    iMod ("Hcl" with "[Hissued Hlo Hln' Hb]") as "_".
+    { iNext. iExists _,_,_; iFrame. assert (n+1 = S n) as -> by lia. done. }
+    iFrame. rewrite !difference_empty_L. iModIntro.
+    rel_pures_l. by iApply wait_loop_refinement.
+  Qed.
+
+  Lemma release_refinement :
+    ⊢ REL release << spin_lock.release : (lockInt → ()).
+  Proof.
+    rel_arrow_val.
+    iIntros (? l') "/= #Hl".
+    iDestruct "Hl" as (γln γlo lo ln γ) "(-> & Hcntn & Hcnto & Hinv)".
+    rel_rec_l. rel_pures_l.
+    rel_apply_l (wkincr_l_2 _ (↑N.@"lock") with "Hcnto"); first solve_ndisj.
+    iIntros (n) "Hlo". iModIntro. iFrame. iIntros (m) "Hlo".
+    iMod (inv_acc_strong with "Hinv") as "[HH Hcl]"; first solve_ndisj.
+    iDestruct "HH" as (o' n2 b) "(>Hlo' & >Hln & >Hissued & >[Hl' Hbticket])".
+    iMod (cnt_update (n+1) with "Hlo Hlo'") as "[Hlo Hlo']".
+    iModIntro. iFrame.
+    rel_apply_r (refines_release_r with "Hl'"). iIntros "Hl'".
+    iMod ("Hcl" with "[-]") as "_".
+    { iNext. rewrite {2}/lockInv.
+      iExists _,_,_. by iFrame. }
+    rewrite -union_difference_L; last done.
+    by rel_values.
+  Qed.
+
+  Lemma newlock_refinement :
+    ⊢ REL newlock << spin_lock.newlock : (() → lockInt).
+  Proof.
+    rel_arrow_val.
+    iIntros (? ?) "[% %]"; subst.
+    rel_rec_l. rel_alloc_l lo as "Hlo".
+    rel_alloc_l ln as "Hln". rel_pures_l.
+    rel_apply_r refines_newlock_r. iIntros (l') "Hl'".
+    iMod (Cnt_alloc (N.@"cnt2") _ 0 with "Hln") as (γln) "[#Hc1 Hln]".
+    iMod (Cnt_alloc (N.@"cnt1") _ 0 with "Hlo") as (γlo) "[#Hc2 Hlo]".
+    iMod newIssuedTickets as (γ) "Hγ".
+    iMod (inv_alloc (N.@"lock") _ (lockInv γln γlo γ l') with "[-]") as "#Hinv".
+    { iNext. iExists 0%nat,0%nat,_. iFrame. }
+    rel_values. iModIntro. iExists _,_,_,_,_. iSplit; eauto with iFrame.
+  Qed.
+
+  Lemma ticket_lock_refinement Δ :
+    ⊢ REL (newlock, acquire, release)
+            <<
+           (spin_lock.newlock, spin_lock.acquire, spin_lock.release) : interp lockT Δ.
+  Proof.
+    iApply (refines_exists lockInt).
+    repeat iApply refines_pair; simpl.
+    - by iApply newlock_refinement.
+    - by iApply acquire_refinement.
+    - by iApply release_refinement.
+  Qed.
+
+End refinement.
+