ticket_lock.v 7.16 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
3
From iris.proofmode Require Import tactics.
Zhen Zhang's avatar
Zhen Zhang committed
4
From iris.heap_lang Require Import proofmode notation.
5
From iris.algebra Require Import auth gset.
6
From iris.heap_lang.lib Require Export lock.
Zhen Zhang's avatar
Zhen Zhang committed
7 8 9
Import uPred.

Definition wait_loop: val :=
10 11
  rec: "wait_loop" "x" "lk" :=
    let: "o" := !(Fst "lk") in
Zhen Zhang's avatar
Zhen Zhang committed
12 13
    if: "x" = "o"
      then #() (* my turn *)
14
      else "wait_loop" "x" "lk".
Zhen Zhang's avatar
Zhen Zhang committed
15 16

Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Zhen Zhang's avatar
Zhen Zhang committed
17 18

Definition acquire : val :=
19 20 21 22 23
  rec: "acquire" "lk" :=
    let: "n" := !(Snd "lk") in
    if: CAS (Snd "lk") "n" ("n" + #1)
      then wait_loop "n" "lk"
      else "acquire" "lk".
Zhen Zhang's avatar
Zhen Zhang committed
24

25 26
Definition release : val := λ: "lk",
  (Fst "lk") <- !(Fst "lk") + #1.
Zhen Zhang's avatar
Zhen Zhang committed
27 28 29

Global Opaque newlock acquire release wait_loop.

30
(** The CMRAs we need. *)
31 32
Class tlockG Σ :=
  tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
33
Definition tlockΣ : gFunctors :=
34
  #[ GFunctor (constRF (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat)))) ].
35

36
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ  tlockG Σ.
37
Proof. by intros ?%subG_inG. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
38 39

Section proof.
Zhen Zhang's avatar
Zhen Zhang committed
40
  Context `{!heapG Σ, !tlockG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
41

42 43 44 45 46
  Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
    ( o n : nat,
      lo  #o  ln  #n 
      own γ ( (Excl' o, GSet (seq_set 0 n))) 
      ((own γ ( (Excl' o, ))  R)  own γ ( (, GSet {[ o ]}))))%I.
Zhen Zhang's avatar
Zhen Zhang committed
47

48 49
  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
    ( lo ln : loc,
Zhen Zhang's avatar
Zhen Zhang committed
50
       heapN  N  heap_ctx 
51
       lk = (#lo, #ln)%V  inv N (lock_inv γ lo ln R))%I.
Zhen Zhang's avatar
Zhen Zhang committed
52

53 54
  Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
    ( lo ln: loc,
Zhen Zhang's avatar
Zhen Zhang committed
55
       heapN  N  heap_ctx 
56 57
       lk = (#lo, #ln)%V  inv N (lock_inv γ lo ln R) 
       own γ ( (, GSet {[ x ]})))%I.
Zhen Zhang's avatar
Zhen Zhang committed
58

59
  Definition locked (γ : gname) : iProp Σ := ( o, own γ ( (Excl' o, )))%I.
Zhen Zhang's avatar
Zhen Zhang committed
60

61 62
  Global Instance lock_inv_ne n γ lo ln :
    Proper (dist n ==> dist n) (lock_inv γ lo ln).
Zhen Zhang's avatar
Zhen Zhang committed
63
  Proof. solve_proper. Qed.
64
  Global Instance is_lock_ne γ n lk : Proper (dist n ==> dist n) (is_lock γ lk).
Zhen Zhang's avatar
Zhen Zhang committed
65
  Proof. solve_proper. Qed.
66
  Global Instance is_lock_persistent γ lk R : PersistentP (is_lock γ lk R).
Zhen Zhang's avatar
Zhen Zhang committed
67
  Proof. apply _. Qed.
68
  Global Instance locked_timeless γ : TimelessP (locked γ).
Zhen Zhang's avatar
Zhen Zhang committed
69 70
  Proof. apply _. Qed.

71 72 73 74 75
  Lemma locked_exclusive (γ : gname) : (locked γ  locked γ  False)%I.
  Proof.
    iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2".
    iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _].
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
76 77

  Lemma newlock_spec (R : iProp Σ) Φ :
78
    heapN  N 
79
    heap_ctx  R  ( lk γ, is_lock γ lk R - Φ lk)  WP newlock #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
80
  Proof.
81
    iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
Zhen Zhang's avatar
Zhen Zhang committed
82
    wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
83
    iMod (own_alloc ( (Excl' 0%nat, )   (Excl' 0%nat, ))) as (γ) "[Hγ Hγ']".
84
    { by rewrite -auth_both_op. }
85
    iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
86 87
    { iNext. rewrite /lock_inv.
      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
88
    iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
89 90
  Qed.

91 92
  Lemma wait_loop_spec γ lk x R (Φ : val  iProp Σ) :
    issued γ lk x R  (locked γ - R - Φ #())  WP wait_loop #x lk {{ Φ }}.
93 94 95
  Proof.
    iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
    iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
96
    iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
97 98
    wp_load. destruct (decide (x = o)) as [->|Hneq].
    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
99
      + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
100
        { iNext. iExists o, n. iFrame. eauto. }
101 102
        iModIntro. wp_let. wp_op=>[_|[]] //.
        wp_if. iModIntro.
103
        iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
104
      + iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
105
        set_solver.
106
    - iMod ("Hclose" with "[Hlo Hln Ha]").
107
      { iNext. iExists o, n. by iFrame. }
108
      iModIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
109 110 111
      wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
  Qed.

112 113
  Lemma acquire_spec γ lk R (Φ : val  iProp Σ) :
    is_lock γ lk R  (locked γ - R - Φ #())  WP acquire lk {{ Φ }}.
114 115 116 117
  Proof.
    iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
    iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
118
    wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
119
    { iNext. iExists o, n. by iFrame. }
120
    iModIntro. wp_let. wp_proj. wp_op.
121
    wp_bind (CAS _ _ _).
122
    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
123 124
    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
    - wp_cas_suc.
125
      iMod (own_update with "Hauth") as "[Hauth Hofull]".
126 127 128
      { eapply auth_update_alloc, prod_local_update_2.
        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
        apply (seq_set_S_disjoint 0). }
129
      rewrite -(seq_set_S_union_L 0).
130
      iMod ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
131 132
      { iNext. iExists o', (S n).
        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
133
      iModIntro. wp_if.
134 135
      iApply (wait_loop_spec γ (#lo, #ln)).
      iFrame "HΦ". rewrite /issued; eauto 10.
136
    - wp_cas_fail.
137
      iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
138
      { iNext. iExists o', n'. by iFrame. }
139
      iModIntro. wp_if. by iApply "IH".
140 141
  Qed.

142 143
  Lemma release_spec γ lk R (Φ : val  iProp Σ):
    is_lock γ lk R  locked γ  R  Φ #()  WP release lk {{ Φ }}.
144
  Proof.
145 146 147 148 149 150
    iIntros "(Hl & Hγ & HR & HΦ)".
    iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
    iDestruct "Hγ" as (o) "Hγo".
    rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
    wp_load.
151 152
    iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
153
    iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
154
    { iNext. iExists o, n. by iFrame. }
155
    iModIntro. wp_op.
156 157
    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
    wp_store.
158 159
    iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
160
    iDestruct "Haown" as "[[Hγo' _]|?]".
161
    { iDestruct (own_valid_2 with "[$Hγo $Hγo']") as %[[] ?]. }
162
    iMod (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
163 164
    { apply auth_update, prod_local_update_1.
      by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
165
    iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
166 167
    iNext. iExists (S o), n'.
    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
168
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
169 170 171
End proof.

Typeclasses Opaque is_lock issued locked.
Zhen Zhang's avatar
Zhen Zhang committed
172

173 174 175
Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.