srv.v 3.83 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.

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
15
16
17
18
19
20
21
Definition wait: val :=
  rec: "wait" "p" :=
    match: !"p" with
      InjR "r" => "p" <- #0 ;; "r"
    | InjL "_" => "wait" "p"
    end.

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

(* 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
58
59
60
61
62
63
64
65
66
67

  Definition srv_inv
             (γ: gname) (p: loc)
             (Q: val  val  Prop): iProp Σ :=
    (( x: val, p  InjRV x) 
     ( (x: val) (γ2: gname), p  InjLV x  own γ ((1/2)%Qp, DecAgree x)  own γ2 (Excl ())) 
     ( (x y: val) (γ2: gname), p  InjRV y  own γ ((1/2)%Qp, DecAgree x)   Q x y  own γ2 (Excl ())))%I.

  Lemma srv_inv_timeless γ p Q: TimelessP (srv_inv γ p Q).
  Proof. apply _. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
68
  
Zhen Zhang's avatar
Zhen Zhang committed
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
  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".
    iVs (own_alloc (Excl ())) as (γ1) "Hγ1"; first done.
    iVs (own_alloc (1%Qp, DecAgree #0)) as (γ2) "Hγ2"; first done.
    iVs (inv_alloc N _ (srv_inv γ1 γ2 p Q) with "[Hp Hγ1]") as "#?".
    { iNext. rewrite /srv_inv. iLeft. iExists #0. by iFrame. }
    wp_let. wp_bind (newlock _).
    iApply newlock_spec=>//. iFrame "Hh".
    iAssert ( x: val, own γ2 (1%Qp, DecAgree x))%I with "[Hγ2]" as "Hinv"; first by eauto.
    iFrame "Hinv". iIntros (lk γ) "#Hlk".
    wp_let. wp_apply wp_fork.
    iSplitL.
    - (* client closure *)
      iVsIntro. wp_seq. iVsIntro.
      iAlways. iIntros (x).
      iLöb as "IH". wp_rec.
      wp_bind (acquire _). iApply acquire_spec.
      iFrame "Hlk". iIntros "Hlked Ho". iDestruct "Ho" as (x') "Ho".
      wp_seq. wp_bind (_ <- _)%E.
      iInv N as ">Hinv" "Hclose".
      rewrite /srv_inv.
      iDestruct "Hinv" as "[Hinv|[Hinv|Hinv]]".
      + iDestruct "Hinv" as (x'') "Hp".
        wp_store.
        iAssert (own γ2 (1%Qp, DecAgree x') - (own γ2 ((1/2)%Qp, DecAgree x)  own γ2 ((1/2)%Qp, DecAgree x)))%I as "Hsplit".
        { admit. }
        iDestruct ("Hsplit" with "Ho") as "[Ho1 Ho2]".
        iVs ("Hclose" with "[Hlked Hp Ho1]").
        * rewrite /locked. iNext. iRight. iLeft.
          iExists x. iFrame.
      + (* Impossible: reenter locked *)
        iExFalso. admit.
      + (* Impossible: reenter locked *)
        iExFalso. admit.