Fractional spin lock.

_CoqProject

@@ -4,6 +4,7 @@ theories/utils/auth_excl.v
 theories/utils/encodable.v
 theories/utils/list.v
 theories/utils/compare.v
+theories/utils/spin_lock.v
 theories/channel/channel.v
 theories/channel/proto_model.v
 theories/channel/proto_channel.v

theories/utils/spin_lock.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import excl auth frac csum.
+From iris.base_logic.lib Require Import cancelable_invariants.
+From iris.bi.lib Require Import fractional.
+Set Default Proof Using "Type".
+
+Definition newlock : val := λ: <>, ref #false.
+Definition try_acquire : val := λ: "l", CAS "l" #false #true.
+Definition acquire : val :=
+  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
+Definition release : val := λ: "l", "l" <- #false.
+
+Class lockG Σ := LockG {
+  lock_tokG :> inG Σ (authR (optionUR (exclR fracR)));
+  lock_cinvG :> cinvG Σ;
+}.
+Definition lockΣ : gFunctors := #[GFunctor (authR (optionUR (exclR fracR))); cinvΣ].
+
+Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+
+  Definition lock_inv (γ γi : gname) (lk : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ b : bool, lk ↦ #b ∗
+                 if b then (∃ p, own γ (● (Excl' p)) ∗ cinv_own γi (p/2))
+                 else own γ (● None) ∗ R)%I.
+
+  Definition is_lock (lk : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv N γi (lock_inv γ γi lk R))%I.
+
+  Definition unlocked (lk : loc) (q : Qp) : iProp Σ :=
+    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv_own γi q)%I.
+
+  Definition locked (lk : loc) (q : Qp) : iProp Σ :=
+    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv_own γi (q/2) ∗ own γ (◯ (Excl' q)))%I.
+
+  Global Instance unlocked_fractional lk : Fractional (unlocked lk).
+  Proof.
+    intros q1 q2. iSplit.
+    - iDestruct 1 as (γ γi) "[#Hm [Hq Hq']]". iSplitL "Hq"; iExists γ, γi; by iSplit.
+    - iIntros "[Hq1 Hq2]". iDestruct "Hq1" as (γ γi) "[#Hm Hq1]".
+      iDestruct "Hq2" as (γ' γi') "[#Hm' Hq2]".
+      iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
+      iExists γ, γi; iSplit; first done. by iSplitL "Hq1".
+  Qed.
+  Global Instance unlocked_as_fractional γ :
+    AsFractional (unlocked γ p) (unlocked γ) p.
+  Proof. split. done. apply _. Qed.
+
+  Global Instance lock_inv_ne γ γi lk : NonExpansive (lock_inv γ γi lk).
+  Proof. solve_proper. Qed.
+  Global Instance is_lock_ne lk : NonExpansive (is_lock lk).
+  Proof. solve_proper. Qed.
+
+  Global Instance is_lock_persistent lk R : Persistent (is_lock lk R).
+  Proof. apply _. Qed.
+  Global Instance locked_timeless lk q : Timeless (locked lk q).
+  Proof. apply _. Qed.
+  Global Instance unlocked_timeless lk q : Timeless (unlocked lk q).
+  Proof. apply _. Qed.
+
+  Lemma newlock_spec (R : iProp Σ):
+    {{{ R }}}
+      newlock #()
+    {{{ lk, RET #lk; is_lock lk R ∗ unlocked lk 1 }}}.
+  Proof.
+    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
+    wp_lam. wp_apply (wp_alloc with "[//]"); iIntros (l) "[Hl Hm]".
+    iDestruct (meta_token_difference _ (↑N) with "Hm") as "[Hm1 Hm2]"; first done.
+    iMod (own_alloc (● None)) as (γ) "Hγ"; first by apply auth_auth_valid.
+    iMod (cinv_alloc_strong (λ _, True))
+      as (γi _) "[Hγi H]"; first by apply pred_infinite_True.
+    iMod (meta_set _ _ (γ,γi) with "Hm1") as "#Hm1"; first done.
+    iMod ("H" $! (lock_inv γ γi l R) with "[HR Hl Hγ]") as "#?".
+    { iIntros "!>". iExists false. by iFrame. }
+    iModIntro. iApply "HΦ". iSplit; iExists γ, γi; auto.
+  Qed.
+
+  Lemma try_acquire_spec lk R q :
+    {{{ is_lock lk R ∗ unlocked lk q }}}
+      try_acquire #lk
+    {{{ b, RET #b; if b is true then locked lk q ∗ R else unlocked lk q }}}.
+  Proof.
+    iIntros (Φ) "[#Hl Hq] HΦ". iDestruct "Hl" as (γ γi) "#[Hm Hinv]".
+    iDestruct "Hq" as (γ' γi') "[Hm' Hq]".
+    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
+    wp_rec. wp_bind (CmpXchg _ _ _).
+    iInv N as "[HR Hq]"; iDestruct "HR" as ([]) "[Hl HR]".
+    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl HR"; first (iExists true; iFrame).
+      wp_pures. iApply ("HΦ" $! false). iExists γ, γi; auto.
+    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]". iDestruct "Hq" as "[Hq Hq']".
+      iMod (own_update with "Hγ") as "[Hγ Hγ']".
+      { by apply auth_update_alloc, (alloc_option_local_update (Excl q)). }
+      iModIntro. iSplitL "Hl Hγ Hq"; first (iNext; iExists true; eauto with iFrame).
+      wp_pures. iApply ("HΦ" $! true with "[$HR Hγ' Hq']"). iExists γ, γi; by iFrame.
+  Qed.
+
+  Lemma acquire_spec lk R q :
+    {{{ is_lock lk R ∗ unlocked lk q }}} acquire #lk {{{ RET #(); locked lk q ∗ R }}}.
+  Proof.
+    iIntros (Φ) "[#Hlk Hq] HΦ". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "[$Hlk $Hq]"); iIntros ([]).
+    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "Hq". wp_if. iApply ("IH" with "[$]"); auto.
+  Qed.
+
+  Lemma release_spec lk R q :
+    {{{ is_lock lk R ∗ locked lk q ∗ R }}} release #lk {{{ RET #(); unlocked lk q }}}.
+  Proof.
+    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
+    iDestruct "Hlock" as (γ γi) "#[Hm Hinv]".
+    iDestruct "Hlocked" as (γ' γi') "(#Hm' & Hq & Hγ')".
+    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
+    wp_lam. iInv N as "[HR' Hq]"; iDestruct "HR'" as ([]) "[Hl HR']".
+    - iDestruct "HR'" as (p) ">[Hγ Hq']".
+      iDestruct (own_valid_2 with "Hγ Hγ'")
+        as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
+      iMod (own_update_2 with "Hγ Hγ'") as "Hγ".
+      { eapply auth_update_dealloc, delete_option_local_update; apply _. }
+      wp_store. iIntros "!>". iSplitL "Hl Hγ HR"; first (iExists false); iFrame.
+      iApply "HΦ". iExists γ, γi. iSplit; first done. by iSplitL "Hq".
+    - iDestruct "HR'" as "[>Hγ _]".
+      by iDestruct (own_valid_2 with "Hγ Hγ'")
+        as %[[[] ?%leibniz_equiv] _]%auth_both_valid.
+  Qed.
+End proof.
+
+Typeclasses Opaque is_lock locked.