srv.v 7.3 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
3
4
5
6
From iris.program_logic Require Export weakestpre.
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.algebra Require Import frac excl dec_agree.
Zhen Zhang's avatar
Zhen Zhang committed
7
From flatcomb Require Import misc.
Zhen Zhang's avatar
Zhen Zhang committed
8
9
10
11
12
13
14
15

Definition srv : val :=
  rec: "srv" "f" "p" :=
       match: !"p" with
         InjL "x" => "p" <- InjR ("f" "x");; "srv" "f" "p"
       | InjR "_" => "srv" "f" "p"
       end.

Zhen Zhang's avatar
Zhen Zhang committed
16
17
18
Definition wait: val :=
  rec: "wait" "p" :=
    match: !"p" with
19
      InjR "r" => "r"
Zhen Zhang's avatar
Zhen Zhang committed
20
21
22
    | InjL "_" => "wait" "p"
    end.

Zhen Zhang's avatar
srv    
Zhen Zhang committed
23
24
Local Opaque wait.

Zhen Zhang's avatar
Zhen Zhang committed
25
26
27
Definition mk_srv : val :=
  λ: "f",
     let: "p" := ref (InjR #0)%V in
Zhen Zhang's avatar
Zhen Zhang committed
28
     let: "l" := newlock #() in
Zhen Zhang's avatar
Zhen Zhang committed
29
     Fork (srv "f" "p");;
Zhen Zhang's avatar
Zhen Zhang committed
30
     λ: "x",
Zhen Zhang's avatar
Zhen Zhang committed
31
        acquire "l";;
Zhen Zhang's avatar
srv    
Zhen Zhang committed
32
        "p" <- InjL "x";;
Zhen Zhang's avatar
Zhen Zhang committed
33
34
35
        let: "ret" := wait "p" in
        release "l";;
        "ret".
Zhen Zhang's avatar
Zhen Zhang committed
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

(* play with some algebraic structure to see what fit ... *)

Definition srvR := prodR fracR (dec_agreeR val).

Lemma srv_coincide:  (x1 x2: val) (q1 q2: Qp),  ((q1, DecAgree x1)  (q2, DecAgree x2))  x1 = x2.
Proof.
  intros x1 x2 q1 q2 H. destruct (decide (x1 = x2))=>//.
  exfalso. destruct H as [H1 H2].
  simpl in H2. apply dec_agree_op_inv in H2.
  by inversion H2.
Qed.

Lemma srv_update:  (x1 x2: val), (1%Qp, DecAgree x1) ~~> (1%Qp, DecAgree x2).
Proof. intros. by apply cmra_update_exclusive. Qed.

(* define the gFunctors *)
Class srvG Σ := FlatG { srv_tokG :> inG Σ srvR }.
Definition srvΣ : gFunctors := #[GFunctor (constRF srvR)].

Instance subG_srvΣ {Σ} : subG srvΣ Σ  srvG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.

Section proof.
  Context `{!heapG Σ, !lockG Σ, !srvG Σ} (N : namespace).
Zhen Zhang's avatar
Zhen Zhang committed
61
62

  Definition srv_inv
Zhen Zhang's avatar
Zhen Zhang committed
63
             (γx γ1 γ2 γ3 γ4: gname) (p: loc)
Zhen Zhang's avatar
Zhen Zhang committed
64
             (Q: val  val  Prop): iProp Σ :=
Zhen Zhang's avatar
Zhen Zhang committed
65
66
67
68
    (( (y: val), p  InjRV y  own γ1 (Excl ())  own γ3 (Excl ())) 
     ( (x: val), p  InjLV x  own γx ((1/2)%Qp, DecAgree x)  own γ1 (Excl ())  own γ4 (Excl ())) 
     ( (x: val), p  InjLV x  own γx ((1/4)%Qp, DecAgree x)  own γ2 (Excl ())  own γ4 (Excl ())) 
     ( (x y: val), p  InjRV y  own γx ((1/2)%Qp, DecAgree x)   Q x y  own γ1 (Excl ())  own γ4 (Excl ())))%I.
Zhen Zhang's avatar
Zhen Zhang committed
69
  
Zhen Zhang's avatar
Zhen Zhang committed
70
  Lemma srv_inv_timeless γx γ1 γ2 γ3 γ4 p Q: TimelessP (srv_inv γx γ1 γ2 γ3 γ4 p Q).
Zhen Zhang's avatar
srv    
Zhen Zhang committed
71
72
  Proof. apply _. Qed.

Zhen Zhang's avatar
Zhen Zhang committed
73
  Lemma wait_spec (Φ: val  iProp Σ) (Q: val  val  Prop) x γx γ1 γ2 γ3 γ4 p:
Zhen Zhang's avatar
srv    
Zhen Zhang committed
74
    heapN  N 
Zhen Zhang's avatar
Zhen Zhang committed
75
76
77
    heap_ctx  inv N (srv_inv γx γ1 γ2 γ3 γ4 p Q) 
    own γx ((1/2)%Qp, DecAgree x)  own γ3 (Excl ()) 
    ( y, own γ4 (Excl ()) - own γx (1%Qp, DecAgree x) -  Q x y- Φ y)
Zhen Zhang's avatar
srv    
Zhen Zhang committed
78
79
     WP wait #p {{ Φ }}.
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
80
    iIntros (HN) "(#Hh & #Hsrv & Hx & Ho3 & HΦ)".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
81
82
    iLöb as "IH".
    wp_rec. wp_bind (! #p)%E.
83
    iInv N as ">[Hinv|[Hinv|[Hinv|Hinv]]]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
84
85
86
87
88
89
    - iExFalso. iDestruct "Hinv" as (?) "[_ [_ Ho3']]".
      iCombine "Ho3" "Ho3'" as "Ho3".
      by iDestruct (own_valid with "Ho3") as "%".
    - admit.
    - admit.
    - iDestruct "Hinv" as (x' y') "(Hp & Hx' & % & Ho1 & Ho4)".
90
      destruct (decide (x = x')) as [->|Hneq].
Zhen Zhang's avatar
Zhen Zhang committed
91
92
      + wp_load. iVs ("Hclose" with "[Hp Ho1 Ho3]").
        { iNext. rewrite /srv_inv. iLeft. iExists y'. by iFrame. }
93
        iVsIntro. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
94
95
96
97
        iCombine "Hx" "Hx'" as "Hx".
        iDestruct (own_update with "Hx") as "==>Hx"; first by apply pair_l_frac_op.
        rewrite Qp_div_2.
        iApply ("HΦ" with "Ho4 Hx"). done.
98
99
      + admit.
  Admitted.
Zhen Zhang's avatar
Zhen Zhang committed
100

Zhen Zhang's avatar
Zhen Zhang committed
101
102
103
104
105
106
107
  Lemma mk_srv_spec (f: val) Q:
    heapN  N 
    heap_ctx   ( x:val, WP f x {{ v,  Q x v }})
     WP mk_srv f {{ f',  ( x:val, WP f' x {{ v,  Q x v }})}}.
  Proof.
    iIntros (HN) "[#Hh #Hf]".
    wp_let. wp_alloc p as "Hp".
Zhen Zhang's avatar
Zhen Zhang committed
108
109
110
111
    iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
    iVs (own_alloc (Excl ())) as (γ2) "Ho2"; first done.
    iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
    iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
112
    iVs (own_alloc (1%Qp, DecAgree #0)) as (γx) "Hx"; first done.
Zhen Zhang's avatar
Zhen Zhang committed
113
    iVs (inv_alloc N _ (srv_inv γx γ1 γ2 γ3 γ4 p Q) with "[Hp Ho1 Ho3]") as "#?".
Zhen Zhang's avatar
Zhen Zhang committed
114
115
116
    { iNext. rewrite /srv_inv. iLeft. iExists #0. by iFrame. }
    wp_let. wp_bind (newlock _).
    iApply newlock_spec=>//. iFrame "Hh".
Zhen Zhang's avatar
Zhen Zhang committed
117
    iAssert ( x, own γx (1%Qp, DecAgree x)  own γ4 (Excl ()))%I with "[Ho4 Hx]" as "Hinv".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
118
119
    { iExists #0. by iFrame. }
    iFrame "Hinv". iIntros (lk γlk) "#Hlk".
Zhen Zhang's avatar
Zhen Zhang committed
120
    wp_let. wp_apply wp_fork.
Zhen Zhang's avatar
Zhen Zhang committed
121
    iSplitR "Ho2".
Zhen Zhang's avatar
Zhen Zhang committed
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
    - (* client closure *)
      iVsIntro. wp_seq. iVsIntro.
      iAlways. iIntros (x).
      wp_let. wp_bind (acquire _). iApply acquire_spec.
      iFrame "Hlk". iIntros "Hlked Ho".
      iDestruct "Ho" as (x') "[Hx Ho4]".
      wp_seq. wp_bind (_ <- _)%E.
      iInv N as ">Hinv" "Hclose".
      iDestruct "Hinv" as "[Hinv|[Hinv|[Hinv|Hinv]]]".
      + iDestruct "Hinv" as (?) "(Hp & Ho1 & Ho3)".
        wp_store. iAssert (|=r=> own γx (1%Qp, DecAgree x))%I with "[Hx]" as "==>Hx".
        { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption.
          apply cmra_update_exclusive. done. }
        iAssert (|=r=> own γx (((1/2)%Qp, DecAgree x)  ((1/2)%Qp, DecAgree x)))%I with "[Hx]" as "==>[Hx1 Hx2]".
        { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption.
          by apply pair_l_frac_op_1'. }
        iVs ("Hclose" with "[Hp Hx1 Ho1 Ho4]").
        { iNext. iRight. iLeft. iExists x. by iFrame. }
        iVsIntro. wp_seq.
        wp_bind (wait _).
        iApply (wait_spec with "[Hx2 Ho3 Hlked]"); first by done.
        iFrame "Hh". iFrame "#". iFrame.
        iIntros (y) "Ho4 Hx %".
        wp_let. wp_bind (release _).
        iApply release_spec. iFrame "Hlk Hlked".
        iSplitL.
        * iExists x. by iFrame.
        * wp_seq. done.
      + admit.
      + admit.
      + admit.
Zhen Zhang's avatar
Zhen Zhang committed
153
    - (* server side *)
154
155
156
      iLöb as "IH".
      wp_rec. wp_let. wp_bind (! _)%E.
      iInv N as ">[Hinv|[Hinv|[Hinv|Hinv]]]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
157
158
159
160
161
162
163
164
165
      + admit.
      + iDestruct "Hinv" as (x) "(Hp & Hx & Ho1 & Ho4)".
        iAssert (|=r=> own γx (((1 / 4)%Qp, DecAgree x)  ((1 / 4)%Qp, DecAgree x)))%I with "[Hx]" as "==>[Hx1 Hx2]".
        { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption.
          replace ((1 / 2)%Qp) with (1/4 + 1/4)%Qp; last by apply Qp_div_S.
          by apply pair_l_frac_op'. }
        wp_load.
        iVs ("Hclose" with "[Hp Hx1 Ho2 Ho4]").
        { iNext. iRight. iRight. iLeft. iExists x. by iFrame. }
166
        iVsIntro. wp_match.
Zhen Zhang's avatar
Zhen Zhang committed
167
168
169
170
        wp_bind (f x).
        iApply wp_wand_r. iSplitR; first by iApply "Hf".
        iIntros (y) "%".
        wp_value. iVsIntro. wp_bind (_ <- _)%E.
171
172
173
        iInv N as ">[Hinv|[Hinv|[Hinv|Hinv]]]" "Hclose".
        * admit.
        * admit.
Zhen Zhang's avatar
Zhen Zhang committed
174
175
176
177
178
179
180
181
182
        * iDestruct "Hinv" as (x') "(Hp & Hx' & Ho2 & Ho4)".
          destruct (decide (x = x')) as [->|Hneq]; last by admit.
          wp_store. iCombine "Hx2" "Hx'" as "Hx". 
          iDestruct (own_update with "Hx") as "==>Hx"; first by apply pair_l_frac_op.
          rewrite Qp_div_S.
          iVs ("Hclose" with "[Hp Hx Ho1 Ho4]").
          { iNext. rewrite /srv_inv. iRight. iRight. iRight.
            iExists x', y. by iFrame. }
          iVsIntro. wp_seq. iApply ("IH" with "Ho2").
183
        * admit.
Zhen Zhang's avatar
Zhen Zhang committed
184
185
      + admit.
      + admit.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
186
  Admitted.