Ticket lock using FAI atomic rule

theories/tests/relatomic.v

+From iris.proofmode Require Import tactics.
+From iris_logrel Require Import logrel.
+From iris.program_logic Require Import hoare.
+From iris.algebra Require Export auth gset excl.
+From iris.base_logic Require Import auth.
+From iris_logrel Require Import examples.lock.
+
+Definition read : val := λ: "x", !"x".
+
+Definition FAI : val := rec: "inc" "x" :=
+  let: "c" := !"x" in
+  if: CAS "x" "c" (#1 + "c")
+  then "c"
+  else "inc" "x".
+
+Definition makeCounter : val := λ: <>, ref #0.
+
+Definition FG_counter : val := λ: <>,
+  let: "x" := makeCounter in
+  (λ: <>, FAI "x", λ: <>, read "x").
+
+(* Definition makeLock : val := λ: <>, *)
+(*   let: "next" := makeCounter #() in *)
+(*   let: "owner" := makeCounter #() in *)
+(*   ref ("owner", "next"). *)
+(* Definition release : val := λ: "x", *)
+(*   FAI (Fst (!"x")). *)
+
+(* Definition wait_loop: val := *)
+(*   rec: "wait_loop" "x" "lk" := *)
+(*     if: "x" = !(Fst "lk") (* read the owner of the lock *) *)
+(*     then #()              (* it's my turn *) *)
+(*     else "wait_loop" "x" "lk". (* otherwise spin on dat *) *)
+
+(* Definition acquire : val := λ: "x", *)
+(*   let: "t" := FAI (Snd (!"x")) in *)
+(*   wait_loop "t" "x". *)
+
+Definition lockT : type :=
+  ∃: (Unit → TVar 0) × (TVar 0 → Unit) × (TVar 0 → Unit).
+Definition newlock : val :=
+  λ: <>, ((* owner *) ref #0, (* next *) ref #0).
+
+Definition wait_loop: val :=
+  rec: "wait_loop" "x" "lk" :=
+    if: "x" = !(Fst "lk")
+    then #() (* my turn *)
+    else "wait_loop" "x" "lk".
+Definition acquire : val :=
+  rec: "acquire" "lk" :=
+    let: "n" := FAI (Snd "lk") in
+    wait_loop "n" "lk".
+
+Definition release : val :=
+  λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
+
+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 contents.
+  Context `{logrelG Σ, tlockG Σ, lockPoolG Σ}.
+
+  Lemma FAI_atomic R1 R2 Γ E1 E2 K x t τ Δ :
+    R2 -∗
+    □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗
+       (x ↦ᵢ #n ∗ R1 n ={E2,E1}=∗ True) ∧
+        (x ↦ᵢ #(S n) ∗ R1 n -∗ R2 -∗
+            {E2,E1;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ))
+    -∗ ({E1;Δ;Γ} ⊨ fill K (FAI #x) ≤log≤ t : τ).
+  Proof.
+    iIntros "HR2 #H".
+    iLöb as "IH".
+    rewrite {2}/FAI. unlock; simpl.
+    rel_rec_l.
+    iPoseProof "H" as "H2". (* iMod later on destroys H *)
+    rel_load_l_atomic.
+    iMod "H" as (n) "[Hx [HR Hrev]]".
+    iModIntro. iRename "H2" into "H".
+    iExists #n. iFrame. iNext. iIntros "Hx".
+    iDestruct "Hrev" as "[Hrev _]".
+    iMod ("Hrev" with "[HR Hx]") as "_".
+    { by iFrame. }
+    rel_rec_l. rel_op_l.
+    rel_cas_l_atomic.
+    iMod "H" as (n') "[Hx [HR HQ]]". iModIntro.
+    iExists #n'. iFrame.
+    destruct (decide (n = n')); subst.
+    - iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
+      iIntros "_ !> Hx". simpl.
+      iDestruct "HQ" as "[_ HQ]".
+      iSpecialize ("HQ" with "[Hx HR]"). { iFrame. }
+      rel_if_l. by iApply "HQ".
+    - iSplitL; eauto; last first.
+      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
+      iIntros "_ !> Hx". simpl.
+      rel_if_l.
+      iDestruct "HQ" as "[HQ _]".
+      iMod ("HQ" with "[Hx HR]") as "_".
+      { by iFrame. }
+      unlock FAI.
+      by iApply "IH".
+  Qed.
+
+  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 : Persistent (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.
+
+  Definition N := logrelN.@"locked".
+
+  (* Allocating a new lock *)
+  Lemma newlock_refinement Δ Γ γp:
+    inv N (moduleInv γp) -∗
+    {(lockInt γp :: Δ); ⤉Γ} ⊨ newlock ≤log≤ lock.newlock : (Unit → TVar 0).
+  Proof.
+    iIntros "#Hinv".
+    unlock newlock.
+    iApply bin_log_related_arrow_val; eauto.
+    { by unlock lock.newlock. }
+    iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
+    rel_let_l.
+    rel_alloc_l as lo "Hlo".
+    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.
+  Qed.
+
+  (* Acquiring a lock *)
+  Lemma acquire_refinement Δ Γ γp :
+    inv N (moduleInv γp) -∗
+    {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
+  Proof.
+    iIntros "#Hinv".
+    unlock acquire; simpl.
+    iApply bin_log_related_arrow_val; eauto.
+    { by unlock lock.acquire. }
+    iAlways. iIntros (? ?) "/= #Hl".
+    iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
+    rel_let_l. repeat rel_proj_l.
+    (* rel_apply_l (FAI_atomic). *)
+    rel_bind_l (FAI #ln).
+    iApply (FAI_atomic (fun _ => True)%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.
+    rewrite {1}/lockInv.
+    iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & >Hseq & Hl' & Hrest)".
+    iModIntro. iExists _; iFrame.
+    iSplitR; first done.
+    iSplit.
+    - iIntros "[Hln ?]".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "Hpool". iExists _,_,_; iFrame. iFrame "Hrest". }
+      done.
+    - iIntros "[Hln ?] _".
+      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). }
+      rewrite -(seq_set_S_union_L 0).
+      iMod ("Hcl" with "[-Hticket]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "Hpool". iExists _,_,_; by iFrame. }
+      simpl. rel_let_l.
+      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".
+      rel_op_l.
+      case_decide; subst; rel_if_l.
+      (* The ticket is called out *)
+      + destruct b.
+        { iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
+          set_solver. }
+        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. }
+        iApply bin_log_related_unit.
+      + iMod ("Hcl" with "[-Hticket]") as "_".
+        { iNext. iExists P; iFrame.
+          iApply "Hpool". iExists _,_,_; by iFrame. }
+        rel_rec_l.
+        by iApply "IH".
+  Qed.
+
+  (* Releasing the lock *)
+  Lemma release_refinement Δ Γ γp :
+    inv N (moduleInv γp) -∗
+    {(lockInt γp :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit).
+  Proof.
+    iIntros "#Hinv".
+    unlock release.
+    iApply bin_log_related_arrow_val; eauto.
+    { by unlock lock.release. }
+    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_apply_r (bin_log_related_release_r with "Hl'").
+    { solve_ndisj. }
+    iIntros "Hl'".
+    iMod ("Hcl" with "[-]") as "_".
+    { iNext. iExists P; iFrame.
+      iApply "Hpool". iExists _,_,_; iFrame. }
+    iApply bin_log_related_unit.
+  Qed.
+
+  Lemma ticket_lock_refinement Γ :
+    Γ ⊨ Pack (newlock, acquire, release)
+      ≤log≤
+        Pack (lock.newlock, lock.acquire, lock.release) : lockT.
+  Proof.
+    iIntros (Δ).
+    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. }
+    iApply (bin_log_related_pack _ (lockInt γp)).
+    repeat iApply bin_log_related_pair.
+    - by iApply newlock_refinement.
+    - by iApply acquire_refinement.
+    - by iApply release_refinement.
+  Qed.
+
+End contents.