flat.v 24.3 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
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
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.

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
52
   λ: "x",
      let: "p" := install "x" "s" in
      loop "f" "p" "s" "lk".
Zhen Zhang's avatar
Zhen Zhang committed
53
54
55
56

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
57
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Zhen Zhang's avatar
Zhen Zhang committed
58
59
60
61
62
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
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
76

Section proof.
  Context `{!heapG Σ, !lockG Σ, !evidenceG loc val Σ, !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 := (1%Qp, DecAgree (γx, γ1, γ3, γ4, γq))]}  m). iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
170
171
172
173
174
175
176
177
178
        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
179
180
181
        iFrame.
        iSplitL "Hpx Hx1 Hf".
        { iExists P, Q. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
182
        iIntros "Hhd". wp_seq. iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
183
184
185
        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
186
187
188
  Qed.

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

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

Zhen Zhang's avatar
Zhen Zhang committed
408
  Definition flatten (f' f: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
409
    ( P Q (x: val), ({{ R  P x }} f x {{ v, R  Q x v }})  ({{ P x }} f' x {{ v,  Q x v }}))%I.
Zhen Zhang's avatar
Zhen Zhang committed
410

Zhen Zhang's avatar
Zhen Zhang committed
411
  Lemma mk_flat_spec (f: val) :
Zhen Zhang's avatar
Zhen Zhang committed
412
     (Φ: val  iProp Σ),
Zhen Zhang's avatar
Zhen Zhang committed
413
      heapN  N  
Zhen Zhang's avatar
Zhen Zhang committed
414
      heap_ctx  R  ( f',  flatten f' f - Φ f')  WP mk_flat f {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
415
416
417
418
419
420
421
422
423
424
  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
425
    iApply (new_stack_spec' _ (p_inv γm γr f))=>//.
Zhen Zhang's avatar
Zhen Zhang committed
426
    iFrame "Hh Hm". iIntros (γ s) "#Hss".
Zhen Zhang's avatar
Zhen Zhang committed
427
    wp_let. iVsIntro. iApply "HΦ". rewrite /flatten.
Zhen Zhang's avatar
Zhen Zhang committed
428
429
    iAlways. iIntros (P Q x) "#Hf".
    iIntros "!# Hp". wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
430
    wp_bind ((install _) _).
Zhen Zhang's avatar
Zhen Zhang committed
431
432
433
    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
434
435
    wp_let. iApply loop_spec=>//.
    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
441
      iNext. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
      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
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544

Definition syncR := prodR fracR (dec_agreeR val).  (* FIXME: can't use a general A instead of val *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].

Instance subG_syncΣ {Σ} : subG syncΣ Σ  syncG Σ.
Proof. by intros ?%subG_inG. Qed.

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

  Definition A := val.

  Definition gFragR g : syncR := ((1/2)%Qp, DecAgree g).
  Definition gFullR g : syncR := ((1/2)%Qp, DecAgree g).

  Definition gFrag (γ: gname) g : iProp Σ := own γ (gFragR g).
  Definition gFull (γ: gname) g : iProp Σ := own γ (gFullR g).
  
  Global Instance frag_timeless γ g: TimelessP (gFrag γ g).
  Proof. apply _. Qed.

  Global Instance full_timeless γ g: TimelessP (gFull γ g).
  Proof. apply _. Qed.
  
  Definition atomic_triple'
             (α: val  iProp Σ)
             (β: val  A  A  val  iProp Σ)
             (Ei Eo: coPset)
             (f x: val) γ : iProp Σ :=
    ( P Q, ( g, (P x ={Eo, Ei}=> gFrag γ g   α x) 
                  (gFrag γ g   α x ={Ei, Eo}=> P x) 
                  ( g' r, gFrag γ g'  β x g g' r ={Ei, Eo}=> Q x r))
            - {{ P x }} f x {{ v,  Q x v }})%I.

  Definition sync : val :=
    λ: "f_cons" "f_seq",
        let: "l"  := "f_cons" #() in
        mk_flat ("f_seq" "l").

  Definition seq_spec (f: val) (ϕ: val  A  iProp Σ) α β (E: coPset) :=
       (Φ: val  iProp Σ) (l: val),
         {{ True }} f l {{ f',  ( (x: val) (Φ: val  iProp Σ) (g: A),
                               heapN  N 
                               heap_ctx  ϕ l g   α x 
                               ( (v: val) (g': A), ϕ l g' - β x g g' v - |={E}=> Φ v)
                                WP f' x @ E {{ Φ }} )}}.

  Definition cons_spec (f: val) (g: A) ϕ :=
       Φ: val  iProp Σ, heapN  N 
        heap_ctx  ( (l: val) (γ: gname), ϕ l g - gFull γ g - gFrag γ g - Φ l)
         WP f #() {{ Φ }}.
  
  Lemma atomic_spec (f_cons f_seq: val) (ϕ: val  A  iProp Σ) α β Ei:
       (g0: A),
        heapN  N  seq_spec f_seq ϕ α β   cons_spec f_cons g0 ϕ 
        heap_ctx
         WP sync f_cons f_seq {{ f,  γ, gFrag γ g0   x,  atomic_triple' α β Ei  f x γ  }}.
  Proof.
    iIntros (g0 HN Hseq Hcons) "#Hh". repeat wp_let.
    wp_bind (f_cons _). iApply Hcons=>//. iFrame "Hh".
    iIntros (l γ) "Hϕ HFull HFrag".
    wp_let. wp_bind (f_seq _)%E.
    iApply wp_wand_r. iSplitR; first by iApply (Hseq with "[]")=>//.
    iIntros (f Hf). iApply (mk_flat_spec _ ( g: A, ϕ l g  gFull γ g)%I)=>//.
    iFrame "#". iSplitL "HFull Hϕ".
    { iExists g0. by iFrame. }
    iIntros (f') "#Hflatten".
    iExists γ. iFrame.
    iIntros (x). iAlways.
    rewrite /atomic_triple'.
    iIntros (P Q) "#Hvss".
    rewrite /flatten.
    iSpecialize ("Hflatten" $! P Q).
    iApply ("Hflatten" with "[]").
    iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ HgFull]".
    (* we should view shift at this point *)
    iDestruct ("Hvss" $! g) as "[Hvs1 [Hvs2 Hvs3]]".
    iApply pvs_wp.
    iVs ("Hvs1" with "HP") as "[HgFrag #Hα]".
    iVs ("Hvs2" with "[HgFrag]") as "HP"; first by iFrame.
    iVsIntro. iApply Hf=>//.
    iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
    iVs ("Hvs1" with "HP") as "[HgFrag _]".
    iCombine "HgFull" "HgFrag" as "Hg".
    rewrite /gFullR /gFragR.
    iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g')  ((1 / 2)%Qp, DecAgree g')))%I with "[Hg]" as "Hupd".
    { iApply (own_update); last by iAssumption. apply pair_l_frac_update. }
    iVs "Hupd" as "[HgFull HgFrag]".
    iVs ("Hvs3" $! g' ret with "[HgFrag Hβ]"); first by iFrame.
    iVsIntro.
    iSplitL "HgFull Hϕ'".
    - iExists g'. by iFrame.
    - done.
  Qed.
  
End atomic_sync.