Ticket lock refines spin lock

_CoqProject

@@ -26,6 +26,7 @@ theories/logrel/contextual_refinement.v
 theories/logrel/soundness_binary.v
 theories/logrel.v
 theories/examples/lock.v
+theories/examples/ticket_lock.v
 theories/examples/counter.v
 theories/examples/lateearlychoice.v
 theories/examples/par.v

theories/examples/ticket_lock.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth gset excl.
+From iris.base_logic Require Import auth.
+From iris_logrel Require Export logrel examples.lock.
+
+Definition wait_loop: val :=
+  rec: "wait_loop" "x" "lk" :=
+    if: "x" = !(Fst "lk")
+      then #() (* my turn *)
+      else "wait_loop" "x" "lk".
+
+Definition newlock : val :=
+  λ: <>, ((* owner *) ref #0, (* next *) ref #0).
+
+Definition acquire : val :=
+  rec: "acquire" "lk" :=
+    let: "n" := !(Snd "lk") in
+    if: CAS (Snd "lk") "n" ("n" + #1)
+      then wait_loop "n" "lk"
+      else "acquire" "lk".
+
+Definition release : val :=
+  λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
+
+Definition LockType := TProd (Tref TNat) (Tref TNat).
+
+Hint Unfold LockType : typeable.
+
+Lemma newlock_type Γ : typed Γ newlock (TArrow TUnit LockType).
+Proof. solve_typed. Qed.
+
+Hint Resolve newlock_type : typeable.
+
+Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
+Proof. unlock acquire wait_loop. solve_typed. Qed.
+
+Hint Resolve acquire_type : typeable.
+
+Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
+Proof. solve_typed. Qed.
+
+Hint Resolve release_type : typeable.
+
+Definition lockτ := TExists (TProd (TProd (TArrow TUnit (TVar 0))
+                                          (TArrow (TVar 0) TUnit))
+                                          (TArrow (TVar 0) TUnit)).
+Lemma ticket_lock_typed Γ : typed Γ (Pack (newlock, acquire, release)) lockτ.
+Proof.
+  apply TPack with LockType.
+  asimpl. solve_typed.
+Qed.
+
+Class tlockG Σ :=
+  tlock_G :> authG Σ (gset_disjUR nat).
+Definition tlockΣ : gFunctors :=
+  #[ authΣ (gset_disjUR nat) ].
+
+Definition lockPool := gset ((loc * loc * gname) * loc).
+Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).
+
+Class lockPoolG Σ :=
+  lockPool_inG :> authG Σ lockPoolR.
+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.
+
+  Definition lockPoolInv (P : lockPool) : iProp Σ :=
+    ([∗ set] rs ∈ P, match rs with
+                     | ((lo, ln, γ), l') => lockInv lo ln γ l'
+                     end)%I.
+
+  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.
+
+  Instance lockInt_persistent γp ww : PersistentP (lockInt γp ww).
+  Proof. apply _. 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).
+  Proof.
+    iIntros (Hrin) "Hreg".
+    rewrite /lockPoolInv.
+    iDestruct (big_sepS_elem_of_acc _ P _ with "Hreg") as "[Hrs Hreg]"; first apply Hrin.
+    by iFrame.
+  Qed.
+
+  Lemma lockPool_lookup γp (P : lockPool) x :
+    own γp (● P) -∗
+    own γp (◯ {[ x ]}) -∗
+    ⌜x ∈ P⌝.
+  Proof.
+    iIntros "Ho Hrs".
+    iDestruct (own_valid_2 with "Ho Hrs") as %Hfoo.
+    iPureIntro.
+    apply auth_valid_discrete in Hfoo.
+    simpl in Hfoo. destruct Hfoo as [Hfoo _].
+    revert Hfoo. rewrite left_id.
+    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⌝.
+  Proof.
+    rewrite /lockPoolInv.
+    iIntros "HP Hlo".
+    iAssert (⌜(lo, ln, γ, l') ∈ P⌝ → False)%I as %Hbaz.
+    {
+      iIntros (HP).
+      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.
+  Qed.
+
+  Lemma ticket_lock_refinement Γ :
+    Γ ⊨ Pack (newlock, acquire, release)
+      ≤log≤
+        Pack (lock.newlock, lock.acquire, lock.release) : lockτ.
+  Proof.
+    iIntros (Δ).
+    pose (N:=logrelN.@"locked").
+    iApply fupd_logrel'.
+    iMod (own_alloc (● (∅ : lockPoolR))) as (γp) "HP"; first done.
+    iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv".
+    { iNext. iExists ∅. iFrame. by rewrite /lockPoolInv big_sepS_empty. }
+    iModIntro.
+    iApply (bin_log_related_pack _ (lockInt γp)).
+    repeat iApply bin_log_related_pair.
+    - (* Allocating a new lock *)
+      unlock newlock lock.newlock.
+      iApply bin_log_related_arrow_val; eauto.
+      iAlways. iIntros (? ?) "/= [% %]". simplify_eq.
+      rel_let_l. rel_let_r.
+      rel_alloc_r as l' "Hl'".
+      rel_alloc_l as lo "Hlo".
+      rel_alloc_l_atomic.
+      iInv N as (P) "[>HP Hpool]" "Hcl".
+      iModIntro. iNext.
+      iIntros (ln) "Hln".
+      iApply fupd_logrel'.
+      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. }
+      iModIntro.
+      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.
+    - (* Acquire *)
+      unlock acquire.
+      iApply bin_log_related_arrow_val; eauto.
+      { by unlock lock.acquire. }
+      iAlways. iIntros (? ?) "/= #Hl".
+      iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
+      iLöb as "IH".
+      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.
+      rewrite {1}/lockInv.
+      iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
+      iModIntro. iExists _; iFrame; iNext.
+      iIntros "Hln".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "Hpool". iExists _,_,_; iFrame. }
+      rel_let_l. rel_proj_l. rel_op_l.
+      clear Hls o b P.
+      rel_cas_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.
+      rewrite {1}/lockInv.
+      iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
+      iModIntro. iExists _; iFrame.
+      iSplit; iIntros (?); iNext; iIntros "Hln"; rel_if_l.
+      + iMod ("Hcl" with "[-]") as "_".
+        { iNext. iExists P; iFrame.
+          iApply "Hpool". iExists _,_,_; by iFrame. }
+        iApply "IH".
+      + simplify_eq.
+        iApply fupd_logrel'.
+        iMod (own_update with "Hseq") as "[Hseq Hticket]".
+        { eapply auth_update_alloc.
+          eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
+          apply (seq_set_S_disjoint 0). }
+        iModIntro.
+        rewrite -(seq_set_S_union_L 0).
+        rewrite Nat.add_1_r.
+        iMod ("Hcl" with "[-Hticket]") as "_".
+        { iNext. iExists P; iFrame.
+          iApply "Hpool". iExists _,_,_; by iFrame. }
+        iClear "IH".
+        unlock wait_loop.
+        rel_rec_l.
+        iLöb as "IH".
+        rel_let_l. rel_proj_l.
+        rel_load_l_atomic. clear Hls P o b.
+        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.
+        rewrite {1}/lockInv.
+        iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
+        iModIntro. iExists _; iFrame; iNext.
+        iIntros "Hlo".
+        destruct (decide (n = o)); simplify_eq; rel_op_l.
+        (* The ticket is called out *)
+        * replace (if PeanoNat.Nat.eq_dec o o then LitV true else LitV false) with #true; last first.
+          { (* TODO :( *) case_match; congruence. }
+          rel_if_l.
+          unlock lock.acquire.
+          rel_rec_r.
+          destruct b.
+          { iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
+            set_solver. }
+          rel_cas_suc_r. rel_if_r.
+          iMod ("Hcl" with "[-]") as "_".
+          { iNext. iExists P; iFrame.
+            iApply "Hpool". iExists _,_,_; by iFrame. }
+          iApply bin_log_related_unit.
+
+        * replace (if PeanoNat.Nat.eq_dec n o then LitV true else LitV false) with #false; last first.
+          { (* TODO :( *) case_match; congruence. }
+          rel_if_l.
+          iMod ("Hcl" with "[-Hticket]") as "_".
+          { iNext. iExists P; iFrame.
+            iApply "Hpool". iExists _,_,_; by iFrame. }
+          rel_rec_l.
+          by iApply "IH".
+    - (* Release *)
+      unlock release lock.release.
+      iApply bin_log_related_arrow_val; eauto.
+      iAlways. iIntros (? ?) "/= #Hl".
+      iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". 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.
+      rewrite {1}/lockInv.
+      iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
+      iModIntro. iExists _; iFrame; iNext.
+      iIntros "Hlo".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "Hpool". iExists _,_,_; 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.
+      rewrite {1}/lockInv.
+      iDestruct "Hlk" as (o' n b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
+      iModIntro. iExists _; iFrame; iNext.
+      iIntros "Hlo".
+      rel_let_r. rel_store_r.
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "Hpool". iExists _,_,_; iFrame. }
+      iApply bin_log_related_unit.
+  Qed.
+End refinement.