Ticket lock refinement (almost) from the HOCAP-like counter specs

_CoqProject

@@ -45,6 +45,7 @@ theories/examples/generative.v
 theories/examples/Y.v
 theories/examples/FAI.v
 theories/examples/hospec/modular_counter.v
+theories/examples/hospec/ticket_lock_refinement.v
 theories/tests/typetest.v
 theories/tests/ghosttp.v
 theories/tests/tactics.v

theories/examples/counter.v

@@ -22,6 +22,9 @@ Definition FG_increment : val := rec: "inc" "v" :=
   then "c"
   else "inc" "v".
 
+Definition wkincr : val := λ: "l",
+  "l" <- !"l" + #1.
+
 Definition FG_counter : val := λ: <>,
   let: "x" := ref #0 in
   ((λ: <>, FG_increment "x"), counter_read "x").

theories/examples/hospec/modular_counter.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac agree.
 From iris.base_logic.lib Require Import invariants viewshifts.
 From iris_logrel Require Export logrel.
-From iris_logrel.examples Require Import counter.
+From iris_logrel.examples Require Export counter.
 
 Definition cntCmra : cmraT := (prodR fracR (agreeR natC)).
 
@@ -196,6 +196,60 @@ Section cnt_spec.
     by iApply bin_log_related_nat.
   Qed.
 
