mapper.v 8.65 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5
From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
From osiris.utils Require Import list compare spin_lock contribution.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From osiris.examples Require Import sort_elem.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 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 58 59 60 61 62 63 64 65 66 67 68 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 112 113 114 115 116 117 118 119 120 121 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 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
From iris.algebra Require Import gmultiset.

Definition mapper : val :=
  rec: "go" "f" "l" "c" :=
    acquire "l";;
      send "c" #true;;
      if: ~recv "c" then release "l" else
      let: "x" := recv "c" in
    release "l";;
      let: "y" := "f" "x" in
    acquire "l";;
      send "c" #false;;
      send "c" "y";;
    release "l";;
    "go" "f" "l" "c".

Definition start_mappers : val :=
  rec: "go" "n" "f" "l" "c" :=
    if: "n" = #0 then #() else
    Fork (mapper "f" "l" "c");;
    "go" ("n" - #1) "f" "l" "c".

Definition loop_mappers : val :=
  rec: "go" "n" "c" "xs" "ys" :=
    if: "n" = #0 then "ys" else
    if: recv "c" then
      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"
    else
      let: "y" := recv "c" in
      "go" "n" "c" "xs" (lcons "y" "ys").

Definition mapper_service : val := λ: "n" "f" "xs",
  let: "l" := new_lock #() in
  let: "c" := start_chan (λ: "c",
    start_mappers "n" "f" "l" "c") in
  loop_mappers "n" "c" "xs" (lnil #()).

Class map_sortG Σ A `{Countable A} := {
  map_sort_contributionG :> contributionG Σ (gmultisetUR A);
  map_sort_lockG :> lockG Σ;
}.

Section mapper.
  Context `{Countable A, Countable B}.
  Context `{!heapG Σ, !proto_chanG Σ, map_sortG Σ A} (N : namespace).
  Context (IA : A  val  iProp Σ) (IB : B  val  iProp Σ) (f : A  B).
  Local Open Scope nat_scope.

  Definition mapper_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) :
      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 =  }&>
         <?> x w, MSG w {{  x  X   IB (f x) w }}; rec i (X  {[ x ]}))%proto.
  Instance mapper_protocol_aux_contractive : Contractive mapper_protocol_aux.
  Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
  Definition mapper_protocol := fixpoint mapper_protocol_aux.
  Global Instance mapper_protocol_unfold n X :
    ProtoUnfold (mapper_protocol n X) (mapper_protocol_aux mapper_protocol n X).
  Proof. apply proto_unfold_eq, (fixpoint_unfold mapper_protocol_aux). Qed.

  Definition mapper_lock_inv (γ : gname) (c : val) : iProp Σ :=
    ( i X, server γ i X  c  iProto_dual (mapper_protocol i X) @ N)%I.

  Lemma mapper_spec γ (ff : val) lk c q :
    ( x v, {{{ IA x v }}} ff v {{{ w, RET w; IB (f x) w }}}) -
    {{{ is_lock N lk (mapper_lock_inv γ c) 
        unlocked N lk q  client γ ( : gmultiset A) }}}
      mapper ff #lk c
    {{{ RET #(); True }}}.
  Proof.
    iIntros "#Hf !>" (Φ) "(#Hlk & Hu & Hγ) HΦ". iLöb as "IH".
    wp_rec; wp_pures.
    wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
    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. }
    clear dependent i X. iIntros "Hu". wp_apply ("Hf" with "HI"); iIntros (w) "HI".
    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.

  Lemma start_mappers_spec γ (n : nat) (ff : val) lk c q :
    ( x v, {{{ IA x v }}} ff v {{{ w, RET w; IB (f x) w }}}) -
    {{{ is_lock N lk (mapper_lock_inv γ c)  unlocked N lk q 
        n * client γ (:gmultiset A) }}}
      start_mappers #n ff #lk c
    {{{ RET #(); True }}}.
  Proof.
    iIntros "#Hf !>" (Φ) "(#Hlk & Hu & Hγs) HΦ".
    iInduction n as [|n] "IH" forall (q); wp_rec; wp_pures; simpl.
    { by iApply "HΦ". }
    iDestruct "Hγs" as "[Hγ Hγs]"; iDestruct "Hu" as "[Hu Hu']".
    wp_apply (wp_fork with "[Hγ Hu]").
    { iNext. wp_apply (mapper_spec with "Hf [$]"); auto. }
    wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
    wp_apply ("IH" with "[$] [$] [$]").
  Qed.

  Lemma loop_mappers_spec (n : nat) c vs xs ws X_send xs_recv :
    (n = 0  X_send =   xs = []) 
    {{{
      c  mapper_protocol n (X_send : gmultiset A) @ N 
      ([ list] x;v  xs;vs, IA x v)  ([ list] x;w  xs_recv;ws, IB (f x) w)
    }}}
      loop_mappers #n c (val_encode vs) (val_encode ws)
    {{{ ys ws, RET (val_encode ws);
       ys ++ (f <$> xs_recv)  f <$> (elements X_send ++ xs ++ xs_recv) 
       [ list] y;w  ys ++ (f <$> xs_recv);ws, IB y w
    }}}.
  Proof.
    iIntros (Hn Φ) "(Hc & Hxs & Hxs_recv) HΦ".
    iLöb as "IH" forall (n vs xs ws X_send xs_recv Hn Φ); wp_rec; wp_pures; simpl.
    case_bool_decide; wp_pures; simplify_eq/=.
    { destruct Hn as [-> ->]; first lia.
      iApply ("HΦ" $! []); simpl. rewrite big_sepL2_fmap_l. auto. }
    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
    - wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
      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.
        iApply ("IH" with "[] Hc [//] [$] HΦ"). iPureIntro; naive_solver.
      + iDestruct "Hxs" as "[Hx Hxs]". wp_select.
        wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
        wp_send with "[$Hx]".
        wp_apply (ltail_spec (A:=val) with "[//]"); iIntros (_).
        wp_apply ("IH" with "[] Hc Hxs Hxs_recv"); first done.
        iIntros (ys ws').
        rewrite gmultiset_elements_disj_union gmultiset_elements_singleton -!assoc_L.
        iApply "HΦ".
    - wp_recv (x w) as (HH) "HIfx".
      wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
      wp_apply ("IH" $! _ _ _ _ _ (_ :: _) with "[] Hc Hxs [HIfx Hxs_recv]"); first done.
      { simpl; iFrame. }
      iIntros (ys ws'); iDestruct 1 as (Hys) "H"; simplify_eq/=.
      iApply ("HΦ" $! (ys ++ [f x])). iSplit.
      + iPureIntro. rewrite -assoc_L /= Hys.
        rewrite {2}(gmultiset_disj_union_difference {[ x ]} X_send)
          -?gmultiset_elem_of_singleton_subseteq //.
        rewrite (comm disj_union) gmultiset_elements_disj_union.
        rewrite gmultiset_elements_singleton.
        by rewrite -assoc_L (assoc_L _ [x]) (comm _ [x]) -!assoc_L.
      + by rewrite -assoc_L.
  Qed.

  Lemma mapper_service_spec (n : nat) (ff : val) vs xs :
    0 < n 
    ( x v, {{{ IA x v }}} ff v {{{ w, RET w; IB (f x) w }}}) -
    {{{ [ list] x;v  xs;vs, IA x v }}}
      mapper_service #n ff (val_encode vs)
    {{{ ys ws, RET (val_encode ws); ys  f <$> xs 
                                    [ list] y;w  ys;ws, IB y w }}}.
  Proof.
    iIntros (?) "#Hf !>"; iIntros (Φ) "HI HΦ". wp_lam; wp_pures.
    wp_apply (new_lock_spec N with "[//]"); iIntros (lk) "[Hu Hlk]".
    wp_apply (start_chan_proto_spec N (mapper_protocol n ) with "[Hu Hlk]");
      try iNext; iIntros (c) "Hc".
    { wp_lam.
      iMod (contribution_initN (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
      iMod ("Hlk" $! (mapper_lock_inv γ c) with "[Hc Hs]") as "#Hlk".
      { iExists n, . iFrame. }
      wp_apply (start_mappers_spec with "Hf [$Hlk $Hu $Hγs]"); auto. }
    wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (_).
    wp_apply (loop_mappers_spec _ _ _ _ []  [] with "[$Hc $HI //]"); first lia.
    iIntros (ys ws). rewrite /= !right_id_L gmultiset_elements_empty. iApply "HΦ".
  Qed.
End mapper.