flat.v 20.7 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
From iris.program_logic Require Export weakestpre saved_prop.
Zhen Zhang's avatar
Zhen Zhang committed
2
3
4
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Zhen Zhang's avatar
Zhen Zhang committed
5
From iris.algebra Require Import auth upred frac agree excl dec_agree upred_big_op gset gmap.
Zhen Zhang's avatar
Zhen Zhang committed
6
From iris_atomic Require Import misc atomic treiber atomic_sync evmap.
Zhen Zhang's avatar
Zhen Zhang committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

Definition doOp : val :=
  λ: "f" "p",
     match: !"p" with
       InjL "x" => "p" <- InjR ("f" "x")
     | InjR "_" => #()
     end.

Definition doOp' (f:val) : val :=
  λ: "p",
     match: !"p" with
       InjL "x" => "p" <- InjR (f "x")
     | InjR "_" => #()
     end.

Definition try_srv : val :=
  λ: "lk" "s" "f",
    if: try_acquire "lk"
      then let: "hd" := !"s" in
           let: "f'" := doOp "f" in
           iter "hd" "f'";;
           release "lk"
      else #().

Definition loop: val :=
  rec: "loop" "f" "p" "s" "lk" :=
    match: !"p" with
    InjL "_" =>
        try_srv "lk" "s" "f";;
        "loop" "f" "p" "s" "lk"
    | InjR "r" => "r"
    end.

Definition install : val :=
  λ: "x" "s",
     let: "p" := ref (InjL "x") in
     push "s" "p";;
     "p".

Definition mk_flat : val :=
Zhen Zhang's avatar
Zhen Zhang committed
47
  λ: "f",
Zhen Zhang's avatar
Zhen Zhang committed
48
49
   let: "lk" := newlock #() in
   let: "s" := new_stack #() in
Zhen Zhang's avatar
Zhen Zhang committed
50
51
   λ: "x",
      let: "p" := install "x" "s" in
Zhen Zhang's avatar
Zhen Zhang committed
52
53
      let: "r" := loop "f" "p" "s" "lk" in
      "r".
Zhen Zhang's avatar
Zhen Zhang committed
54
55
56
57

Global Opaque doOp try_srv install loop mk_flat.

Definition reqR := prodR fracR (dec_agreeR val). (* request x should be kept same *)
Zhen Zhang's avatar
Zhen Zhang committed
58
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Zhen Zhang's avatar
Zhen Zhang committed
59
Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *)
Zhen Zhang's avatar
Zhen Zhang committed
60
61
62
Class flatG Σ := FlatG {
  req_G :> inG Σ reqR;
  tok_G :> inG Σ (authR tokmR);
Zhen Zhang's avatar
Zhen Zhang committed
63
  sp_G  :> savedPropG Σ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
64
65
66
67
}.

Definition flatΣ : gFunctors :=
  #[ GFunctor (constRF reqR);
Zhen Zhang's avatar
Zhen Zhang committed
68
69
     GFunctor (constRF (authR tokmR));
     savedPropΣ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
70
71
72
   ].

Instance subG_flatΣ {Σ} : subG flatΣ Σ  flatG Σ.
Zhen Zhang's avatar
Zhen Zhang committed
73
Proof. intros [?%subG_inG [?%subG_inG [? _]%subG_inv]%subG_inv]%subG_inv. split; apply _. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
74
75

