map.v 8.67 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From actris.utils Require Import list 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 33
  rec: "go" "n" "c" "xs" "ys" :=
    if: "n" = #0 then "ys" 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 40 41
      if: lisnil "xs" then
        send "c" #false;;
        "go" ("n" - #1) "c" "xs" "ys"
      else
        send "c" #true;;
        send "c" (lhead "xs");;
        "go" "n" "c" (ltail "xs") "ys"
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    else (* receive item from map_worker *)
43 44
      let: "zs" := recv "c" in
      "go" "n" "c" "xs" (lapp "zs" "ys").
Robbert Krebbers's avatar
Robbert Krebbers committed
45

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
55
Section map.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  Context `{Countable A} {B : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
  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
59
  Local Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62 63 64 65
  Implicit Types n : nat.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
67
  Definition map_worker_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71 72 73 74
      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 =  }&>
Robbert Krebbers's avatar
Robbert Krebbers committed
75
         <?> x ws, MSG llist ws {{  x  X   [ list] y;w  map x;ws, IB y w }};
76
         rec i (X  {[ x ]}))%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  Instance map_worker_protocol_aux_contractive : Contractive map_worker_protocol_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81 82
  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
83

Robbert Krebbers's avatar
Robbert Krebbers committed
84 85
  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
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90
  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
91 92
    {{{ RET #(); True }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
94
    wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
    wp_apply (acquire_spec with "Hlk"); iIntros "[Hl H]".
Robbert Krebbers's avatar
Robbert Krebbers committed
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
    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. }
Robbert Krebbers's avatar
Robbert Krebbers committed
112
    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (w) "HI".
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115 116 117 118 119 120 121 122 123 124 125 126
    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
127 128 129 130
  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
131 132
    {{{ RET #(); True }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134
    iIntros "#Hmap !>" (Φ) "[#Hlk Hγs] HΦ".
    iInduction n as [|n] "IH"; wp_rec; wp_pures; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
    { by iApply "HΦ". }
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137 138
    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
139
    wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
    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
157 158
  Qed.

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

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