From 0e7e1e0770efef65f19112e1d16a6d9b6596e785 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 6 May 2020 16:12:12 +0200
Subject: [PATCH] Ticket lock refinement using HOCAP-style specs

---
 _CoqProject                               |   1 +
 theories/examples/ticket_lock.v           |   4 +-
 theories/experimental/hocap/counter.v     |  69 +++++++++--
 theories/experimental/hocap/ticket_lock.v | 137 ++++++++++++++++++++++
 4 files changed, 199 insertions(+), 12 deletions(-)
 create mode 100644 theories/experimental/hocap/ticket_lock.v

diff --git a/_CoqProject b/_CoqProject
index fffd12e..2a786e2 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 92515f0..c5a8257 100644
--- a/theories/examples/ticket_lock.v
+++ b/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 â†’ ()).
 
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 97404a8..37a1839 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -1,13 +1,11 @@
 (* 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.
diff --git a/theories/experimental/hocap/ticket_lock.v b/theories/experimental/hocap/ticket_lock.v
new file mode 100644
index 0000000..d0f2058
--- /dev/null
+++ b/theories/experimental/hocap/ticket_lock.v
@@ -0,0 +1,137 @@
+(* 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.
+
-- 
GitLab