+  Theorem read_l (γ : gname) (E : coPset) (ℓ : loc) Δ Γ K t τ:
+    ↑(N .@ "internal") ## E →
+    Cnt ℓ γ -∗
+    (∀ (n : nat),
+       γ ⤇½ n ={⊤∖ ↑(N .@ "internal"), ⊤∖↑(N .@ "internal")∖E}=∗
+       γ ⤇½ n ∗ {⊤∖E;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ) -∗
+    {Δ;Γ} ⊨ fill K (! #ℓ) ≤log≤ t : τ.
+  Proof.
+    iIntros (?) "#Hcnt Hupd".
+    rel_load_l_atomic.
+    iMod (inv_open_strong with "Hcnt") as "[HH Hcl]"; first done.
+    iDestruct "HH" as (m') "[>Hl >Hown]".
+    iModIntro. iExists _; iFrame. iNext. iIntros "Hl".
+    iMod ("Hupd" with "Hown") as "[Hown Hlog]".
+    iMod ("Hcl" with "[Hl Hown]") as "_".
+    { iNext. iExists _. iFrame. }
+    assert (⊤ ∖ ↑N.@"internal" ∖ E
+            = ((⊤ ∖ E) ∖ ↑N.@"internal" : coPset)) as -> by set_solver.
+    rewrite -union_difference_L; last set_solver.
+    by iApply "Hlog".
+  Qed.
+
+  Theorem wkincr_l (γ : gname) (E : coPset) (ℓ : loc) (n : nat) (q : Qp) Δ Γ K t τ:
+    ↑(N .@"internal") ## E →
+    Cnt ℓ γ -∗
+    γ ⤇[q] n -∗
+    (γ ⤇½ n ∗ γ ⤇[q] n ={⊤∖ ↑(N .@ "internal"), ⊤∖↑(N .@ "internal")∖E}=∗ γ ⤇½ (n+1) ∗ γ ⤇[q] (n+1)) -∗
+    (γ ⤇[q] (n+1) -∗ {⊤∖E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ) -∗
+    {Δ;Γ} ⊨ fill K (wkincr #ℓ) ≤log≤ t : τ.
+  Proof.
+    iIntros (?) "#Hcnt Hγ Hupd H".
+    unlock wkincr. rel_rec_l.
+    rel_load_l_atomic.
+    iInv (N  .@ "internal") as (n') "[>Hl >Hown]" "Hcl".
+    iDestruct (makeElem_eq with "Hγ Hown") as %<-.
+    iModIntro. iExists _; iFrame. iNext. iIntros "Hl".
+    iMod ("Hcl" with "[Hl Hown]") as "_".
+    { iNext. iExists _. iFrame. }
+    rel_op_l.
+    rel_store_l_atomic.
+    iMod (inv_open_strong with "Hcnt") as "[HH Hcl]"; first solve_ndisj.
+    iDestruct "HH" as (m) "[>Hl >Hown]".
+    iDestruct (makeElem_eq with "Hγ Hown") as %<-.
+    iModIntro. iExists _; iFrame.
+    iNext. iIntros "Hl".
+    iMod ("Hupd" with "[$Hown $Hγ]") as "[Hown Hγ]".
+    assert (⊤ ∖ ↑N.@"internal" ∖ E
+            = ((⊤ ∖ E) ∖ ↑N.@"internal" : coPset)) as -> by set_solver.
+    iMod ("Hcl" with "[Hl Hown]") as "_".
+    { iNext. iExists _. iFrame. }
+    rewrite -union_difference_L; last set_solver.
+    by iApply "H".
+  Qed.
+
   (** Proving the refinement with the WP rule doesn't really work out that well: *)
   Theorem incr_spec (γ : gname) (P : iProp Σ) (Q : nat → iProp Σ) (ℓ : loc):
     □(∀ (n : nat), γ ⤇½ n ∗ P  ={⊤ ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗ Q n) ⊢

theories/examples/hospec/ticket_lock_refinement.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Export auth gset excl.
+From iris.base_logic Require Import auth.
+From iris_logrel Require Export logrel.
+From iris_logrel.examples Require Import lock ticket_lock hospec.modular_counter.
+
+(** Here we prove the ticket lock refinement using the modular specifications for the counter *)
+Section refinement.
+  Context `{logrelG Σ, tlockG Σ, cntG Σ}.
+
+  (** * Invariants and abstracts for them *)
+  Definition lockInv (γlo γln : gname) (γ : 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 N := nroot.@"locked".
+
+  Program Definition lockInt := λne vv,
+    (∃ (γln γlo : gname) (lo ln : loc) (γ : gname) (l' : loc),
+        ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝
+      ∗ Cnt (N.@"cnt1") ln γln
+      ∗ Cnt (N.@"cnt2") lo γlo
+      ∗ inv (N.@"lock") (lockInv γlo γln γ l'))%I.
+  Next Obligation. solve_proper. Qed.
+
+  Instance lockInt_persistent ww : Persistent (lockInt ww).
+  Proof. apply _. Qed.
+
+  Lemma wait_loop_refinement Δ Γ (lo ln : loc) (γlo γln γ : gname) (l' : loc) (m : nat) :
+    inv (N.@"lock") (lockInv γlo γln γ l') -∗
+    Cnt (N.@"cnt1") ln γln -∗
+    Cnt (N.@"cnt2") lo γlo -∗
+    ticket γ m -∗
+    {(lockInt :: Δ); ⤉Γ} ⊨
+      wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit.
+  Proof.
+    iIntros "#Hinv #Hcntn #Hcnto Hticket".
+    rel_rec_l.
+    iLöb as "IH".
+    unlock {2}wait_loop. simpl.
+    rel_let_l. rel_proj_l.
+    rel_apply_l (read_l _ _ _ _ (↑N.@"lock") with "Hcnto"); first solve_ndisj.
+    Unshelve. 2,3: solve_ndisj.
+    iIntros (o) "Hlo".
+    iMod (inv_open_strong with "Hinv") as "[HH Hcl]"; first solve_ndisj.
+    iDestruct "HH" as (o' n b) "(>Hlo' & >Hln & >Hissued & >[Hl' Hbticket])".
+    iDestruct (makeElem_eq with "Hlo Hlo'") as %<-.
+    iModIntro. iFrame.
+    rel_op_l.
+    case_decide; subst; rel_if_l.
+    (* Whether the ticket is called out *)
+    - destruct b.
+      { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. }
+      rel_apply_r (bin_log_related_acquire_r with "Hl'").
+      { solve_ndisj. }
+      iIntros "Hl'".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext; iExists _,_,_; iFrame. }
+      rewrite -union_difference_L; last done.
+      iApply bin_log_related_unit.
+    - iMod ("Hcl" with "[-Hticket]") as "_".
+      { iNext. iExists _,_,_; by iFrame. }
+      rel_rec_l.
+      unlock wait_loop. simpl_subst/=.
+      rewrite -union_difference_L; last done.
+      by iApply "IH".
+  Qed.
+
+  Lemma acquire_refinement_direct Δ Γ :
+    {(lockInt :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
+  Proof.
+    unlock acquire; simpl.
+    iApply bin_log_related_arrow_val; eauto.
+    { by unlock lock.acquire. }
+    iAlways. iIntros (? ?) "/= #Hl".
+    iDestruct "Hl" as (γln γlo lo ln γ l') "(% & % & Hcntn & Hcnto & Hin)".
+    simplify_eq/=.
+    rel_let_l. repeat rel_proj_l.
+    rel_apply_l
+      (FG_increment_l _ _ _ _ ∅
+         with "Hcntn"); eauto; try by (solve_ndisj||set_solver).
+    Unshelve. 2,3: solve_ndisj. (* TODO: this is annoying *)
+    (* the viewshift *)
+    iIntros (n) "Hln".
+    iInv (N.@"lock") as (o n' b) "(Hlo & >Hln' & >Hissued & >Hb)" "Hcl".
+    iDestruct (makeElem_eq with "Hln Hln'") as %<-.
+    iMod (issueNewTicket with "Hissued") as "[Hissued Hticket]".
+    iMod (makeElem_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 ->; try omega; done. }
+    iFrame. rewrite !difference_empty_L. iModIntro.
+    rel_let_l. by iApply wait_loop_refinement.
+  Qed.
+
+  (* TODO: cannot use the hocap rule
+     Here we run into a similar problem that we had when proving the release refinement against the abstract specification: what if we don't have access to `locked`? I.e. what if we call release without acquiring a lock first?
+     We cannot reasonably provide the γlo ⤇[q] - resource.
+ *)
+
+  Lemma logrel_mask_mono E1 E2 Δ Γ e e' τ :
+    E1 ⊆ E2 →
+    {E1;Δ;Γ} ⊨ e ≤log≤ e' : τ -∗
+    {E2;Δ;Γ} ⊨ e ≤log≤ e' : τ.
+  Proof.
+    iIntros (?) "Hlog".
+    rewrite bin_log_related_eq /bin_log_related_def.
+    iIntros (vvs ρ) "Hspec HΓ". rewrite /interp_expr.
+    iIntros (j K) "Hj".
+    iSpecialize ("Hlog" with "Hspec HΓ Hj").
+    assert (E2 = E1 ∪ (E2 ∖ E1)) as ->. rewrite -union_difference_L; eauto.
+    assert (⊤ = ⊤ ∪ (E2 ∖ E1)) as Ht. set_solver.
+    rewrite {4}Ht.
+    iApply fupd_mask_frame_r. set_solver.
+    iApply "Hlog".
+  Qed.
+
+  (* we prove an atomic relational triple, by breaking the abstraction
+     this is actually different from the lax atomic triple you would normally see
+     a standard version would say that the environment does not interfere with the value of lo, until a certain moment, e.g: the value of the counter is constant until the linearization point
+     this specification, otoh, says that the environment is resiliant to "incorrect"/non-atomic changes of the counter.
+*)
+  Lemma wkincr_l_atomic R1 R2 Δ Γ E K x γlo t τ  :
+    Cnt (N.@"cnt2") x γlo -∗
+    R2 -∗
+    □ (|={⊤ ∖ ↑N.@"cnt2".@"internal",E ∖ ↑N.@"cnt2".@"internal"}=>
+       ∃ o : nat, γlo ⤇½ o ∗ R1 o ∗
+       (γlo ⤇½ o ∗ R1 o ={E∖↑N.@"cnt2".@"internal",⊤∖↑N.@"cnt2".@"internal"}=∗ True) ∧
+       ((∃ o : nat, γlo ⤇½ (o+1)) ∗ R1 o -∗ R2 -∗
+            {E;Δ;Γ} ⊨ fill K Unit ≤log≤ t : τ))
+    -∗ ({Δ;Γ} ⊨ fill K (wkincr #x) ≤log≤ t : τ).
+  Proof.
+    iIntros "#Hcnt HR2 #H".
+    unlock wkincr.
+    rel_rec_l.
+    rel_apply_l (read_l _ _ _ _ ∅ with "Hcnt"); first set_solver.
+    Unshelve. 2,3: solve_ndisj.
+    iIntros (o) "Hγlo". rewrite !difference_empty_L.
+    iPoseProof "H" as "H2".
+    iMod "H" as (n) "[Hx [HR1 [Hrev _]]]".
+    iDestruct (makeElem_eq with "Hx Hγlo") as %->.
+    iFrame "Hx".
+    iMod ("Hrev" with "[$HR1 $Hγlo]") as "_"; simpl.
+    iModIntro. rel_op_l.
+    rel_store_l_atomic.
+    iMod (inv_open_strong with "Hcnt") as "[HH Hcl]"; first solve_ndisj.
+    iDestruct "HH" as (o') "[>Hl >Hown]".
+    iModIntro. iExists _; iFrame. iNext. iIntros "Hx".
+    iMod "H2" as (o'') "[Hγlo [HR1 [_ Hcomm]]]".
+    iDestruct (makeElem_eq with "Hγlo Hown") as %->.
+    iMod (makeElem_update _ _ _ (o+1) with "Hγlo Hown") as "[Hγlo Hown]". simpl.
+    iMod ("Hcl" with "[Hx Hγlo]") as "_".
+    { iNext. iExists _. iFrame. }
+    rewrite (union_comm_L _ (E∖_)) difference_union_L.
+    iApply (logrel_mask_mono E); first set_solver.
+    iApply ("Hcomm" with "[$HR1 Hown] HR2").
+    iExists _; by iFrame.
+  Qed.
+
+  Lemma release_refinement Δ Γ :
+    {(lockInt :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit).
+  Proof.
+    unlock release.
+    iApply bin_log_related_arrow_val; eauto.
+    { by unlock lock.release. }
+    iAlways. iIntros (? ?) "/= #Hl".
+    iDestruct "Hl" as (γln γlo lo ln γ l') "(% & % & Hcntn & Hcnto & Hinv)".
+    simplify_eq/=.
+    rel_let_l. rel_proj_l.
+    (* rel_apply_l *)
+    (*   (wkincr_l _ _ _ _ ∅ *)
+    (*      with "Hcnto []"); eauto; try by (solve_ndisj||set_solver). *)
+    pose (R := fun (o : nat) =>
+                 (∃ (n : nat) (b : bool), γln⤇½ n
+                 ∗ issuedTickets γ n ∗ l' ↦ₛ #b
+                 ∗ if b then ticket γ o else True)%I).
+    rel_apply_l (wkincr_l_atomic R True%I _ _ (⊤∖↑N.@"lock") with "Hcnto"); first done.
+    iAlways.
+    iMod (inv_open_strong with "Hinv") as "[HH Hcl]"; first solve_ndisj.
+    iDestruct "HH" as (o n b) "(>Hlo & >Hln & >Hissued & >Hb)".
+    (* iInv (N.@"lock") as (o n b) "(>Hlo & >Hln & >Hissued & >Hb)" "Hcl". *)
+    assert ((⊤∖↑N.@"cnt2".@"internal" ∖↑N.@"lock")
+           = (⊤∖↑N.@"lock"∖↑N.@"cnt2".@"internal")) as ->.
+    { set_solver. }
+    iModIntro. iExists o; iFrame.
+    rewrite {1}/R. iSplitR "Hcl".
+    { iExists _,_; by iFrame. }
+    iSplit.
+    - iIntros "[Hlo HR]".
+      unfold R. iDestruct "HR" as (n' b') "HR".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists _,_,_; by iFrame. }
+      assert (⊤ ∖ ↑N.@"lock" ∖ ↑N.@"cnt2".@"internal"
+                = ⊤ ∖ ↑N.@"cnt2".@"internal" ∖ ↑N.@"lock") as -> by set_solver.
+      rewrite -union_difference_L; last solve_ndisj.
+      done.
+    - iIntros "[Hlo HR] _".
+      iDestruct "Hlo" as (o') "Hlo".
+      unfold R. iDestruct "HR" as (n' b') "(Hln & Hissued & Hl' & Hticket)".
+      rel_apply_r (bin_log_related_release_r with "Hl'").
+      { (* wtf is this monstrosity ? *)
+        assert (nclose specN ⊆ ⊤ ∖ ↑N.@"lock") as HZ by solve_ndisj.
+        etransitivity. apply HZ.
+        set_solver. }
+      iIntros "Hl'".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists _,_,_. by iFrame. }
+      assert (⊤ = ↑N.@"lock" ∪ ⊤ ∖ ↑N.@"lock") as <-.
+      { rewrite (union_comm_L _ (⊤∖_)) difference_union_L. set_solver. }
+      iApply bin_log_related_unit.
+  Qed.
+
+  Lemma newlock_refinement Δ Γ:
+    {(lockInt:: Δ); ⤉Γ} ⊨ newlock ≤log≤ lock.newlock : (Unit → TVar 0).
+  Proof.
+    unlock newlock.
+    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".
+    iMod (Cnt_alloc with "Hlo") as (γlo) "[#Hcnto Hγlo]".
+    iMod (Cnt_alloc with "Hln") as (γln) "[#Hcntn Hγln]".
+    (* Reducing to a value on the RHS *)
+    rel_apply_r bin_log_related_newlock_r.
+    { solve_ndisj. }
+    iIntros (l') "Hl'".
+    (* Establishing the invariant *)
+    iMod newIssuedTickets as (γ) "Hγ".
+    iMod (inv_alloc (N.@"lock") _ (lockInv γlo γln γ l') with "[-]") as "#Hinv".
+    { iNext. iExists _,_,_. iFrame. }
+    rel_vals. iModIntro. iAlways.
+    iExists _,_,_,_,_,_. iFrame "Hinv Hcnto Hcntn". eauto.
+  Qed.
+
+  Lemma ticket_lock_refinement Γ :
+    Γ ⊨ Pack (newlock, acquire, release)
+      ≤log≤
+        Pack (lock.newlock, lock.acquire, lock.release) : lockT.
+  Proof.
+    iIntros (Δ).
+    iApply (bin_log_related_pack lockInt).
+    repeat iApply bin_log_related_pair.
+    - by iApply newlock_refinement.
+    - by iApply acquire_refinement_direct.
+    - by iApply release_refinement.
+  Qed.
+
+End refinement.

theories/examples/ticket_lock.v

@@ -16,8 +16,6 @@ Definition acquire : val := λ: "lk",
   let: "n" := FG_increment (Snd "lk") in
   wait_loop "n" "lk".
 
-Definition wkincr : val := λ: "l",
-  "l" <- !"l" + #1.
 Definition release : val := λ: "lk", wkincr (Fst "lk").
 
 Definition LockType : type := ref TNat × ref TNat.