flat.v 21.1 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
From iris.program_logic Require Export auth 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
6
From iris.algebra Require Import upred frac agree excl dec_agree upred_big_op gset gmap.
From iris.tests Require Import misc atomic treiber_stack.
Zhen Zhang's avatar
Zhen Zhang committed
7
Require Import flatcomb.atomic_sync.
Zhen Zhang's avatar
Zhen Zhang committed
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
47

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
48
  λ: "f",
Zhen Zhang's avatar
Zhen Zhang committed
49
50
   let: "lk" := newlock #() in
   let: "s" := new_stack #() in
Zhen Zhang's avatar
Zhen Zhang committed
51
52
   λ: "x",
      let: "p" := install "x" "s" in
Zhen Zhang's avatar
Zhen Zhang committed
53
54
      let: "r" := loop "f" "p" "s" "lk" in
      "r".
Zhen Zhang's avatar
Zhen Zhang committed
55
56
57
58

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
59
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Zhen Zhang's avatar
Zhen Zhang committed
60
61
62
63
64
Definition tokmR := evmapR loc toks. (* tie each slot to tokens *)
Definition reqmR := evmapR loc val. (* tie each slot to request value *)
Class flatG Σ := FlatG {
  req_G :> inG Σ reqR;
  tok_G :> inG Σ (authR tokmR);
Zhen Zhang's avatar
Zhen Zhang committed
65
  sp_G  :> savedPropG Σ (cofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
66
67
68
69
}.

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

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

Section proof.
  Context `{!heapG Σ, !lockG Σ, !evidenceG loc val Σ, !flatG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
79
80
81
82
83
84
85
86
87
  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
88
89

  Definition received_s (ts: toks) (x: val) γr :=
Zhen Zhang's avatar
Zhen Zhang committed
90
91
92
    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
93
  Definition finished_s (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
94
95
96
97
    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
98
99
100
101

  Definition evm := ev loc toks.
  
  (* p slot invariant *)
Zhen Zhang's avatar
Zhen Zhang committed
102
  Definition p_inv (γm γr: gname) (f v: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
103
104
105
106
107
    ( (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
108
        ( x: val, p {1/2} InjLV x  installed_s ts f x) 
Zhen Zhang's avatar
Zhen Zhang committed
109
110
111
112
113
        (* 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
114
  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
115
116
117
118
119
120

  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
121
        (s: loc) (f x: val) :
Zhen Zhang's avatar
Zhen Zhang committed
122
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
123
124
    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
125
126
127
128
129
    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
130
    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
131
132
133
134
135
136
137
138
139
140
               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
141
142
143
  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
144
145

  Lemma install_spec
Zhen Zhang's avatar
Zhen Zhang committed
146
147
        (Φ: val  iProp Σ) P Q
        (f x: val) (γs γm γr: gname) (s: loc):
Zhen Zhang's avatar
Zhen Zhang committed
148
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
149
150
    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
151
152
     WP install x #s {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
153
    iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
154
155
156
157
158
159
    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
160
161
    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
162
163
164
165
166
167
    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
168
      iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as "==>[Hm1 Hm2]"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
169
170
      iDestruct "Hl" as "[Hl1 Hl2]".
      iVs ("Hclose" with "[HRm Hm1 Hl1 Hrs]").
Zhen Zhang's avatar
Zhen Zhang committed
171
      + iNext. iFrame. iExists ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4, γq))]}  m). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
172
173
174
175
176
177
178
179
180
        rewrite <-(insert_singleton_op m)=>//.
        iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
        iSplitL "Hl1"; last by iAssumption. eauto.
      + iDestruct (pack_ev with "Hm2") as "Hev".
        iDestruct (dup_ev with "Hev") as "==>[Hev1 Hev2]".
        iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
        iVsIntro. wp_let. wp_bind ((push _) _).
        iApply install_push_spec=>//.
        iFrame "#". rewrite /evm /installed_s.
Zhen Zhang's avatar
Zhen Zhang committed
181
182
183
        iFrame.
        iSplitL "Hpx Hx1 Hf".
        { iExists P, Q. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
184
        iIntros "Hhd". wp_seq. iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
185
186
187
        iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hev1 Hhd]")=>//.
        { rewrite /installed_recp. iFrame. iFrame "#". }
        by iApply ("HΦ" with "Hev1").
Zhen Zhang's avatar
Zhen Zhang committed
188
189
190
  Qed.

  Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) (γs γm γr: gname) xs:
Zhen Zhang's avatar
Zhen Zhang committed
191
192
    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
193
194
195
    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
196
    iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
197
198
199
200
    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
201
202
    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
203
204
205
                         (doOp' f) (doOp' f)
                         with "[-Hl1 HΦ]") as "Hiter"=>//.
    - rewrite /f_spec.
Zhen Zhang's avatar
Zhen Zhang committed
206
207
208
      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
209
      iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
210
211
212
213
214
215
      iDestruct "HRs" as (m) "[>Hom HRs]".
      (* acccess *)
      iDestruct (access with "[Hom HRs Hls1]") as (hd'' ?) "(Hrest & HRx & % & Hom)"=>//; first iFrame.
      iDestruct "HRx" as (v') "[>% [Hpinv' >Hhd'']]". inversion H1. subst.
      iDestruct "Hpinv'" as (ts p'') "[>% [>Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst.
      + iDestruct "Hp" as (y) "(>Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
216
217
218
        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
219
          iFrame "Hom". iDestruct (big_sepM_delete _ m with "[Hrest Hhd'' Hevm Hp Hs]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
220
221
222
223
          iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
          iSplitR; first done. iFrame. iLeft. iExists y. iFrame. }
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
      + iDestruct "Hp" as (x') "(Hp & Hs)".
Zhen Zhang's avatar
Zhen Zhang committed
224
225
226
        wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
        iDestruct "Hs" as  (P Q) "(Hx & Hpx & Hf & HoQ& Ho1 & Ho4)".
        iDestruct (dup_ev with "Hevm") as "==>[Hevm1 Hevm2]".
Zhen Zhang's avatar
Zhen Zhang committed
227
228
229
230
231
        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
232
        iVs ("Hclose" with "[-Hf Hls2 Ho1 Hx2 HR Hevm2 HoQ Hpx HΦ']").
Zhen Zhang's avatar
Zhen Zhang committed
233
234
235
236
        { 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
237
          iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
Zhen Zhang's avatar
Zhen Zhang committed
238
239
          iFrame. iRight. iRight. iLeft. iExists x'. iFrame. }
        iVsIntro. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
240
        wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf HR".
Zhen Zhang's avatar
Zhen Zhang committed
241
242
        { iApply "Hf". iFrame. }
        iIntros (v) "[HR HQ]".
Zhen Zhang's avatar
Zhen Zhang committed
243
244
245
        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
246
        iDestruct (dup_is_list' with "[Hls2]") as "==>[Hls2 Hls3]"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
247
248
249
250
251
        iDestruct (access with "[Hom HRs Hls2]") as (hd'''' q) "(Hrest & HRx & % & Hom)"=>//; first iFrame.
        iDestruct "HRx" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H2. subst.
        iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>Hevm Hps]]".
        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
252
253
        {
          iDestruct "Hps" as "[Hp | [Hp | [Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
254
          * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
255
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
256
          * iDestruct "Hp" as (?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
257
            iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
258
          * iDestruct "Hp" as (x5) ">(Hp & Hx & Ho2 & Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
            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
277
278
                  iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
                  iSplitR; first auto. iFrame "Hevm". iRight. iRight.
Zhen Zhang's avatar
Zhen Zhang committed
279
                  iRight. iExists x5, v. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
280
                  iExists Q. iFrame.                  
Zhen Zhang's avatar
Zhen Zhang committed
281
282
283
284
285
                }
              }
              iApply "HΦ'". by iFrame.
            }
            { iExFalso. iApply (map_agree_none' _ _ _ m2)=>//. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
286
          * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
287
288
            iApply excl_falso. iFrame.
        }
Zhen Zhang's avatar
Zhen Zhang committed
289
290
291
        { iDestruct (ev_agree with "[Hevm Hevm2]") as "==>[_ [_ %]]"; first iFrame.
          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
292
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
293
294
      + 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
295
296
297
298
        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
299
300
301
          iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
          iSplitR; auto. iFrame. iRight. iRight. iRight. iExists x', y. iFrame.
          iExists Q. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
302
303
        iVsIntro. wp_match. iApply "HΦ'". by iFrame.
    - apply to_of_val.
Zhen Zhang's avatar
Zhen Zhang committed
304
    - rewrite /srv_stack_inv. iFrame "#". iFrame. iIntros "(? & ? & ?)". by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
305
306
307
308
    - 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
309
  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Zhen Zhang's avatar
Zhen Zhang committed
310
  Definition finished_recp (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
311
312
    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
313
314
315

  Lemma try_srv_spec Φ (s: loc) (lk: val) (f: val)
        (γs γr γm γlk: gname):
Zhen Zhang's avatar
Zhen Zhang committed
316
317
    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
318
319
320
    is_lock N γlk lk (own γr (Excl ())  R)  Φ #()
     WP try_srv lk #s f {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
321
    iIntros (?) "(#? & #? & #? & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
322
323
324
325
326
327
    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
328
329
    iInv N as "[H >Hm]" "Hclose".
    iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
Zhen Zhang's avatar
Zhen Zhang committed
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
    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.
    
  Lemma loop_spec Φ (p s: loc) (lk: val) (f: val)
        (γs γr γm γlk: gname) (ts: toks):
Zhen Zhang's avatar
Zhen Zhang committed
347
348
    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
349
350
351
352
353
    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
354
    iIntros (HN) "(#Hh & #? & #? & Ho3 & Hev & Hhd & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
355
    iLöb as "IH". wp_rec. repeat wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
356
357
358
    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
359
360
    iDestruct "Hhd" as (hdp ?) "Hhd".
    destruct (m !! hdp) eqn:Heqn.
Zhen Zhang's avatar
Zhen Zhang committed
361
362
363
    - 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
364
365
      subst. iDestruct (map_agree_eq' _ _ γs m with "[Hom Hhd]") as "(Hom & Hhd & %)"=>//.
      { iFrame. rewrite /ev. eauto. }
Zhen Zhang's avatar
Zhen Zhang committed
366
      inversion H0. subst.
Zhen Zhang's avatar
Zhen Zhang committed
367
      iDestruct (ev_agree with "[Hev Hp']") as "==>[Hγs2 [Hγs %]]"; first iFrame. subst.
Zhen Zhang's avatar
Zhen Zhang committed
368
      destruct ts as [[[[γx γ1] γ3] γ4] γq].
Zhen Zhang's avatar
Zhen Zhang committed
369
      iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
Zhen Zhang's avatar
Zhen Zhang committed
370
      + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
Zhen Zhang's avatar
Zhen Zhang committed
371
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
372
      + iDestruct "Hp" as (x) "(>Hp & Hs')".
Zhen Zhang's avatar
Zhen Zhang committed
373
374
375
        wp_load. iVs ("Hclose" with "[-Hγs2 Ho3 HΦ Hhd]").
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
376
          iFrame. iExists #p'. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
377
          iSplitR; first auto. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
378
          iRight. iLeft. iExists x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
379
380
381
382
383
384
385
386
387
388
        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.
        by iApply ("IH" with "Ho3 Hγs2 Hhd").
      + iDestruct "Hp" as (x) "(Hp & Hx & Ho2 & Ho4)".
        wp_load.
        iVs ("Hclose" with "[-Hγs Ho3 HΦ Hhd]").
        { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
          iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
389
          iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
390
          iSplitR; first auto. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
391
          iRight. iRight. iLeft. iExists x. iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
392
393
394
395
396
        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.
        by iApply ("IH" with "Ho3 Hγs Hhd").
Zhen Zhang's avatar
Zhen Zhang committed
397
398
       + iDestruct "Hp" as (x y) "[>Hp Hs']". iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
          wp_load. iVs ("Hclose" with "[-Hγs Ho4 HΦ Hx HoQ HQ]").
Zhen Zhang's avatar
Zhen Zhang committed
399
400
          { iNext. iFrame. iExists xs, hd. iFrame. iExists m. iFrame.
            iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
Zhen Zhang's avatar
Zhen Zhang committed
401
            iFrame. iExists #p'. iSplitR; auto. iExists (γx, γ1, γ3, γ4, γq), p'.
Zhen Zhang's avatar
Zhen Zhang committed
402
403
404
            iSplitR; first auto. iFrame.
            iLeft. iExists y. iFrame. }
          iVsIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
405
          iExists Q. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
406
407
408
409
    - iExFalso. iApply (map_agree_none' _ _ _ m)=>//. iFrame "Hom".
      rewrite /ev. eauto.
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
410
  Lemma mk_flat_spec (f: val) :
Zhen Zhang's avatar
Zhen Zhang committed
411
     (Φ: val  iProp Σ),
Zhen Zhang's avatar
Zhen Zhang committed
412
      heapN  N  
Zhen Zhang's avatar
Zhen Zhang committed
413
      heap_ctx  R  ( f',  synced R f' f - Φ f')  WP mk_flat f {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
414
415
416
417
418
419
420
421
422
423
  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
424
    iApply (new_stack_spec' _ (p_inv γm γr f))=>//.
Zhen Zhang's avatar
Zhen Zhang committed
425
    iFrame "Hh Hm". iIntros (γ s) "#Hss".
Zhen Zhang's avatar
Zhen Zhang committed
426
    wp_let. iVsIntro. iApply "HΦ". rewrite /synced.
Zhen Zhang's avatar
Zhen Zhang committed
427
428
    iAlways. iIntros (P Q x) "#Hf".
    iIntros "!# Hp". wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
429
    wp_bind ((install _) _).
Zhen Zhang's avatar
Zhen Zhang committed
430
431
432
    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
433
434
    wp_let. wp_bind (loop _ _ _ _).
    iApply loop_spec=>//.
Zhen Zhang's avatar
Zhen Zhang committed
435
    iFrame "#". iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
436
437
438
439
    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
440
      wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
Zhen Zhang's avatar
Zhen Zhang committed
441
      iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
Zhen Zhang's avatar
Zhen Zhang committed
442
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
Zhen Zhang's avatar
Zhen Zhang committed
443
444
      iDestruct (own_valid with "Hx") as %[_ H1].
      rewrite pair_op //= dec_agree_ne in H1=>//.
Zhen Zhang's avatar
Zhen Zhang committed
445
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
446
447

End proof.
Zhen Zhang's avatar
Zhen Zhang committed
448
449
450
451

Section atomic_sync.
  Context `{!heapG Σ, !lockG Σ, !syncG Σ, !evidenceG loc val Σ, !flatG Σ} (N : namespace).

Zhen Zhang's avatar
Zhen Zhang committed
452
  Definition flat_sync : val :=
Zhen Zhang's avatar
Zhen Zhang committed
453
454
455
456
    λ: "f_cons" "f_seq",
        let: "l"  := "f_cons" #() in
        mk_flat ("f_seq" "l").
  
Zhen Zhang's avatar
Zhen Zhang committed
457
  Lemma flat_atomic_spec (f_cons f_seq: val) (ϕ: val  A  iProp Σ) α β Ei:
Zhen Zhang's avatar
Zhen Zhang committed
458
       (g0: A),
Zhen Zhang's avatar
Zhen Zhang committed
459
        heapN  N  seq_spec N f_seq ϕ α β   cons_spec N f_cons g0 ϕ 
Zhen Zhang's avatar
Zhen Zhang committed
460
        heap_ctx
Zhen Zhang's avatar
Zhen Zhang committed
461
         WP flat_sync f_cons f_seq {{ f,  γ, gHalf γ g0   x,  atomic_triple' α β Ei  f x γ  }}.
Zhen Zhang's avatar
Zhen Zhang committed
462
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
463
464
465
466
467
    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
468
469
  Qed.
End atomic_sync.