srv.v 6.89 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
Zhen Zhang's avatar
srv    
Zhen Zhang committed
19
      InjR "r" => "p" <- InjR #0 ;; "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
srv    
Zhen Zhang committed
63
             (γx γ1 γ2: gname) (p: loc)
Zhen Zhang's avatar
Zhen Zhang committed
64
             (Q: val  val  Prop): iProp Σ :=
Zhen Zhang's avatar
srv    
Zhen Zhang committed
65
    (( (x: val),   p  InjRV x  own γ1 (Excl ())) 
Zhen Zhang's avatar
Zhen Zhang committed
66
     ( (x: val),   p  InjLV x  own γx ((1/2)%Qp, DecAgree x)  own γ1 (Excl ())) 
Zhen Zhang's avatar
srv    
Zhen Zhang committed
67
     ( (x y: val), p  InjRV y  own γx ((1/2)%Qp, DecAgree x)   Q x y  own γ2 (Excl ())))%I.
Zhen Zhang's avatar
Zhen Zhang committed
68
  
Zhen Zhang's avatar
srv    
Zhen Zhang committed
69
70
71
72
73
74
75
  Lemma srv_inv_timeless γx γ1 γ2 p Q: TimelessP (srv_inv γx γ1 γ2 p Q).
  Proof. apply _. Qed.

  Lemma wait_spec (Φ: val  iProp Σ) (Q: val  val  Prop) x γx γ1 γ2 p:
    heapN  N 
    heap_ctx  inv N (srv_inv γx γ1 γ2 p Q) 
    own γx ((1/2)%Qp, DecAgree x)  own γ1 (Excl ()) 
Zhen Zhang's avatar
Zhen Zhang committed
76
    ( x y, own γ2 (Excl ()) - own γx (1%Qp, DecAgree x) -  Q x y- Φ y)
