map.v 8.84 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From actris.channel Require Import proto_channel proofmode.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.heap_lang Require Import proofmode notation lib.spin_lock.
3
From actris.utils Require Import llist contribution.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
From iris.algebra Require Import gmultiset.

Robbert Krebbers's avatar
Robbert Krebbers committed
6 7
Definition map_worker : val :=
  rec: "go" "map" "l" "c" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11 12
    acquire "l";;
      send "c" #true;;
      if: ~recv "c" then release "l" else
      let: "x" := recv "c" in
    release "l";;
Robbert Krebbers's avatar
Robbert Krebbers committed
13
      let: "y" := "map" "x" in
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17
    acquire "l";;
      send "c" #false;;
      send "c" "y";;
    release "l";;
Robbert Krebbers's avatar
Robbert Krebbers committed
18
    "go" "map" "l" "c".
Robbert Krebbers's avatar
Robbert Krebbers committed
19

Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
Definition start_map_workers : val :=
  rec: "go" "n" "map" "l" "c" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
22
    if: "n" = #0 then #() else
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24
    Fork (map_worker "map" "l" "c");;
    "go" ("n" - #1) "map" "l" "c".
Robbert Krebbers's avatar
Robbert Krebbers committed
25

Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29 30 31
Definition start_map_service : val := λ: "n" "map",
  start_chan (λ: "c",
    let: "l" := newlock #() in
    start_map_workers "n" "map" "l" "c").

Definition par_map_server : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  rec: "go" "n" "c" "xs" "ys" :=
33
    if: "n" = #0 then #() else
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    if: recv "c" then (* send item to map_worker *)
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36 37 38 39
      if: lisnil "xs" then
        send "c" #false;;
        "go" ("n" - #1) "c" "xs" "ys"
      else
        send "c" #true;;
40 41
        send "c" (lpop "xs");;
        "go" "n" "c" "xs" "ys"
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    else (* receive item from map_worker *)
43
      let: "zs" := recv "c" in
44 45
      lprep "ys" "zs";;
      "go" "n" "c" "xs" "ys".
Robbert Krebbers's avatar
Robbert Krebbers committed
46

Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
Definition par_map : val := λ: "n" "map" "xs",
  let: "c" := start_map_service "n" "map" in
49 50 51
  let: "ys" := lnil #() in
  par_map_server "n" "c" "xs" "ys";;
  "ys".
Robbert Krebbers's avatar
Robbert Krebbers committed
52

Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55
Class mapG Σ A `{Countable A} := {
  map_contributionG :> contributionG Σ (gmultisetUR A);
  map_lockG :> lockG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
58
Section map.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  Context `{Countable A} {B : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
  Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A} (N : namespace).
  Context (IA : A  val  iProp Σ) (IB : B  val  iProp Σ) (map : A  list B).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Local Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65 66 67
  Implicit Types n : nat.

  Definition map_spec (vmap : val) : iProp Σ := ( x v,
    {{{ IA x v }}}
      vmap v
68
    {{{ l ws, RET #l; llist l ws  [ list] y;w  map x;ws, IB y w }}})%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
69

Robbert Krebbers's avatar
Robbert Krebbers committed
70
  Definition map_worker_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72 73 74 75 76 77
      nat -d> gmultiset A -d> iProto Σ := λ i X,
    let rec : nat  gmultiset A  iProto Σ := rec in
    (if i is 0 then END else
     ((<!> x v, MSG v {{ IA x v }}; rec i (X  {[ x ]}))
        <+>
      rec (pred i) X
     ) <{ i  1  X =  }&>
78
         <?> x (l : loc) ws, MSG #l {{  x  X   llist l ws  [ list] y;w  map x;ws, IB y w }};
79
         rec i (X  {[ x ]}))%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  Instance map_worker_protocol_aux_contractive : Contractive map_worker_protocol_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85
  Definition map_worker_protocol := fixpoint map_worker_protocol_aux.
  Global Instance map_worker_protocol_unfold n X :
    ProtoUnfold (map_worker_protocol n X) (map_worker_protocol_aux map_worker_protocol n X).
  Proof. apply proto_unfold_eq, (fixpoint_unfold map_worker_protocol_aux). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87 88
  Definition map_worker_lock_inv (γ : gname) (c : val) : iProp Σ :=
    ( i X, server γ i X  c  iProto_dual (map_worker_protocol i X) @ N)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

Robbert Krebbers's avatar
Robbert Krebbers committed
90 91 92 93
  Lemma map_worker_spec γl γ vmap lk c :
    map_spec vmap -
    {{{ is_lock N γl lk (map_worker_lock_inv γ c)  client γ ( : gmultiset A) }}}
      map_worker vmap lk c
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95
    {{{ RET #(); True }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
97
    wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
    wp_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
    iDestruct "H" as (i X) "[Hs Hc]".
    iDestruct (@server_agree with "Hs Hγ") as %[??]; destruct i as [|i]=>//=.
    iAssert  S i  1  X =  %I as %?.
    { destruct i as [|i]; last auto with lia.
      iDestruct (@server_1_agree with "Hs Hγ") as %?%leibniz_equiv; auto. }
    wp_select. wp_branch; wp_pures; last first.
    { iMod (@dealloc_client with "Hs Hγ") as "Hs /=".
      wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
      { iExists i, _. iFrame. }
      iIntros "_". by iApply "HΦ". }
    wp_recv (x v) as "HI".
    iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
    { apply (gmultiset_local_update_alloc _ _ {[ x ]}). }
    rewrite left_id_L.
    wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
    { iExists (S i), _. iFrame. }
115
    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l ws) "HI".
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129
    wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
    iDestruct "H" as (i X) "[Hs Hc]".
    iDestruct (@server_agree with "Hs Hγ")
      as %[??%gmultiset_included]; destruct i as [|i]=>//=.
    wp_select. wp_send with "[$HI]".
    { by rewrite gmultiset_elem_of_singleton_subseteq. }
    iMod (@update_client with "Hs Hγ") as "[Hs Hγ]".
    { by apply (gmultiset_local_update_dealloc _ _ {[ x ]}). }
    rewrite gmultiset_difference_diag.
    wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
    { iExists (S i), _. iFrame. }
    iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
130 131 132 133
  Lemma start_map_workers_spec γl γ n vmap lk c :
    map_spec vmap -
    {{{ is_lock N γl lk (map_worker_lock_inv γ c)  client γ (:gmultiset A) ^ n }}}
      start_map_workers #n vmap lk c
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135
    {{{ RET #(); True }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137
    iIntros "#Hmap !>" (Φ) "[#Hlk Hγs] HΦ".
    iInduction n as [|n] "IH"; wp_rec; wp_pures; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
    { by iApply "HΦ". }
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140 141
    iDestruct "Hγs" as "[Hγ Hγs]".
    wp_apply (wp_fork with "[Hγ]").
    { iNext. wp_apply (map_worker_spec with "Hmap [$]"); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
    wp_apply ("IH" with "[$] [$]").
  Qed.

  Lemma start_map_service_spec n vmap :
    map_spec vmap -
    {{{ True }}}
      start_map_service #n vmap
    {{{ c, RET c; c  map_worker_protocol n  @ N }}}.
  Proof.
    iIntros "#Hf !>"; iIntros (Φ _) "HΦ". wp_lam; wp_pures.
    wp_apply (start_chan_proto_spec N (map_worker_protocol n )); iIntros (c) "// Hc".
    wp_lam.
    iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
    wp_apply (newlock_spec N (map_worker_lock_inv γ c) with "[Hc Hs]").
    { iExists n, . iFrame. }
    iIntros (lk γl) "#Hlk".
    wp_apply (start_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
  Qed.

162
  Lemma par_map_server_spec n c l k vs xs ws X ys :
Robbert Krebbers's avatar
Robbert Krebbers committed
163
    (n = 0  X =   xs = []) 
Robbert Krebbers's avatar
Robbert Krebbers committed
164
    {{{
165
      llist l vs  llist k ws 
Robbert Krebbers's avatar
Robbert Krebbers committed
166
      c  map_worker_protocol n X @ N 
Robbert Krebbers's avatar
Robbert Krebbers committed
167
      ([ list] x;v  xs;vs, IA x v)  ([ list] y;w  ys;ws, IB y w)
Robbert Krebbers's avatar
Robbert Krebbers committed
168
    }}}
169 170 171 172
      par_map_server #n c #l #k
    {{{ ys' ws', RET #();
       ys'  (xs ++ elements X) = map 
       llist k ws'  [ list] y;w  ys' ++ ys;ws', IB y w
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174
    }}}.
  Proof.
175 176
    iIntros (Hn Φ) "(Hl & Hk & Hc & HIA & HIB) HΦ".
    iLöb as "IH" forall (n l vs xs ws X ys Hn Φ); wp_rec; wp_pures; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178
    case_bool_decide; wp_pures; simplify_eq/=.
    { destruct Hn as [-> ->]; first lia.
179
      iApply ("HΦ" $! []); simpl; auto with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
180
    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
181
    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
182 183
      destruct vs as [|v vs], xs as [|x xs]; csimpl; try done; wp_pures.
      + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
184
        iApply ("IH" with "[%] Hl Hk Hc [//] [$] HΦ"); naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
      + iDestruct "HIA" as "[HIAx HIA]". wp_select.
186
        wp_apply (lpop_spec with "Hl"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
187
        wp_send with "[$HIAx]".
188
        wp_apply ("IH" with "[] Hl Hk Hc HIA HIB"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
        iIntros (ys' ws').
190 191
        rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
        rewrite assoc_L -(comm _ [x]). iApply "HΦ".
192 193 194
    - wp_recv (x l' w) as (Hx) "[Hl' HIBx]".
      wp_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
      wp_apply ("IH" $! _ _ _ _ _ _ (_ ++ _) with "[] Hl Hk Hc HIA [HIBx HIB]"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
      { simpl; iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
196
      iIntros (ys' ws'); iDestruct 1 as (Hys) "HIB"; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
      iApply ("HΦ" $! (ys' ++ map x)). iSplit.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
      + iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200
          -?gmultiset_elem_of_singleton_subseteq //.
        rewrite (comm disj_union) gmultiset_elements_disj_union.
201
        by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204
      + by rewrite -assoc_L.
  Qed.

205
  Lemma par_map_spec n vmap l vs xs :
Robbert Krebbers's avatar
Robbert Krebbers committed
206
    0 < n 
Robbert Krebbers's avatar
Robbert Krebbers committed
207
    map_spec vmap -
208 209 210
    {{{ llist l vs  [ list] x;v  xs;vs, IA x v }}}
      par_map #n vmap #l
    {{{ k ys ws, RET #k; ys  xs = map  llist k ws  [ list] y;w  ys;ws, IB y w }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  Proof.
212
    iIntros (?) "#Hmap !>"; iIntros (Φ) "[Hl HI] HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
    wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (c) "Hc".
214 215 216 217
    wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
    wp_apply (par_map_server_spec _ _ _ _ _ _ []  [] with "[$Hl $Hk $Hc $HI //]"); first lia.
    iIntros (ys ws) "H". rewrite /= gmultiset_elements_empty !right_id_L .
    wp_pures. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
End map.