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.