Section proof.
Zhen Zhang's avatar
Zhen Zhang committed
76
  Context `{!heapG Σ, !lockG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
77
78
79
80
81
82
83
84
85
  Context (R: iProp Σ).

  Definition init_s (ts: toks) :=
    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ())  own γ3 (Excl ()))%I.

  Definition installed_s (ts: toks) (f x: val) :=
    let '(γx, γ1, _, γ4, γq) := ts in
    ( (P: val  iProp Σ) Q, own γx ((1/2)%Qp, DecAgree x)  P x  ({{ R  P x }} f x {{ v, R  Q x v }}) 
                             saved_prop_own γq (Q x)  own γ1 (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
86
87

  Definition received_s (ts: toks) (x: val) γr :=
Zhen Zhang's avatar
Zhen Zhang committed
88
89
90
    let '(γx, _, _, γ4, _) := ts in
    (own γx ((1/2/2)%Qp, DecAgree x)  own γr (Excl ())  own γ4 (Excl ()))%I.

Zhen Zhang's avatar
Zhen Zhang committed
91
  Definition finished_s (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
92
93
94
95
    let '(γx, γ1, _, γ4, γq) := ts in
    ( Q: val  val  iProp Σ,
       own γx ((1/2)%Qp, DecAgree x)  saved_prop_own γq (Q x) 
       Q x y  own γ1 (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
96
97
98
99

  Definition evm := ev loc toks.
  
  (* p slot invariant *)
Zhen Zhang's avatar
Zhen Zhang committed
100
  Definition p_inv (γm γr: gname) (f v: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
101
102
103
104
105
    ( (ts: toks) (p : loc),
       v = #p  evm γm p ts 
       ((* INIT *)
        ( y: val, p {1/2} InjRV y  init_s ts)
        (* INSTALLED *)
Zhen Zhang's avatar
Zhen Zhang committed
106
        ( x: val, p {1/2} InjLV x  installed_s ts f x) 
Zhen Zhang's avatar
Zhen Zhang committed
107
108
109
110
111
        (* RECEIVED *)
        ( x: val, p {1/2} InjLV x  received_s ts x γr) 
        (* FINISHED *)
        ( x y: val, p {1/2} InjRV y  finished_s ts x y)))%I.

Zhen Zhang's avatar
Zhen Zhang committed
112
  Definition srv_stack_inv γs γm γr s f := ( xs, is_stack' (p_inv γm γr f) γs xs s)%I.
Zhen Zhang's avatar
Zhen Zhang committed
113
114
115
116
117
118

  Definition srv_tokm_inv γm := ( m : tokmR, own γm ( m)  [ map] p  _  m,  v, p {1/2} v)%I.

  Lemma install_push_spec
        (Φ: val  iProp Σ)
        (p: loc) (γs γm γr: gname) (ts: toks)
Zhen Zhang's avatar
Zhen Zhang committed
119
        (s: loc) (f x: val) :
Zhen Zhang's avatar
Zhen Zhang committed
120
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
121
122
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm) 
    evm γm p ts  installed_s ts f x 
Zhen Zhang's avatar
Zhen Zhang committed
123
124
125
126
127
    p {1/2} InjLV x  (( hd, evs γs hd #p) - Φ #())
     WP push #s #p {{ Φ }}.
  Proof.
    iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)".
    rewrite /srv_stack_inv.
Zhen Zhang's avatar
Zhen Zhang committed
128
    iDestruct (push_spec N (p_inv γm γr f) (fun v => ( hd, evs γs hd #p)  v = #())%I
Zhen Zhang's avatar
Zhen Zhang committed
129
130
131
132
133
134
135
136
137
138
               with "[-HΦ]") as "Hpush"=>//.
    - iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto.
      iExists ts. iExists p. iSplit=>//. iFrame "Hpm".
      iRight. iLeft. iExists x. iFrame.
    - iApply wp_wand_r.
      iSplitL "Hpush"; first done.
      iIntros (?) "[? %]". subst.
      by iApply "HΦ".
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
139
140
141
  Definition installed_recp (ts: toks) (x: val) (Q: val  val  iProp Σ) :=
    let '(γx, _, γ3, _, γq) := ts in
    (own γ3 (Excl ())  own γx ((1/2)%Qp, DecAgree x)  saved_prop_own γq (Q x))%I.
Zhen Zhang's avatar
Zhen Zhang committed
142
143

  Lemma install_spec
Zhen Zhang's avatar
Zhen Zhang committed
144
145
        (Φ: val  iProp Σ) P Q
        (f x: val) (γs γm γr: gname) (s: loc):
Zhen Zhang's avatar
Zhen Zhang committed
146
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
147
148
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm)  P x  ({{ R  P x }} f x {{ v, R  Q x v }}) 
    ( (p: loc) (ts: toks), installed_recp ts x Q - evm γm p ts -( hd, evs γs hd #p) - Φ #p)
Zhen Zhang's avatar
Zhen Zhang committed
149
150
     WP install x #s {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
151
    iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
152
153
154
155
156
157
    wp_seq. wp_let. wp_alloc p as "Hl".
    iApply pvs_wp.
    iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
    iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
    iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
    iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
Zhen Zhang's avatar
Zhen Zhang committed
158
159
    iVs (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
    iInv N as "[Hrs >Hm]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
160
161
162
163
164
165
    iDestruct "Hm" as (m) "[Hm HRm]".
    destruct (m !! p) eqn:Heqn.
    - (* old name *)
      iDestruct (big_sepM_delete (fun p _ =>  v : val, p {1 / 2} v)%I m with "HRm") as "[Hp HRm]"=>//.
      iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hh Hl Hp". auto.
    - (* fresh name *)
Zhen Zhang's avatar
Zhen Zhang committed
166
      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as "==>[Hm1 #Hm2]"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
167
168
      iDestruct "Hl" as "[Hl1 Hl2]".
      iVs ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
Zhen Zhang's avatar
Zhen Zhang committed
169
      + iNext. iFrame. iExists (<[p := (, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
170
171
        iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
        iSplitL "Hl1"; last by iAssumption. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
172
      + iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
Zhen Zhang's avatar
Zhen Zhang committed
173
174
        iVsIntro. wp_let. wp_bind ((push _) _).
        iApply install_push_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
175
176
        iFrame "#". rewrite /evm /installed_s. iFrame.
        iSplitL "Hpx Hf".
Zhen Zhang's avatar
Zhen Zhang committed
177
        { iExists P, Q. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
178
        iIntros "Hhd". wp_seq. iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
179
        iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
Zhen Zhang's avatar
Zhen Zhang committed
180
        { rewrite /installed_recp. iFrame. iFrame "#". }
Zhen Zhang's avatar
Zhen Zhang committed
181
        by iApply ("HΦ" with "[]").
Zhen Zhang's avatar
Zhen Zhang committed
182
183
184
  Qed.

  Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) (γs γm γr: gname) xs:
Zhen Zhang's avatar
Zhen Zhang committed
185
186
    heapN  N 
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm)  own γr (Excl ())  R 
Zhen Zhang's avatar
Zhen Zhang committed
187
188
189
    is_list' γs hd xs  (own γr (Excl ()) - R - Φ #())
     WP doOp f {{ f', WP iter #hd f' {{ Φ }} }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
190
    iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
191
192
193
194
    iApply pvs_wp.
    iDestruct (dup_is_list' with "[Hlist']") as "==>[Hl1 Hl2]"; first by iFrame.
    iDestruct (dup_is_list' with "[Hl2]") as "==>[Hl2 Hl3]"; first by iFrame.
    iVsIntro. wp_seq.
Zhen Zhang's avatar
Zhen Zhang committed
195
196
    iDestruct (iter_spec _ (p_inv γm γr f) (fun v => v = #()  own γr (Excl ())  R)%I γs s
                         (is_list' γs hd xs  own γr (Excl ())  R)%I (srv_tokm_inv γm) xs hd
Zhen Zhang's avatar
Zhen Zhang committed
197
198
199
                         (doOp' f) (doOp' f)
                         with "[-Hl1 HΦ]") as "Hiter"=>//.
    - rewrite /f_spec.
Zhen Zhang's avatar
Zhen Zhang committed
200
201
202
      iIntros (Φ' p _ Hin) "(#Hh & #? & (Hls & Ho2 & HR) & HΦ')".
      wp_let. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
      iDestruct "Hs" as (xs' hd') "[>Hhd [>Hxs HRs]]".
Zhen Zhang's avatar
Zhen Zhang committed
203
      iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
204
205
      iDestruct "HRs" as (m) "[>Hom HRs]".
      (* acccess *)
Zhen Zhang's avatar
Zhen Zhang committed
206
207
208
      iDestruct (access with "[Hom HRs Hls1]") as (hd'') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
      iDestruct "HRx" as (v') "[>% [Hpinv' >Hhd'']]". inversion H0. subst.
      iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
Zhen Zhang's avatar
Zhen Zhang committed
209
      + iDestruct "Hp" as (y) "(>Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
210
211
212
        wp_load. iVs ("Hclose" with "[-HΦ' Ho2 HR Hls2]").
        { iNext. iFrame. iExists xs', hd'.
          iFrame "Hhd Hxs". iExists m.
Zhen Zhang's avatar
Zhen Zhang committed
213
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[Hrest Hhd'' Hevm Hp Hs]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
214
          iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
Zhen Zhang's avatar
Zhen Zhang committed
215
          iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
216
217
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
      + iDestruct "Hp" as (x') "(Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
218
219
        wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
        iDestruct "Hs" as  (P Q) "(Hx & Hpx & Hf & HoQ& Ho1 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
220
221
222
223
224
        iAssert (|=r=> own γx (((1/2/2)%Qp, DecAgree x') 
                               ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as "==>[Hx1 Hx2]".
        { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
          rewrite -{1}(Qp_div_2 (1/2)%Qp).
          by apply pair_l_frac_op'. }
Zhen Zhang's avatar
Zhen Zhang committed
225
        iVs ("Hclose" with "[-Hf Hls2 Ho1 Hx2 HR HoQ Hpx HΦ']").
Zhen Zhang's avatar
Zhen Zhang committed
226
227
228
229
        { iNext. iFrame. iExists xs', hd'.
          iFrame "Hhd Hxs". iExists m.
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
          simpl. iFrame. iExists #p''. iSplitR; auto. rewrite /allocated.
Zhen Zhang's avatar
Zhen Zhang committed
230
          iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
Zhen Zhang's avatar
Zhen Zhang committed
231
          iFrame "#". iRight. iRight. iLeft. iExists x'. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
232
        iVsIntro. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
233
        wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf HR".
Zhen Zhang's avatar
Zhen Zhang committed
234
235
        { iApply "Hf". iFrame. }
        iIntros (v) "[HR HQ]".
Zhen Zhang's avatar
Zhen Zhang committed
236
237
238
        wp_value. iVsIntro. iInv N as "[Hs >Hm]" "Hclose".
        iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
        iDestruct "HRs" as (m') "[>Hom HRs]".
Zhen Zhang's avatar
Zhen Zhang committed
239
        iDestruct (dup_is_list' with "[Hls2]") as "==>[Hls2 Hls3]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
240
        iDestruct (access with "[Hom HRs Hls2]") as (hd'''') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
241
        iDestruct "HRx" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H2. subst.
Zhen Zhang's avatar
Zhen Zhang committed
242
        iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>#Hevm2 Hps]]".
Zhen Zhang's avatar
Zhen Zhang committed
243
244
        inversion H3. subst.
        destruct (decide (γ1 = γ1'  γx = γx'  γ3 = γ3'  γ4 = γ4'  γq = γq')) as [[? [? [? [? ?]]]]|Hneq]; subst.
Zhen Zhang's avatar
Zhen Zhang committed
245
246
        {
          iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
247
          * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
248
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
249
          * iDestruct "Hp" as (?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
250
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
251
          * iDestruct "Hp" as (x5) ">(Hp & Hx & Ho2 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
            iDestruct "Hm" as (m2) "[Hom2 HRm]".
            destruct (m2 !! p'''') eqn:Heqn.
            {
              iDestruct (big_sepM_delete _ m2 with "HRm") as "[HRk HRm]"=>//.
              iDestruct "HRk" as (?) "HRk".
              iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
              rewrite Qp_div_2. wp_store.
              (* now close the invariant *)
              iDestruct (m_frag_agree with "[Hx Hx2]") as "==>[Hx %]"; first iFrame.
              subst. rewrite Qp_div_2. iVs ("Hclose" with "[-HΦ' Ho2 HR Hls3]").
              { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
                iAssert (srv_tokm_inv γm) with "[Hp1 HRm Hom2]" as "HRm".
                { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
                  iFrame. eauto. }
                iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
                iExists m'. iFrame.
                iDestruct (big_sepM_delete _ m' with "[-]") as "?"=>//.
                { simpl. iFrame. iExists #p''''.
Zhen Zhang's avatar
Zhen Zhang committed
270
271
                  iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
                  iSplitR; first auto. iFrame "Hevm". iRight. iRight.
Zhen Zhang's avatar
Zhen Zhang committed
272
                  iRight. iExists x5, v. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
273
                  iExists Q. iFrame.                  
Zhen Zhang's avatar
Zhen Zhang committed
274
275
276
277
                }
              }
              iApply "HΦ'". by iFrame.
            }
Zhen Zhang's avatar
Zhen Zhang committed
278
            { iExFalso. iApply (map_agree_none' _ _ _ m2)=>//. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
279
          * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
280
281
            iApply excl_falso. iFrame.
        }
Zhen Zhang's avatar
Zhen Zhang committed
282
        { iDestruct (evmap_frag_agree_split with "[]") as "%"; first iFrame "Hevm Hevm2".
Zhen Zhang's avatar
Zhen Zhang committed
283
284
          inversion H4. subst. by contradiction Hneq. }
      + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (y) "(_ & _ & >Ho2' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
285
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
286
287
      + destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
        iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
288
289
290
291
        wp_load. iVs ("Hclose" with "[-HΦ' HR Ho2 Hls2]").
        { iNext. iFrame. iExists xs', hd'.
          iFrame "Hhd Hxs". iExists m.
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
292
          iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
Zhen Zhang's avatar
Zhen Zhang committed
293
          iSplitR; auto. iFrame "#". iRight. iRight. iRight. iExists x', y. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
294
          iExists Q. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
295
296
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
    - apply to_of_val.
Zhen Zhang's avatar
Zhen Zhang committed
297
    - rewrite /srv_stack_inv. iFrame "#". iFrame. iIntros "(? & ? & ?)". by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
298
299
300
301
    - iApply wp_wand_r. iSplitL "Hiter"; first done.
      iIntros (?) "[% [Ho2 HR]]". subst. iApply ("HΦ" with "Ho2 HR").
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
302
  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Zhen Zhang's avatar
Zhen Zhang committed
303
  Definition finished_recp (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
304
305
    let '(γx, _, _, _, γq) := ts in
    ( Q, own γx ((1 / 2)%Qp, DecAgree x)  saved_prop_own γq (Q x)  Q x y)%I.
Zhen Zhang's avatar
Zhen Zhang committed
306
307
308

  Lemma try_srv_spec Φ (s: loc) (lk: val) (f: val)
        (γs γr γm γlk: gname):
Zhen Zhang's avatar
Zhen Zhang committed
309
310
    heapN  N 
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm) 
Zhen Zhang's avatar
Zhen Zhang committed
311
312
313
    is_lock N γlk lk (own γr (Excl ())  R)  Φ #()
     WP try_srv lk #s f {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
314
    iIntros (?) "(#? & #? & #? & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
315
316
317
318
319
320
    wp_seq. wp_let. wp_let.
    wp_bind (try_acquire _). iApply try_acquire_spec.
    iFrame "#". iSplit; last by wp_if.
    (* acquired the lock *)
    iIntros "Hlocked [Ho2 HR]".
    wp_if. wp_bind (! _)%E.
Zhen Zhang's avatar
Zhen Zhang committed
321
322
    iInv N as "[H >Hm]" "Hclose".
    iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
Zhen Zhang's avatar
Zhen Zhang committed
323
324
325
326
327
328
329
330
331
332
333
334
335
336
    wp_load. iDestruct (dup_is_list' with "[Hxs]") as "==>[Hxs1 Hxs2]"; first by iFrame.
    iVs ("Hclose" with "[Hs Hxs1 HRs Hm]").
    { iNext. iFrame. iExists xs', hd'. by iFrame. }
    iVsIntro. wp_let. wp_bind (doOp f).
    iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
    { iApply (loop_iter_list_spec (fun v => own γr (Excl ())  R  v = #()))%I=>//.
      iFrame "#". iFrame. iIntros "? ?". by iFrame. }
    iIntros (f') "Hf'".
    wp_let. wp_bind ((iter _) _).
    iApply wp_wand_r. iSplitL "Hf'"; first iApply "Hf'".
    iIntros (?) "[Ho2 [HR %]]". subst.
    wp_seq. iApply release_spec.
    iFrame "#". iFrame.
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
337

Zhen Zhang's avatar
Zhen Zhang committed
338
339
  Lemma loop_spec Φ (p s: loc) (lk: val) (f: val)
        (γs γr γm γlk: gname) (ts: toks):
Zhen Zhang's avatar
Zhen Zhang committed
340
341
    heapN  N 
    heap_ctx  inv N (srv_stack_inv γs γm γr s f  srv_tokm_inv γm) 
Zhen Zhang's avatar
Zhen Zhang committed
342
343
344
345
346
    is_lock N γlk lk (own γr (Excl ())  R) 
    own_γ3 ts  evm γm p ts 
    ( hd, evs γs hd #p)  ( x y, finished_recp ts x y - Φ y)
     WP loop f #p #s lk {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
347
    iIntros (HN) "(#Hh & #? & #? & Ho3 & #Hev & Hhd & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
348
    iLöb as "IH". wp_rec. repeat wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
349
350
351
    wp_bind (! _)%E. iInv N as "[Hinv >?]" "Hclose".
    iDestruct "Hinv" as (xs hd) "[>Hs [>Hxs HRs]]".
    iDestruct "HRs" as (m) "[>Hom HRs]".
Zhen Zhang's avatar
Zhen Zhang committed
352
    iDestruct "Hhd" as (hdp) "Hhd".
Zhen Zhang's avatar
Zhen Zhang committed
353
    destruct (m !! hdp) eqn:Heqn.
Zhen Zhang's avatar
Zhen Zhang committed
354
355
356
    - iDestruct (big_sepM_delete_later _ m with "HRs") as "[Hp Hrs]"=>//.
      iDestruct "Hp" as (?) "[>% [Hpr ?]]"; subst.
      iDestruct "Hpr" as (ts' p') "(>% & >Hp' & Hp)".
Zhen Zhang's avatar
Zhen Zhang committed
357
358
359
360
      subst. iDestruct (map_agree_eq' _ _ γs m with "[Hom Hhd]") as %H=>//; first iFrame.
      inversion H. subst.
      iDestruct (evmap_frag_agree_split with "[Hp']") as "%"; first iFrame "Hev Hp'". subst.
      destruct ts' as [[[[γx γ1] γ3] γ4] γq].
Zhen Zhang's avatar
Zhen Zhang committed
361
      iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
362
      + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
Zhen Zhang's avatar
Zhen Zhang committed
363
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
364
      + iDestruct "Hp" as (x) "(>Hp & Hs')".
Zhen Zhang's avatar
Zhen Zhang committed
365
        wp_load. iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
Zhen Zhang's avatar
Zhen Zhang committed
366
367
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
368
          iFrame. iExists #p'. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
369
          iSplitR; first auto. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
370
          iRight. iLeft. iExists x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
371
372
373
374
        iVsIntro. wp_match.
        wp_bind (try_srv _ _ _). iApply try_srv_spec=>//.
        iFrame "#". wp_seq.
        iAssert ( hd, evs γs hd #p')%I with "[Hhd]" as "Hhd"; eauto.
Zhen Zhang's avatar
Zhen Zhang committed
375
        by iApply ("IH" with "Ho3 Hhd").
Zhen Zhang's avatar
Zhen Zhang committed
376
377
      + iDestruct "Hp" as (x) "(Hp & Hx & Ho2 & Ho4)".
        wp_load.
Zhen Zhang's avatar
Zhen Zhang committed
378
        iVs ("Hclose" with "[-Ho3 HΦ Hhd]").
Zhen Zhang's avatar
Zhen Zhang committed
379
380
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
381
          iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
382
          iSplitR; first auto. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
383
          iRight. iRight. iLeft. iExists x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
384
385
386
387
        iVsIntro. wp_match.
        wp_bind (try_srv _ _ _). iApply try_srv_spec=>//.
        iFrame "#". wp_seq.
        iAssert ( hd, evs γs hd #p')%I with "[Hhd]" as "Hhd"; eauto.
Zhen Zhang's avatar
Zhen Zhang committed
388
        by iApply ("IH" with "Ho3 Hhd").
Zhen Zhang's avatar
Zhen Zhang committed
389
       + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
390
          wp_load. iVs ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
Zhen Zhang's avatar
Zhen Zhang committed
391
392
          { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
            iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
393
            iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
394
395
396
            iSplitR; first auto. iFrame.
            iLeft. iExists y. iFrame. }
          iVsIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
397
          iExists Q. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
398
399
400
401
    - iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame "Hom".
      rewrite /ev. eauto.
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
402
  Lemma mk_flat_spec (f: val) :
Zhen Zhang's avatar
Zhen Zhang committed
403
     (Φ: val  iProp Σ),
Zhen Zhang's avatar
Zhen Zhang committed
404
      heapN  N  
Zhen Zhang's avatar
Zhen Zhang committed
405
      heap_ctx  R  ( f',  synced R f' f - Φ f')  WP mk_flat f {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
406
407
408
409
410
411
412
413
414
415
  Proof.
    iIntros (Φ HN) "(#Hh & HR & HΦ)".
    iVs (own_alloc (Excl ())) as (γr) "Ho2"; first done.
    iVs (own_alloc ( (: tokmR)   )) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
    iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
    { iExists . iFrame. by rewrite big_sepM_empty. }
    wp_seq. wp_bind (newlock _).
    iApply (newlock_spec _ (own γr (Excl ())  R))%I=>//.
    iFrame "Hh Ho2 HR". iIntros (lk γlk) "#Hlk".
    wp_let. wp_bind (new_stack _).
Zhen Zhang's avatar
Zhen Zhang committed
416
    iApply (new_stack_spec' _ (p_inv γm γr f))=>//.
Zhen Zhang's avatar
Zhen Zhang committed
417
    iFrame "Hh Hm". iIntros (γ s) "#Hss".
Zhen Zhang's avatar
Zhen Zhang committed
418
    wp_let. iVsIntro. iApply "HΦ". rewrite /synced.
Zhen Zhang's avatar
Zhen Zhang committed
419
420
    iAlways. iIntros (P Q x) "#Hf".
    iIntros "!# Hp". wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
421
    wp_bind ((install _) _).
Zhen Zhang's avatar
Zhen Zhang committed
422
423
424
    iApply (install_spec _ P Q)=>//.
    iFrame "#". iFrame "Hp". iSplitR; first iApply "Hf".
    iIntros (p [[[[γx γ1] γ3] γ4] γq]) "(Ho3 & Hx & HoQ) Hev Hhd".
Zhen Zhang's avatar
Zhen Zhang committed
425
426
    wp_let. wp_bind (loop _ _ _ _).
    iApply loop_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
427
    iFrame "#". iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
428
429
430
431
    iIntros (? ?) "Hs".
    iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
    destruct (decide (x = a)) as [->|Hneq].
    - iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
432
      wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
Zhen Zhang's avatar
Zhen Zhang committed
433
      iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
Zhen Zhang's avatar
Zhen Zhang committed
434
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
Zhen Zhang's avatar
Zhen Zhang committed
435
436
      iDestruct (own_valid with "Hx") as %[_ H1].
      rewrite pair_op //= dec_agree_ne in H1=>//.
Zhen Zhang's avatar
Zhen Zhang committed
437
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
438
439

End proof.
Zhen Zhang's avatar
Zhen Zhang committed
440
441

Section atomic_sync.
Zhen Zhang's avatar
Zhen Zhang committed
442
  Context `{!heapG Σ, !lockG Σ, !syncG Σ, !evidenceG loc val unitR Σ, !flatG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
443

Zhen Zhang's avatar
Zhen Zhang committed
444
  Definition flat_sync : val :=
Zhen Zhang's avatar
Zhen Zhang committed
445
446
447
448
    λ: "f_cons" "f_seq",
        let: "l"  := "f_cons" #() in
        mk_flat ("f_seq" "l").
  
Zhen Zhang's avatar
Zhen Zhang committed
449
  Lemma flat_atomic_spec (f_cons f_seq: val) (ϕ: val  A  iProp Σ) α β Ei:
Zhen Zhang's avatar
Zhen Zhang committed
450
       (g0: A),
Zhen Zhang's avatar
Zhen Zhang committed
451
        heapN  N  seq_spec N f_seq ϕ α β   cons_spec N f_cons g0 ϕ 
Zhen Zhang's avatar
Zhen Zhang committed
452
        heap_ctx
Zhen Zhang's avatar
Zhen Zhang committed
453
         WP flat_sync f_cons f_seq {{ f,  γ, gHalf γ g0   x,  atomic_triple' α β Ei  f x γ  }}.
Zhen Zhang's avatar
Zhen Zhang committed
454
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
455
456
457
458
459
    iIntros (????) "#?". iApply (atomic_spec N mk_flat with "[-]")=>//.
    rewrite /mk_sync_spec.
    iIntros (????) "(?&?&?)".
    iApply (mk_flat_spec N R)=>//.
    iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
460
461
  Qed.
End atomic_sync.