sync.v 9.67 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
3
4
5
6
From iris.program_logic Require Export weakestpre hoare.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.tests Require Import atomic.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
7
8
From iris.algebra Require Import dec_agree frac.
From iris.program_logic Require Import auth.
Zhen Zhang's avatar
Zhen Zhang committed
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
Import uPred.

(* See CaReSL paper §3.2 *)
Definition mk_sync: val :=
  λ: <>,
       let: "l" := newlock #() in
       λ: "f" "x",
          acquire "l";;
          let: "ret" := "f" "x" in
          release "l";;
          "ret".

Global Opaque mk_sync.

Section proof.
  Context `{!heapG Σ, !lockG Σ} (N: namespace).

  (* concurrent object triple: R, p . <l, α p l> e <v, β p l v>*)
  Definition conc_obj_triple {A: Type}
             (α: val  A  iProp Σ)
             (β: val  A  val  iProp Σ)
             (Ei Eo: coPset)
             (e: expr) : iProp Σ :=
    ( P Q,
       ( ( (R: val  iProp Σ) p,
             P  R p -
                l: A, α p l 
                 ( v, β p l v - Q l v  R p)))
          - {{ P }} e {{ v,  l, Q l v }})%I.

  Arguments conc_obj_triple {_} _ _ _ _ _.
  
  (* f' refines f *)
  Definition refines (f' f: val) (R: iProp Σ): iProp Σ :=
    (  (x: expr) (v: val) (P: iProp Σ) (Q: val -> iProp Σ),
         to_val x = Some v -
         {{ R  P }} f x {{ z, R  Q z }} -
         {{ P }} f' x {{ z, Q z }})%I.

  Global Instance refines_persistent f f' R: PersistentP (refines f f' R).
  Proof. apply _. Qed.

  Global Opaque refines.
  
  Definition is_syncer (R: iProp Σ) (s: val) : iProp Σ :=
    ( (f : val), WP s f {{ f', refines f' f R }})%I.

  Lemma mk_sync_spec_wp:
     (R: iProp Σ) (Φ: val -> iProp Σ),
      heapN  N 
      heap_ctx  R  ( s,  (is_syncer R s) - Φ s)  WP mk_sync #() {{ Φ }}.
  Proof.
    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
    wp_seq. wp_bind (newlock _).
    iApply newlock_spec; first by auto.
    iSplitR "HR HΦ"; first by auto.
    iFrame "HR".
    iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
    rewrite /is_syncer. iIntros (f).
    wp_let. iVsIntro. rewrite /refines. iIntros "!#".
    iIntros (x v P Q <-%of_to_val) "#Hf !# HP".
    wp_let.
    wp_bind (acquire _).
    iApply acquire_spec.
    iSplit; first by auto.
    iIntros "Hlocked R".
    wp_seq. wp_bind (f _).
    iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
    iApply wp_wand_r.
    iSplitL "Hf'"; first by auto.
    iIntros (v') "[HR HQv]".
    wp_let.
    wp_bind (release _).
    iApply release_spec.
    iFrame "HR".
    iSplitR; eauto.
    iFrame.
    by wp_seq.
  Qed.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
88
End proof.
Zhen Zhang's avatar
Zhen Zhang committed
89

Zhen Zhang's avatar
srv    
Zhen Zhang committed
90
91
Section generic.
  Context {A: Type} `{ x y : A, Decision (x = y)}.
Zhen Zhang's avatar
Zhen Zhang committed
92
  
Zhen Zhang's avatar
srv    
Zhen Zhang committed
93
  Definition syncR := authR (optionUR (prodR fracR (dec_agreeR A))).
Zhen Zhang's avatar
Zhen Zhang committed
94

Zhen Zhang's avatar
srv    
Zhen Zhang committed
95
96
  Class syncG Σ := SyncG { sync_tokG :> inG Σ syncR }.
  Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
Zhen Zhang's avatar
Zhen Zhang committed
97

