ticket_lock.v 6.62 KB
Newer Older
1 2 3 4
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Import auth.
From iris.proofmode Require Import invariants.
Zhen Zhang's avatar
Zhen Zhang committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset.
Import uPred.

Definition wait_loop: val :=
  rec: "wait_loop" "x" "l" :=
    let: "o" := Fst !"l" in
    if: "x" = "o"
      then #() (* my turn *)
      else "wait_loop" "x" "l".

Definition newlock : val := λ: <>, ref((* owner *) #0, (* next *) #0).
Definition acquire : val :=
  rec: "acquire" "l" :=
    let: "oldl" := !"l" in
    if: CAS "l" "oldl" (Fst "oldl", Snd "oldl" + #1)
      then wait_loop (Snd "oldl") "l"
      else "acquire" "l".

Definition release : val :=
  rec: "release" "l" :=
    let: "oldl" := !"l" in
    if: CAS "l" "oldl" (Fst "oldl" + #1, Snd "oldl")
      then #()
29
      else "release" "l".
Zhen Zhang's avatar
Zhen Zhang committed
30 31 32

Global Opaque newlock acquire release wait_loop.

33
(** The CMRAs we need. *)
Zhen Zhang's avatar
Zhen Zhang committed
34
Class tlockG Σ := TlockG {
35 36
   tlock_G :> authG Σ (gset_disjUR nat);
   tlock_exclG  :> inG Σ (exclR unitC)
Zhen Zhang's avatar
Zhen Zhang committed
37 38
}.

39 40
Definition tlockGF : gFunctorList :=
  [authGF (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
41
Instance inGF_tlockG `{H : inGFs Σ tlockGF} : tlockG Σ.
Zhen Zhang's avatar
Zhen Zhang committed
42 43 44 45 46
Proof. destruct H as (? & ? & ?). split. apply _. apply: inGF_inG. Qed.

Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace).

47
Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
48
  (gs = GSet (seq_set 0 n))%I.
Zhen Zhang's avatar
Zhen Zhang committed
49

50
Definition lock_inv (γ1 γ2: gname) (l : loc) (R : iProp Σ) : iProp Σ :=
51
  ( o n: nat, l  (#o, #n) 
Zhen Zhang's avatar
Zhen Zhang committed
52
               auth_inv γ1 (tickets_inv n) 
53
               ((own γ2 (Excl ())   R)  auth_own γ1 (GSet {[ o ]})))%I.
Zhen Zhang's avatar
Zhen Zhang committed
54

55
Definition is_lock (l: loc) (R: iProp Σ) : iProp Σ :=
Zhen Zhang's avatar
Zhen Zhang committed
56 57
  ( γ1 γ2, heapN  N  heap_ctx  inv N (lock_inv γ1 γ2 l R))%I.

58
Definition issued (l : loc) (x: nat) (R : iProp Σ) : iProp Σ :=
59 60
  ( γ1 γ2, heapN  N  heap_ctx  inv N (lock_inv γ1 γ2 l R) 
            auth_own γ1 (GSet {[ x ]}))%I.
Zhen Zhang's avatar
Zhen Zhang committed
61

62
Definition locked (l : loc) (R : iProp Σ) : iProp Σ :=
63 64
  ( γ1 γ2, heapN  N  heap_ctx  inv N (lock_inv γ1 γ2 l R) 
            own γ2 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
65 66 67 68 69 70 71 72 73 74 75

Global Instance lock_inv_ne n γ1 γ2 l : Proper (dist n ==> dist n) (lock_inv γ1 γ2 l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne n l: Proper (dist n ==> dist n) (is_lock l).
Proof. solve_proper. Qed.
Global Instance locked_ne n l: Proper (dist n ==> dist n) (locked l).
Proof. solve_proper. Qed.

Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.

76
Lemma newlock_spec (R : iProp Σ) Φ :
Zhen Zhang's avatar
Zhen Zhang committed
77 78 79 80 81
  heapN  N 
  heap_ctx  R  ( l, is_lock l R - Φ #l)  WP newlock #() {{ Φ }}.
Proof.
  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
  wp_seq. wp_alloc l as "Hl".
82 83 84
  iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
  iVs (own_alloc_strong (Auth (Excl' ) ) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
  iVs (inv_alloc N _ (lock_inv γ1 γ2 l R) with "[-HΦ]").
Zhen Zhang's avatar
Zhen Zhang committed
85 86 87 88 89 90
  { iNext. rewrite /lock_inv.
    iExists 0%nat, 0%nat.
    iFrame.
    iSplitL "Hγ1".
    { rewrite /auth_inv.
      iExists (GSet ).
91
      by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
92
    iLeft.
93
    by iFrame. }
94
  iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
95 96 97 98 99
  iApply "HΦ".
  iExists γ1, γ2.
  iSplit; by auto.
Qed.

100
Lemma wait_loop_spec l x R (Φ : val  iProp Σ) :
Zhen Zhang's avatar
Zhen Zhang committed
101 102 103
  issued l x R  ( l, locked l R - R - Φ #())  WP wait_loop #x #l {{ Φ }}.
Proof.
  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Ht)".
104
  iLöb as "IH". wp_rec. wp_let. wp_bind (! _)%E.
105 106 107 108 109 110 111 112
  iInv N as (o n) "[Hl Ha]" "Hclose".
  wp_load. destruct (decide (x = o)) as [->|Hneq].
  - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
    + iVs ("Hclose" with "[Hl Hainv Ht]").
      { iNext. iExists o, n. iFrame. eauto. }
      iVsIntro. wp_proj. wp_let. wp_op=>[_|[]] //.
      wp_if. iVsIntro.
      iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2; eauto.
Zhen Zhang's avatar
Zhen Zhang committed
113
    + iExFalso. iCombine "Ht" "Haown" as "Haown".
114
      iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
Zhen Zhang's avatar
Zhen Zhang committed
115
      set_solver.
116 117 118 119
  - iVs ("Hclose" with "[Hl Ha]").
    { iNext. iExists o, n. by iFrame. }
    iVsIntro. wp_proj. wp_let. wp_op=>?; first omega.
    wp_if. by iApply ("IH" with "Ht").
Zhen Zhang's avatar
Zhen Zhang committed
120 121
Qed.

122
Lemma acquire_spec l R (Φ : val  iProp Σ) :
Zhen Zhang's avatar
Zhen Zhang committed
123 124 125
  is_lock l R  ( l, locked l R - R - Φ #())  WP acquire #l {{ Φ }}.
Proof.
  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #?)".
126
  iLöb as "IH". wp_rec. wp_bind (! _)%E.
127 128 129 130
  iInv N as (o n) "[Hl Ha]" "Hclose".
  wp_load. iVs ("Hclose" with "[Hl Ha]").
  { iNext. iExists o, n. by iFrame. }
  iVsIntro. wp_let. wp_proj. wp_proj. wp_op.
131
  wp_bind (CAS _ _ _).
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
  iInv N as (o' n') "[Hl [Hainv Haown]]" "Hclose".
  destruct (decide ((#o', #n') = (#o, #n)))%V
    as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
  - wp_cas_suc.
    iDestruct "Hainv" as (s) "[Ho %]"; subst.
    iVs (own_update with "Ho") as "Ho".
    { eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
      rewrite elem_of_seq_set; omega. }
    iDestruct "Ho" as "[Hofull Hofrag]".
    iVs ("Hclose" with "[Hl Haown Hofull]").
    { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
      rewrite -(seq_set_S_union_L 0).
      iNext. iExists o, (S n)%nat.
      rewrite Nat2Z.inj_succ -Z.add_1_r.
      iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
    iVsIntro. wp_if. wp_proj.
    iApply wait_loop_spec.
    iSplitR "HΦ"; last by done.
    rewrite /issued /auth_own; eauto 10.
  - wp_cas_fail.
    iVs ("Hclose" with "[Hl Hainv Haown]").
    { iNext. iExists o', n'. by iFrame. }
    iVsIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
155 156
Qed.

157
Lemma release_spec R l (Φ : val  iProp Σ):
Zhen Zhang's avatar
Zhen Zhang committed
158 159 160
  locked l R  R  Φ #()  WP release #l {{ Φ }}.
Proof.
  iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Hγ)".
161
  iLöb as "IH". wp_rec. wp_bind (! _)%E.
162 163 164
  iInv N as (o n) "[Hl Hr]" "Hclose".
  wp_load. iVs ("Hclose" with "[Hl Hr]").
  { iNext. iExists o, n. by iFrame. }
165
  iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  wp_proj. wp_op. wp_proj.
  iInv N as (o' n') "[Hl Hr]" "Hclose".
  destruct (decide ((#o', #n') = (#o, #n)))%V
    as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
  - wp_cas_suc.
    iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
    + iExFalso. iCombine "Hγ" "Ho" as "Ho".
      iDestruct (own_valid with "#Ho") as %[].
    + iVs ("Hclose" with "[Hl HR Hγ Hainv]").
      { iNext. iExists (o + 1)%nat, n%nat.
        iFrame. rewrite Nat2Z.inj_add.
        iFrame. iLeft; by iFrame. }
      iVsIntro. by wp_if.
  - wp_cas_fail. iVs ("Hclose" with "[Hl Hr]").
    { iNext. iExists o', n'. by iFrame. }
    iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
Zhen Zhang's avatar
Zhen Zhang committed
182 183 184 185
Qed.
End proof.

Typeclasses Opaque is_lock issued locked.