Zhen Zhang's avatar
srv    
Zhen Zhang committed
77
78
79
80
81
82
     WP wait #p {{ Φ }}.
  Proof.
    iIntros (HN) "(#Hh & #Hsrv & Hx & Hempty & HΦ)".
    iLöb as "IH".
    wp_rec. wp_bind (! #p)%E.
    iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
Zhen Zhang's avatar
Zhen Zhang committed
83
84
85
86
    + iExFalso. iDestruct "Hinv" as (?) "[_ Ho1]".
      iCombine "Hempty" "Ho1" as "Hempty".
      by iDestruct (own_valid with "Hempty") as "%".
    + iDestruct "Hinv" as (x') "(Hp & Hx' & Hissued)".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
87
88
89
90
      wp_load.
      iVs ("Hclose" with "[Hp Hx' Hissued]").
      { iNext. iRight. iLeft. iExists x'. by iFrame. }
      iVsIntro. wp_match. by iApply ("IH" with "Hx Hempty").
Zhen Zhang's avatar
Zhen Zhang committed
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
    + iDestruct "Hinv" as (x' y') "(Hp & Hx' & % & Hissued)".
      wp_load.
      destruct (decide (x = x')) as [->|Hneq].
      { subst.
        iVs ("Hclose" with "[Hp Hx' Hissued]").
        { iNext. iRight. iRight. iExists x', y'. by iFrame. }
        iVsIntro. wp_match.
        wp_bind (_ <- _)%E.
        iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
        - iExFalso. iDestruct "Hinv" as (?) "[_ Ho1]".
          iCombine "Hempty" "Ho1" as "Hempty".
          iDestruct (own_valid with "Hempty") as "%". done.
        - iExFalso. iDestruct "Hinv" as (?) "[_ [_ Ho1]]". 
          iCombine "Hempty" "Ho1" as "Hempty".
          iDestruct (own_valid with "Hempty") as "%". done.
        - iDestruct "Hinv" as (x'' y'') "(Hp & Hx'' & % & Hissued)".
          iCombine "Hx" "Hx''" as "Hx".
          destruct (decide (x' = x'')) as [->|Hneq].
          + wp_store. iVs ("Hclose" with "[Hp Hempty]").
            { iNext. iLeft. iExists #0. by iFrame. }
            iVsIntro. wp_seq.
            iDestruct (own_update with "Hx") as "Hx"; first by apply pair_l_frac_op.
            iVs "Hx". iVsIntro.
            by iApply ("HΦ" $! x'' y' with "Hissued Hx").
          + iExFalso. iDestruct (own_valid with "Hx") as "%".
            iPureIntro. apply Hneq. destruct H1 as [_ Hag]. apply dec_agree_op_inv in Hag.
            by inversion Hag. }
      { iCombine "Hx" "Hx'" as "Hx". iExFalso. iDestruct (own_valid with "Hx") as "%".
        iPureIntro. apply Hneq. destruct H0 as [_ Hag]. apply dec_agree_op_inv in Hag.
        by inversion Hag. }
  Qed.
                  
Zhen Zhang's avatar
Zhen Zhang committed
123
124
125
126
127
128
129
  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
srv    
Zhen Zhang committed
130
131
132
133
    iVs (own_alloc (Excl ())) as (γ1) "Hempty"; first done. (* black token *)
    iVs (own_alloc (Excl ())) as (γ2) "Hissued"; first done. (* white token *)
    iVs (own_alloc (1%Qp, DecAgree #0)) as (γx) "Hx"; first done.
    iVs (inv_alloc N _ (srv_inv γx γ1 γ2 p Q) with "[Hp Hempty]") as "#?".
Zhen Zhang's avatar
Zhen Zhang committed
134
135
136
    { iNext. rewrite /srv_inv. iLeft. iExists #0. by iFrame. }
    wp_let. wp_bind (newlock _).
    iApply newlock_spec=>//. iFrame "Hh".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
137
138
139
    iAssert ( x, own γx (1%Qp, DecAgree x)  own γ2 (Excl ()))%I with "[Hissued Hx]" as "Hinv".
    { iExists #0. by iFrame. }
    iFrame "Hinv". iIntros (lk γlk) "#Hlk".
Zhen Zhang's avatar
Zhen Zhang committed
140
141
142
143
144
    wp_let. wp_apply wp_fork.
    iSplitL.
    - (* client closure *)
      iVsIntro. wp_seq. iVsIntro.
      iAlways. iIntros (x).
Zhen Zhang's avatar
srv    
Zhen Zhang committed
145
146
147
      wp_let. wp_bind (acquire _). iApply acquire_spec.
      iFrame "Hlk". iIntros "Hlked Ho".
      iDestruct "Ho" as (x') "[Hx Hissued]".
Zhen Zhang's avatar
Zhen Zhang committed
148
149
150
151
      wp_seq. wp_bind (_ <- _)%E.
      iInv N as ">Hinv" "Hclose".
      rewrite /srv_inv.
      iDestruct "Hinv" as "[Hinv|[Hinv|Hinv]]".
Zhen Zhang's avatar
srv    
Zhen Zhang committed
152
      + iDestruct "Hinv" as (x'') "[Hp Hempty]".
Zhen Zhang's avatar
Zhen Zhang committed
153
        wp_store.
Zhen Zhang's avatar
srv    
Zhen Zhang committed
154
        iAssert (own γx (1%Qp, DecAgree x') - (own γx ((1/2)%Qp, DecAgree x)  own γx ((1/2)%Qp, DecAgree x)))%I as "Hsplit".
Zhen Zhang's avatar
Zhen Zhang committed
155
        { admit. }
Zhen Zhang's avatar
srv    
Zhen Zhang committed
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
        iDestruct ("Hsplit" with "Hx") as "[Hx1 Hx2]".
        iVs ("Hclose" with "[Hp Hissued Hx1]").
        { rewrite /locked. iNext. iRight. iLeft.
          iExists x. by iFrame. }
        (* now prove things about wait *)
        iVsIntro. wp_seq.
        wp_bind (wait _).
        iApply (wait_spec with "[Hempty Hx2 Hlked]"); first by auto.
        { iFrame "Hh". iFrame "~". iFrame.
          iIntros (y) "Hempty Hx HQ".
          wp_let.
          wp_bind (release _).
          iApply release_spec.
          iFrame "Hlk Hlked".
          iSplitL "Hempty Hx".
          - iExists x. by iFrame.
          - by wp_seq.
        }
Zhen Zhang's avatar
Zhen Zhang committed
174
175
176
      + (* Impossible: reenter locked *)
        iExFalso. admit.
      + (* Impossible: reenter locked *)
Zhen Zhang's avatar
srv    
Zhen Zhang committed
177
178
        iExFalso. admit.      
  Admitted.