Zhen Zhang's avatar
srv    
Zhen Zhang committed
98
99
  Section triple.
    Context `{!heapG Σ, !lockG Σ, !syncG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
100

Zhen Zhang's avatar
srv    
Zhen Zhang committed
101
102
103
104
105
106
107
108
109
110
111
112
113
114
    Definition gFragR (g: A) : syncR :=  Some ((1/2)%Qp, DecAgree g).
    Definition gFullR (g: A) : syncR :=  Some ((1/2)%Qp, DecAgree g).
    
    Definition gFrag (γ: gname) (g: A) : iProp Σ := own γ (gFragR g).
    Definition gFull (γ: gname) (g: A) : iProp Σ := own γ (gFullR g).
  
    Definition atomic_triple'
               (β: A  A  val  iProp Σ)
               (Ei Eo: coPset)
               (e: expr) γ : iProp Σ :=
      ( Q, ( g g' r, (True ={Eo, Ei}=> gFrag γ g) 
                     (gFrag γ g'  β g g' r ={Ei, Eo}=> Q r)) - WP e {{ Q }})%I.
  End triple.
End generic.
Zhen Zhang's avatar
Zhen Zhang committed
115
116

Section atomic_pair.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
117
  Context `{!heapG Σ, !lockG Σ, !(@syncG (val * val) _ Σ)} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
  
  Definition pcas_seq : val :=
    λ: "l1" "l2" "a" "b",
       if: !"l1" = "a"
         then if: !"l2" = "a"
                then "l1" <- "b";; "l2" <- "b";; #true
                else #false
         else #false.

  Lemma pcas_seq_spec (l1 l2: loc) (a b x1 x2: val):
     (Φ: val  iProp Σ),
      heapN  N 
      heap_ctx  l1  x1  l2  x2 
      ( (x1 = a  x2 = a) - l1  b - l2  b - Φ #true)%I 
      ( (¬ (x1 = a  x2 = a)) - l1  x1 - l2  x2 - Φ #false)%I
       WP pcas_seq #l1 #l2 a b {{ Φ }}.
  Proof.
    iIntros (Φ HN) "(#Hh & Hl1 & Hl2 & HΦ1 & HΦ2)".
    wp_seq. repeat wp_let.
    wp_load.
    wp_op=>[?|Hx1na].
    - subst.
      wp_if. wp_load.
      wp_op=>[?|Hx2na]. subst.
      + wp_if. wp_store. wp_store.
        iAssert ( (a = a  a = a))%I as "Ha"; first by auto.
        iApply ("HΦ1" with "Ha Hl1 Hl2").
      + wp_if.
        iAssert ( ¬ (a = a  x2 = a))%I as "Ha".
        { iPureIntro. move=>[_ Heq]//. }
        iApply ("HΦ2" with "Ha Hl1 Hl2").
    - subst.
      wp_if.
        iAssert ( ¬ (x1 = a  x2 = a))%I as "Ha".
        { iPureIntro. move=>[_ Heq]//. }
        iApply ("HΦ2" with "Ha Hl1 Hl2").
  Qed.

  Definition mk_pcas : val :=
    λ: "x1" "x2",
       let: "l1" := ref "x1" in
       let: "l2" := ref "x2" in
       let: "lk" := newlock #() in
       λ: "a" "b",
          acquire "lk";;
          let: "v" := pcas_seq "l1" "l2" "a" "b" in
          release "lk";;
          "v".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
166
167
168
169
  
  Definition β (a b: val) (xs xs': val * val) (v: val) : iProp Σ :=
    ((v = #true   fst xs = a  snd xs = a  fst xs' = b  snd xs' = b) 
     (v = #false  fst xs = a  snd xs = a  fst xs' = b  snd xs' = b))%I.
Zhen Zhang's avatar
Zhen Zhang committed
170

Zhen Zhang's avatar
srv    
Zhen Zhang committed
171
172
  Definition is_pcas γ (f: val): iProp Σ :=
    ( a b: val, atomic_triple' (β a b) heapN (  nclose N) (f a b) γ)%I.
Zhen Zhang's avatar
Zhen Zhang committed
173

Zhen Zhang's avatar
srv    
Zhen Zhang committed
174
175
  Lemma pcas_atomic_spec (x10 x20: val):
    heapN  N  heap_ctx  WP mk_pcas x10 x20 {{ f,  γ,  is_pcas γ f }}.
Zhen Zhang's avatar
Zhen Zhang committed
176
177
178
  Proof.
    iIntros (HN) "#Hh". repeat wp_let.
    wp_alloc l1 as "Hl1". wp_let.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
179
    wp_alloc l2 as "Hl2". iVs (own_alloc (gFullR (x10, x20)  gFragR (x10, x20))) as (γ) "Hγ"; first by done.
Zhen Zhang's avatar
Zhen Zhang committed
180
    iDestruct (own_op with "Hγ") as "[Hfull Hfrag]".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
181
    iAssert ( x1 x2, l1  x1  l2  x2  gFull γ (x1, x2))%I with "[-Hfrag]" as "HR".
Zhen Zhang's avatar
Zhen Zhang committed
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
    { iExists x10, x20. by iFrame. }
    wp_let.
    wp_bind (newlock _). iApply newlock_spec=>//.
    iFrame "Hh".
    iFrame "HR".
    iIntros (lk γ') "#Hlk".
    wp_let.
    iClear "Hfrag". (* HFrag should be handled to user? *) 
    iVsIntro. iExists γ. iAlways.
    rewrite /is_pcas.
    iIntros (a b Q) "H".
    repeat wp_let.
    wp_bind (acquire _).
    iApply acquire_spec.
    iFrame "Hlk". iIntros "Hlked Hls".
    iDestruct "Hls" as (x1 x2) "(Hl1 & Hl2 & HFulla)".
    wp_seq. repeat wp_let.
    wp_load.
    destruct (decide (x1 = a)).
    - subst. wp_op=>[_|]//.
      wp_if. wp_load.
      destruct (decide (x2 = a)).
      + subst. wp_op=>[_|]//.
        wp_if. wp_store.
        wp_store. wp_let.
        wp_let.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
208
        iDestruct ("H" $! (a, a) (b, b) #true) as "[Hvs1 Hvs2]".
Zhen Zhang's avatar
Zhen Zhang committed
209
210
211
212
213
        rewrite /is_lock.
        iDestruct "Hlk" as (l) "(% & _ & % & Hinv)".
        iInv N as ([]) ">[Hl _]" "Hclose".
        * iVs ("Hvs1" with "[]") as "Hfraga"; first by auto.
          subst. wp_store.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
214
          iAssert (β a b (a, a) (b, b) #true) as "Hβ".
Zhen Zhang's avatar
Zhen Zhang committed
215
          { iLeft. eauto. }
Zhen Zhang's avatar
srv    
Zhen Zhang committed
216
          iAssert (gFrag γ (a, a)  gFull γ (a, a) - gFrag γ (b, b)  gFull γ (b, b))%I as "H".
Zhen Zhang's avatar
Zhen Zhang committed
217
218
          { admit. }
          iDestruct ("H" with "[Hfraga HFulla]") as "[HFragb HFullb]"; first by iFrame.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
219
          
Zhen Zhang's avatar
Zhen Zhang committed
220
221
222
223
224
225
          iVs ("Hvs2" with "[HFragb Hβ]"); first by iFrame.
          rewrite /lock_inv.
          iVsIntro. iVs ("Hclose" with "[-~]").
          { iNext. iExists false.
            iFrame. iExists b, b. by iFrame. }
          iVsIntro. wp_seq. done.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
226
227
  Admitted.
End atomic_pair.
Zhen Zhang's avatar
Zhen Zhang committed
228

Zhen Zhang's avatar
Zhen Zhang committed
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
Section sync_atomic.
  Context `{!heapG Σ, !lockG Σ} (N : namespace) {A: Type}.

  Variable α: val  A  iProp Σ.
  Variable β: val  A  val  iProp Σ.
  Variable f_cons f_seq: val.
  Variable R: val  iProp Σ.

  Definition mk_whatever (f_cons: val) (f_seq: val) : val :=
    λ: <>,
         let: "x" := f_cons #() in
         let: "s" := mk_sync #() in
         "s" (λ:<>, f_seq "x").

  Definition whatever_triple (obj: val) :=
    conc_obj_triple α β (nclose heapN)  (obj #()).

  Definition whatever_seq_spec :=
     (p: val) (l: A) (Φ: val  iProp Σ),
      heapN  N 
      heap_ctx  α p l  ( v, β p l v - Φ v)
       WP f_seq p {{ Φ }}.

  Definition f_cons_spec :=
     (Φ: val  iProp Σ),
      heapN  N 
      heap_ctx  ( v, R v - Φ v)%I
       WP f_cons #() {{ Φ }}.
  
  Lemma mk_whatever_spec:
     (Φ: val  iProp Σ),
      heapN  N 
      whatever_seq_spec 
      f_cons_spec 
      heap_ctx       
      ( obj, whatever_triple obj - Φ obj)
       WP mk_whatever f_cons f_seq #() {{ Φ }}.
  Proof.
    iIntros (Φ HN Hseq Hcons) "[#Hh HΦ]".
    wp_let. wp_bind (f_cons _). iApply Hcons=>//.
    iFrame "Hh".
    iIntros (v) "HR".
    wp_let. rewrite /mk_sync. (* TODO: use the derived lemmas above *)
    wp_seq. wp_bind (newlock _). iApply (newlock_spec)=>//.
    iFrame "Hh HR".
    iIntros (lk γ) "#Hlk".
    repeat wp_let.
    iApply "HΦ".
    rewrite /whatever_triple /conc_obj_triple.
    iIntros (P Q) "#H".
    iAlways. iIntros "HP". wp_seq.
    iSpecialize ("H" $! R v).
    wp_bind (acquire _).
    iApply acquire_spec.
    iFrame "Hlk". iIntros "Hlked HR".
    iDestruct ("H" with "[HP HR]") as (x) "[Hl Hnext]"; first by iFrame.
    wp_seq. wp_let.
    iApply Hseq=>//. iFrame "Hh Hl".
    iIntros (v') "Hbeta".
    iDestruct ("Hnext" $! v' with "Hbeta") as "[HQ HR]".
    wp_let. wp_bind (release _). iApply release_spec.
    iFrame "Hlk Hlked HR".
    wp_seq. iVsIntro. by iExists x.
  Qed.
End sync_atomic.