ticket_lock.v 7.11 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 excl auth gset.
6
From iris.heap_lang.lib Require Export lock.
7
Set Default Proof Using "Type".
Zhen Zhang's avatar
Zhen Zhang committed
8 9 10
Import uPred.

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

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

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

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

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 (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
35

36
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ  tlockG Σ.
37
Proof. solve_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
  Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
    ( o n : nat,
44
      lo  #o  ln  #n 
Robbert Krebbers's avatar
Robbert Krebbers committed
45
      own γ ( (Excl' o, GSet (set_seq 0 n))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
46
      ((own γ ( (Excl' o, GSet ))  R)  own γ ( (ε, GSet {[ o ]}))))%I.
Zhen Zhang's avatar
Zhen Zhang committed
47

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

Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54
  Definition issued (lk : val) (x : nat) : iProp Σ :=
    ( γ (lo ln : loc),
       lk = (#lo, #ln)%V  meta lo nroot γ  own γ ( (ε, GSet {[ x ]})))%I.
Zhen Zhang's avatar
Zhen Zhang committed
55

Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58
  Definition locked (lk : val) : iProp Σ :=
    ( γ (lo ln : loc) o,
       lk = (#lo, #ln)%V  meta lo nroot γ  own γ ( (Excl' o, GSet )))%I.
Zhen Zhang's avatar
Zhen Zhang committed
59

60 61
  Global Instance lock_inv_ne γ lo ln :
    NonExpansive (lock_inv γ lo ln).
Zhen Zhang's avatar
Zhen Zhang committed
62
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Global Instance is_lock_ne lk : NonExpansive (is_lock lk).
Zhen Zhang's avatar
Zhen Zhang committed
64
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  Global Instance is_lock_persistent lk R : Persistent (is_lock lk R).
Zhen Zhang's avatar
Zhen Zhang committed
66
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  Global Instance locked_timeless lk : Timeless (locked lk).
Zhen Zhang's avatar
Zhen Zhang committed
68 69
  Proof. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
70
  Lemma locked_exclusive lk : locked lk - locked lk - False.
71
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74
    iDestruct 1 as (γ1 lo1 ln1 o1 ?) "[#Hm1 H1]".
    iDestruct 1 as (γ2 lo2 ln2 o2 ?) "[#Hm2 H2]"; simplify_eq/=.
    iDestruct (meta_agree with "Hm1 Hm2") as %<-.
75
    iDestruct (own_valid_2 with "H1 H2") as %[[] _].
76
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
77

78
  Lemma newlock_spec (R : iProp Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    {{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}.
Zhen Zhang's avatar
Zhen Zhang committed
80
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
81
    iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
    wp_alloc ln as "Hln". wp_apply (wp_alloc with "[//]"); iIntros (lo) "[Hlo Hm]".
Robbert Krebbers's avatar
Robbert Krebbers committed
83
    iMod (own_alloc ( (Excl' 0%nat, GSet )   (Excl' 0%nat, GSet ))) as (γ) "[Hγ Hγ']".
84
    { by apply auth_both_valid. }
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    iMod (meta_set _ _ γ nroot with "Hm") as "#Hm"; first done.
86
    iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
87 88
    { iNext. rewrite /lock_inv.
      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
89
    wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V). iExists γ, lo, ln. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
90 91
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
  Lemma wait_loop_spec lk x R :
    {{{ is_lock lk R  issued lk x }}} wait_loop #x lk {{{ RET #(); locked lk  R }}}.
94
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97
    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (γ lo' ln' ->) "#[Hm Hinv]".
    iDestruct "Ht" as (γ' lo ln ?) "[#Hm' Ht]"; simplify_eq/=.
    iDestruct (meta_agree with "Hm Hm'") as %<-.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
98
    iLöb as "IH". wp_rec. subst. wp_pures. wp_bind (! _)%E.
99
    iInv N as (o n) "(Hlo & Hln & Ha)".
100 101
    wp_load. destruct (decide (x = o)) as [->|Hneq].
    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
102
      + iModIntro. iSplitL "Hlo Hln Hainv Ht".
103
        { iNext. iExists o, n. iFrame. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
104
        wp_pures. case_bool_decide; [|done]. wp_if.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto 20.
106
      + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
107
        set_solver.
108
    - iModIntro. iSplitL "Hlo Hln Ha".
109
      { iNext. iExists o, n. by iFrame. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
110
      wp_pures. case_bool_decide; [simplify_eq |].
111
      wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
112 113
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
  Lemma acquire_spec lk R :
    {{{ is_lock lk R }}} acquire lk {{{ RET #(); locked lk  R }}}.
116
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (γ lo ln ->) "#[Hm Hinv]".
Robbert Krebbers's avatar
Robbert Krebbers committed
118
    iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
119
    iInv N as (o n) "[Hlo [Hln Ha]]".
120
    wp_load. iModIntro. iSplitL "Hlo Hln Ha".
121
    { iNext. iExists o, n. by iFrame. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
122
    wp_pures. wp_bind (CAS _ _ _).
123
    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
124
    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
125
    - iMod (own_update with "Hauth") as "[Hauth Hofull]".
126 127
      { eapply auth_update_alloc, prod_local_update_2.
        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129
        apply (set_seq_S_end_disjoint 0). }
      rewrite -(set_seq_S_end_union_L 0).
130
      wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
131 132
      { iNext. iExists o', (S n).
        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
133
      wp_if.
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135
      iApply (wait_loop_spec (#lo, #ln) with "[-HΦ]").
      + iFrame. rewrite /is_lock /issued; eauto 20.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
136
      + by iNext.
137
    - wp_cas_fail. iModIntro.
138
      iSplitL "Hlo' Hln' Hauth Haown".
139
      { iNext. iExists o', n'. by iFrame. }
140
      wp_if. by iApply "IH"; auto.
141 142
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
143 144
  Lemma release_spec lk R :
    {{{ is_lock lk R  locked lk  R }}} release lk {{{ RET #(); True }}}.
145
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147 148
    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (γ' lo' ln' ->) "#[Hm Hinv]".
    iDestruct "Hγ" as (γ lo ln o ?) "[#Hm' Hγo]"; simplify_eq/=.
    iDestruct (meta_agree with "Hm Hm'") as %<-.
149
    wp_lam. wp_proj. wp_bind (! _)%E.
150
    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
151
    wp_load.
152
    iDestruct (own_valid_2 with "Hauth Hγo") as
153
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
154
    iModIntro. iSplitL "Hlo Hln Hauth Haown".
155
    { iNext. iExists o, n. by iFrame. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
156
    wp_pures.
157 158
    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
    iApply wp_fupd. wp_store.
159
    iDestruct (own_valid_2 with "Hauth Hγo") as
160
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
161
    iDestruct "Haown" as "[[Hγo' _]|Haown]".
162 163
    { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
    iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
164 165
    { apply auth_update, prod_local_update_1.
      by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
166
    iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
167
    iIntros "!> !>". iExists (S o), n'.
168
    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
169
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
170 171 172
End proof.

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

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