Commit f6a4683d authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent naming & more consistent use of in-place.

parent 85f7b196
...@@ -3,7 +3,7 @@ From iris.heap_lang Require Import proofmode notation lib.spin_lock. ...@@ -3,7 +3,7 @@ From iris.heap_lang Require Import proofmode notation lib.spin_lock.
From actris.utils Require Import llist contribution. From actris.utils Require Import llist contribution.
From iris.algebra Require Import gmultiset. From iris.algebra Require Import gmultiset.
Definition map_worker : val := Definition par_map_worker : val :=
rec: "go" "map" "l" "c" := rec: "go" "map" "l" "c" :=
acquire "l";; acquire "l";;
send "c" #true;; send "c" #true;;
...@@ -17,18 +17,17 @@ Definition map_worker : val := ...@@ -17,18 +17,17 @@ Definition map_worker : val :=
release "l";; release "l";;
"go" "map" "l" "c". "go" "map" "l" "c".
Definition start_map_workers : val := Definition par_map_workers : val :=
rec: "go" "n" "map" "l" "c" := rec: "go" "n" "map" "l" "c" :=
if: "n" = #0 then #() else if: "n" = #0 then #() else
Fork (map_worker "map" "l" "c");; Fork (par_map_worker "map" "l" "c");;
"go" ("n" - #1) "map" "l" "c". "go" ("n" - #1) "map" "l" "c".
Definition start_map_service : val := λ: "n" "map", Definition par_map_service : val := λ: "n" "map" "c",
start_chan (λ: "c", let: "l" := newlock #() in
let: "l" := newlock #() in par_map_workers "n" "map" "l" "c".
start_map_workers "n" "map" "l" "c").
Definition par_map_server : val := Definition par_map_client_loop : val :=
rec: "go" "n" "c" "xs" "ys" := rec: "go" "n" "c" "xs" "ys" :=
if: "n" = #0 then #() else if: "n" = #0 then #() else
if: recv "c" then (* send item to map_worker *) if: recv "c" then (* send item to map_worker *)
...@@ -44,11 +43,11 @@ Definition par_map_server : val := ...@@ -44,11 +43,11 @@ Definition par_map_server : val :=
lprep "ys" "zs";; lprep "ys" "zs";;
"go" "n" "c" "xs" "ys". "go" "n" "c" "xs" "ys".
Definition par_map : val := λ: "n" "map" "xs", Definition par_map_client : val := λ: "n" "map" "xs",
let: "c" := start_map_service "n" "map" in let: "c" := start_chan (λ: "c", par_map_service "n" "map" "c") in
let: "ys" := lnil #() in let: "ys" := lnil #() in
par_map_server "n" "c" "xs" "ys";; par_map_client_loop "n" "c" "xs" "ys";;
"ys". lapp "xs" "ys".
Class mapG Σ A `{Countable A} := { Class mapG Σ A `{Countable A} := {
map_contributionG :> contributionG Σ (gmultisetUR A); map_contributionG :> contributionG Σ (gmultisetUR A);
...@@ -65,7 +64,7 @@ Section map. ...@@ -65,7 +64,7 @@ Section map.
Definition map_spec (vmap : val) : iProp Σ := ( x v, Definition map_spec (vmap : val) : iProp Σ := ( x v,
{{{ IA x v }}} vmap v {{{ l, RET #l; llist IB l (map x) }}})%I. {{{ IA x v }}} vmap v {{{ l, RET #l; llist IB l (map x) }}})%I.
Definition map_worker_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) : Definition par_map_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) :
nat -d> gmultiset A -d> iProto Σ := λ i X, nat -d> gmultiset A -d> iProto Σ := λ i X,
let rec : nat gmultiset A iProto Σ := rec in let rec : nat gmultiset A iProto Σ := rec in
(if i is 0 then END else (if i is 0 then END else
...@@ -75,20 +74,20 @@ Section map. ...@@ -75,20 +74,20 @@ Section map.
) <{ i 1 X = }&> ) <{ i 1 X = }&>
<?> x (l : loc), MSG #l {{ x X llist IB l (map x) }}; <?> x (l : loc), MSG #l {{ x X llist IB l (map x) }};
rec i (X {[ x ]}))%proto. rec i (X {[ x ]}))%proto.
Instance map_worker_protocol_aux_contractive : Contractive map_worker_protocol_aux. Instance par_map_protocol_aux_contractive : Contractive par_map_protocol_aux.
Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed. Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
Definition map_worker_protocol := fixpoint map_worker_protocol_aux. Definition par_map_protocol := fixpoint par_map_protocol_aux.
Global Instance map_worker_protocol_unfold n X : Global Instance par_map_protocol_unfold n X :
ProtoUnfold (map_worker_protocol n X) (map_worker_protocol_aux map_worker_protocol n X). ProtoUnfold (par_map_protocol n X) (par_map_protocol_aux par_map_protocol n X).
Proof. apply proto_unfold_eq, (fixpoint_unfold map_worker_protocol_aux). Qed. Proof. apply proto_unfold_eq, (fixpoint_unfold par_map_protocol_aux). Qed.
Definition map_worker_lock_inv (γ : gname) (c : val) : iProp Σ := Definition map_worker_lock_inv (γ : gname) (c : val) : iProp Σ :=
( i X, server γ i X c iProto_dual (map_worker_protocol i X) @ N)%I. ( i X, server γ i X c iProto_dual (par_map_protocol i X) @ N)%I.
Lemma map_worker_spec γl γ vmap lk c : Lemma par_map_worker_spec γl γ vmap lk c :
map_spec vmap - map_spec vmap -
{{{ is_lock N γl lk (map_worker_lock_inv γ c) client γ ( : gmultiset A) }}} {{{ is_lock N γl lk (map_worker_lock_inv γ c) client γ ( : gmultiset A) }}}
map_worker vmap lk c par_map_worker vmap lk c
{{{ RET #(); True }}}. {{{ RET #(); True }}}.
Proof. Proof.
iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH". iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
...@@ -125,10 +124,10 @@ Section map. ...@@ -125,10 +124,10 @@ Section map.
iIntros "Hu". by wp_apply ("IH" with "[$] [$]"). iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
Qed. Qed.
Lemma start_map_workers_spec γl γ n vmap lk c : Lemma par_map_workers_spec γl γ n vmap lk c :
map_spec vmap - map_spec vmap -
{{{ is_lock N γl lk (map_worker_lock_inv γ c) client γ (:gmultiset A) ^ n }}} {{{ is_lock N γl lk (map_worker_lock_inv γ c) client γ (:gmultiset A) ^ n }}}
start_map_workers #n vmap lk c par_map_workers #n vmap lk c
{{{ RET #(); True }}}. {{{ RET #(); True }}}.
Proof. Proof.
iIntros "#Hmap !>" (Φ) "[#Hlk Hγs] HΦ". iIntros "#Hmap !>" (Φ) "[#Hlk Hγs] HΦ".
...@@ -136,32 +135,32 @@ Section map. ...@@ -136,32 +135,32 @@ Section map.
{ by iApply "HΦ". } { by iApply "HΦ". }
iDestruct "Hγs" as "[Hγ Hγs]". iDestruct "Hγs" as "[Hγ Hγs]".
wp_apply (wp_fork with "[Hγ]"). wp_apply (wp_fork with "[Hγ]").
{ iNext. wp_apply (map_worker_spec with "Hmap [$]"); auto. } { iNext. wp_apply (par_map_worker_spec with "Hmap [$]"); auto. }
wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply ("IH" with "[$] [$]"). wp_apply ("IH" with "[$] [$]").
Qed. Qed.
Lemma start_map_service_spec n vmap : Lemma par_map_service_spec n vmap c :
map_spec vmap - map_spec vmap -
{{{ True }}} {{{ c iProto_dual (par_map_protocol n ) @ N }}}
start_map_service #n vmap par_map_service #n vmap c
{{{ c, RET c; c map_worker_protocol n @ N }}}. {{{ RET #(); True }}}.
Proof. Proof.
iIntros "#Hf !>"; iIntros (Φ _) "HΦ". wp_lam; wp_pures. iIntros "#Hf !>"; iIntros (Φ) "Hc 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]". 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]"). wp_apply (newlock_spec N (map_worker_lock_inv γ c) with "[Hc Hs]").
{ iExists n, . iFrame. } { iExists n, . iFrame. }
iIntros (lk γl) "#Hlk". iIntros (lk γl) "#Hlk".
wp_apply (start_map_workers_spec with "Hf [$Hlk $Hγs]"); auto. wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
Qed. Qed.
Lemma par_map_server_spec n c l k xs X ys : Lemma par_map_client_loop_spec n c l k xs X ys :
(n = 0 X = xs = []) (n = 0 X = xs = [])
{{{ llist IA l xs llist IB k ys c map_worker_protocol n X @ N }}} {{{ llist IA l xs llist IB k ys c par_map_protocol n X @ N }}}
par_map_server #n c #l #k par_map_client_loop #n c #l #k
{{{ ys', RET #(); ys' (xs ++ elements X) = map llist IB k (ys' ++ ys) }}}. {{{ ys', RET #();
ys' (xs ++ elements X) = map llist IA l [] llist IB k (ys' ++ ys)
}}}.
Proof. Proof.
iIntros (Hn Φ) "(Hl & Hk & Hc) HΦ". iIntros (Hn Φ) "(Hl & Hk & Hc) HΦ".
iLöb as "IH" forall (n l xs X ys Hn Φ); wp_rec; wp_pures; simpl. iLöb as "IH" forall (n l xs X ys Hn Φ); wp_rec; wp_pures; simpl.
...@@ -190,18 +189,20 @@ Section map. ...@@ -190,18 +189,20 @@ Section map.
+ by rewrite -assoc_L. + by rewrite -assoc_L.
Qed. Qed.
Lemma par_map_spec n vmap l xs : Lemma par_map_client_spec n vmap l xs :
0 < n 0 < n
map_spec vmap - map_spec vmap -
{{{ llist IA l xs }}} {{{ llist IA l xs }}}
par_map #n vmap #l par_map_client #n vmap #l
{{{ k ys, RET #k; ys xs = map llist IB k ys }}}. {{{ ys, RET #(); ys xs = map llist IB l ys }}}.
Proof. Proof.
iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures. iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (c) "Hc". wp_apply (start_chan_proto_spec N (par_map_protocol n )); iIntros (c) "// Hc".
{ wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk". wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_apply (par_map_server_spec with "[$Hl $Hk $Hc //]"); first lia. wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
iIntros (ys) "[??]". rewrite /= gmultiset_elements_empty !right_id_L . iIntros (ys) "(?&Hl&Hk)". rewrite /= gmultiset_elements_empty !right_id_L.
wp_apply (lapp_spec IB _ _ [] with "[$Hl $Hk]"); iIntros "[Hk _] /=".
wp_pures. iApply "HΦ"; auto. wp_pures. iApply "HΦ"; auto.
Qed. Qed.
End map. End map.
...@@ -31,7 +31,7 @@ Instance: Params (@group) 7. ...@@ -31,7 +31,7 @@ Instance: Params (@group) 7.
(** Distributed version *) (** Distributed version *)
Definition par_map_reduce_map_server : val := Definition par_map_reduce_map : val :=
rec: "go" "n" "cmap" "csort" "xs" := rec: "go" "n" "cmap" "csort" "xs" :=
if: "n" = #0 then #() else if: "n" = #0 then #() else
if: recv "cmap" then (* send item to mapper *) if: recv "cmap" then (* send item to mapper *)
...@@ -55,7 +55,7 @@ Definition par_map_reduce_collect : val := ...@@ -55,7 +55,7 @@ Definition par_map_reduce_collect : val :=
if: "i" = "j" then lcons "y" "ys";; "go" "csort" "j" "ys" else if: "i" = "j" then lcons "y" "ys";; "go" "csort" "j" "ys" else
SOME ("j", "y"). SOME ("j", "y").
Definition par_map_reduce_reduce_server : val := Definition par_map_reduce_reduce : val :=
rec: "go" "n" "csort" "cred" "acc" "zs" := rec: "go" "n" "csort" "cred" "acc" "zs" :=
if: "n" = #0 then #() else if: "n" = #0 then #() else
if: recv "cred" then (* Send item to mapper *) if: recv "cred" then (* Send item to mapper *)
...@@ -79,16 +79,15 @@ Definition par_map_reduce_reduce_server : val := ...@@ -79,16 +79,15 @@ Definition par_map_reduce_reduce_server : val :=
Definition cmpZfst : val := λ: "x" "y", Fst "x" Fst "y". Definition cmpZfst : val := λ: "x" "y", Fst "x" Fst "y".
Definition par_map_reduce : val := λ: "n" "map" "red" "xs", Definition par_map_reduce : val := λ: "n" "map" "red" "xs",
let: "cmap" := start_map_service "n" "map" in let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
par_map_reduce_map_server "n" "cmap" "csort" "xs";; par_map_reduce_map "n" "cmap" "csort" "xs";;
send "csort" #stop;; send "csort" #stop;;
let: "cred" := start_map_service "n" "red" in let: "cred" := start_chan (λ: "c", par_map_service "n" "red" "c") in
(* We need the first sorted element in the loop to compare subsequent elements *) (* We need the first sorted element in the loop to compare subsequent elements *)
if: ~recv "csort" then lnil #() else (* Handle the empty case *) if: ~recv "csort" then #() else (* Handle the empty case *)
let: "jy" := recv "csort" in let: "jy" := recv "csort" in
let: "zs" := lnil #() in par_map_reduce_reduce "n" "csort" "cred" (SOME "jy") "xs".
par_map_reduce_reduce_server "n" "csort" "cred" (SOME "jy") "zs";; "zs".
(** Properties about the functional version *) (** Properties about the functional version *)
...@@ -240,24 +239,24 @@ Section mapper. ...@@ -240,24 +239,24 @@ Section mapper.
repeat case_bool_decide=> //; unfold RZB, prod_relation in *; naive_solver. repeat case_bool_decide=> //; unfold RZB, prod_relation in *; naive_solver.
Qed. Qed.
Lemma par_map_reduce_map_server_spec n cmap csort l xs X ys : Lemma par_map_reduce_map_spec n cmap csort l xs X ys :
(n = 0 X = xs = []) (n = 0 X = xs = [])
{{{ {{{
llist IA l xs llist IA l xs
cmap map_worker_protocol IA IZB map n (X : gmultiset A) @ N cmap par_map_protocol IA IZB map n (X : gmultiset A) @ N
csort sort_fg_head_protocol IZB RZB ys @ N csort sort_fg_head_protocol IZB RZB ys @ N
}}} }}}
par_map_reduce_map_server #n cmap csort #l par_map_reduce_map #n cmap csort #l
{{{ ys', RET #(); {{{ ys', RET #();
ys' (xs ++ elements X) = map ys' (xs ++ elements X) = map
csort sort_fg_head_protocol IZB RZB (ys ++ ys') @ N llist IA l [] csort sort_fg_head_protocol IZB RZB (ys ++ ys') @ N
}}}. }}}.
Proof. Proof.
iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ". iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ".
iLöb as "IH" forall (n xs X ys Hn Φ); wp_rec; wp_pures; simpl. iLöb as "IH" forall (n xs X ys Hn Φ); wp_rec; wp_pures; simpl.
case_bool_decide; wp_pures; simplify_eq/=. case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia. { destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []). rewrite right_id_L. auto. } iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures. destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
- wp_apply (lisnil_spec with "Hl"); iIntros "Hl". - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
destruct xs as [|x xs]; csimpl; wp_pures. destruct xs as [|x xs]; csimpl; wp_pures.
...@@ -270,7 +269,7 @@ Section mapper. ...@@ -270,7 +269,7 @@ Section mapper.
rewrite assoc_L -(comm _ [x]). iApply "HΦ". rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x k) as (Hx) "Hk". - wp_recv (x k) as (Hx) "Hk".
rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)). rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "Hcsort". wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
rewrite right_id. rewrite right_id.
wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done. wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=. iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
...@@ -330,7 +329,7 @@ Section mapper. ...@@ -330,7 +329,7 @@ Section mapper.
eapply elem_of_StronglySorted_app; set_solver. eapply elem_of_StronglySorted_app; set_solver.
Qed. Qed.
Lemma par_map_reduce_reduce_server_spec n iys iys_sorted miy zs l Y csort cred : Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
let acc := from_option (λ '(i,y,w), [(i,y)]) [] in let acc := from_option (λ '(i,y,w), [(i,y)]) [] in
let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in
(n = 0 miy = None Y = ) (n = 0 miy = None Y = )
...@@ -340,10 +339,10 @@ Section mapper. ...@@ -340,10 +339,10 @@ Section mapper.
llist IC l zs llist IC l zs
csort from_option (λ _, sort_fg_tail_protocol IZB RZB iys csort from_option (λ _, sort_fg_tail_protocol IZB RZB iys
(iys_sorted ++ acc miy)) END%proto miy @ N (iys_sorted ++ acc miy)) END%proto miy @ N
cred map_worker_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) @ N cred par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) @ N
from_option (λ '(i,y,w), IB i y w) True miy from_option (λ '(i,y,w), IB i y w) True miy
}}} }}}
par_map_reduce_reduce_server #n csort cred (accv miy) #l par_map_reduce_reduce #n csort cred (accv miy) #l
{{{ zs', RET #(); {{{ zs', RET #();
(group iys_sorted = curry red) ++ zs' (group iys ++ elements Y) = curry red (group iys_sorted = curry red) ++ zs' (group iys ++ elements Y) = curry red
llist IC l (zs' ++ zs) llist IC l (zs' ++ zs)
...@@ -394,27 +393,29 @@ Section mapper. ...@@ -394,27 +393,29 @@ Section mapper.
map_spec IZBs IC (curry red) vred - map_spec IZBs IC (curry red) vred -
{{{ llist IA l xs }}} {{{ llist IA l xs }}}
par_map_reduce #n vmap vred #l par_map_reduce #n vmap vred #l
{{{ k zs, RET #k; zs map_reduce map red xs llist IC k zs }}}. {{{ zs, RET #(); zs map_reduce map red xs llist IC l zs }}}.
Proof. Proof.
iIntros (?) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures. iIntros (?) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (cmap) "Hcmap". wp_apply (start_chan_proto_spec N (par_map_protocol IA IZB map n ));
iIntros (cmap) "// Hcmap".
{ wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
wp_apply (start_chan_proto_spec N (sort_fg_protocol IZB RZB <++> END)%proto); wp_apply (start_chan_proto_spec N (sort_fg_protocol IZB RZB <++> END)%proto);
iIntros (csort) "Hcsort". iIntros (csort) "Hcsort".
{ wp_apply (sort_service_fg_spec N with "[] Hcsort"); last by auto. { wp_apply (sort_service_fg_spec N with "[] Hcsort"); last by auto.
iApply RZB_cmp_spec. } iApply RZB_cmp_spec. }
rewrite right_id. rewrite right_id.
wp_apply (par_map_reduce_map_server_spec with "[$Hl $Hcmap $Hcsort]"); first lia. wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
iIntros (iys). rewrite gmultiset_elements_empty right_id_L. iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
iDestruct 1 as (Hiys) "Hcsort /=". wp_select; wp_pures; simpl. iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
wp_apply (start_map_service_spec with "Hred [//]"); iIntros (cred) "Hcred". wp_apply (start_chan_proto_spec N (par_map_protocol IZBs IC (curry red) n ));
iIntros (cred) "// Hcred".
{ wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as %_|%Hnil; last first. wp_branch as %_|%Hnil; last first.
{ wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk". { wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
iApply ("HΦ" $! k [] with "[$Hk]"); simpl.
by rewrite /map_reduce /= -Hiys -Hnil. } by rewrite /map_reduce /= -Hiys -Hnil. }
wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures. wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk". wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
wp_apply (par_map_reduce_reduce_server_spec _ _ [] (Some (i, y, w)) with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
with "[$Hk $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
iIntros (zs). rewrite /= gmultiset_elements_empty !right_id. iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
iDestruct 1 as (Hzs) "Hk". wp_pures. iDestruct 1 as (Hzs) "Hk". wp_pures.
iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys. iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
......
...@@ -11,16 +11,16 @@ Definition send_all : val := ...@@ -11,16 +11,16 @@ Definition send_all : val :=
send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs". send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".
Definition recv_all : val := Definition recv_all : val :=
rec: "go" "c" := rec: "go" "c" "ys" :=
if: ~recv "c" then lnil #() else if: ~recv "c" then #() else
let: "x" := recv "c" in let: "x" := recv "c" in
let: "l" := "go" "c" in lcons "x" "l";; "l". "go" "c" "ys";; lcons "x" "ys".
Definition sort_client_fg : val := λ: "cmp" "xs", Definition sort_client_fg : val := λ: "cmp" "xs",
let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
send_all "c" "xs";; send_all "c" "xs";;
send "c" #stop;; send "c" #stop;;
recv_all "c". recv_all "c" "xs".
Section sort_fg_client. Section sort_fg_client.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace). Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
...@@ -29,7 +29,7 @@ Section sort_fg_client. ...@@ -29,7 +29,7 @@ Section sort_fg_client.
Lemma send_all_spec c p xs' l xs : Lemma send_all_spec c p xs' l xs :
{{{ llist I l xs c sort_fg_head_protocol I R xs' <++> p @ N }}} {{{ llist I l xs c sort_fg_head_protocol I R xs' <++> p @ N }}}
send_all c #l send_all c #l
{{{ RET #(); c sort_fg_head_protocol I R (xs' ++ xs) <++> p @ N }}}. {{{ RET #(); llist I l [] c sort_fg_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
Proof. Proof.
iIntros (Φ) "[Hl Hc] HΦ". iIntros (Φ) "[Hl Hc] HΦ".
iInduction xs as [|x xs] "IH" forall (xs'). iInduction xs as [|x xs] "IH" forall (xs').
...@@ -40,40 +40,39 @@ Section sort_fg_client. ...@@ -40,40 +40,39 @@ Section sort_fg_client.
wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L. wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
Qed. Qed.
Lemma recv_all_spec c p xs ys' : Lemma recv_all_spec c p l xs ys' :
Sorted R ys' Sorted R ys'
{{{ c sort_fg_tail_protocol I R xs ys' <++> p @ N }}} {{{ llist I l [] c sort_fg_tail_protocol I R xs ys' <++> p @ N }}}
recv_all c recv_all c #l
{{{ l ys, RET #l; {{{ ys, RET #();
Sorted R (ys' ++ ys) ys' ++ ys xs llist I l ys c p @ N Sorted R (ys' ++ ys) ys' ++ ys xs llist I l ys c p @ N
}}}. }}}.
Proof. Proof.
iIntros (Hsort Φ) "Hc HΦ". iIntros (Hsort Φ) "[Hl Hc] HΦ".
iLöb as "IH" forall (xs ys' Φ Hsort). iLöb as "IH" forall (xs ys' Φ Hsort).
wp_lam. wp_branch as %_ | %Hperm; wp_pures. wp_lam. wp_branch as %_ | %Hperm; wp_pures.
- wp_recv (y v) as (Htl) "HIx". - wp_recv (y v) as (Htl) "HIx".
wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc. wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
iIntros (l ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]". iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures. wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto. iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
- wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl". - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
iApply ("HΦ" $! _ []); rewrite /= right_id_L; by iFrame.
Qed. Qed.
Lemma sort_client_fg_spec cmp l xs : Lemma sort_client_fg_spec cmp l xs :
cmp_spec I R cmp - cmp_spec I R cmp -
{{{ llist I l xs }}} {{{ llist I l xs }}}
sort_client_fg cmp #l sort_client_fg cmp #l
{{{ k ys, RET #k; Sorted R ys ys xs llist I k ys }}}. {{{ ys, RET #(); Sorted R ys ys xs llist I l ys }}}.
Proof. Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam. iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_proto_spec N (sort_fg_protocol I R <++> END)%proto); wp_apply (start_chan_proto_spec N (sort_fg_protocol I R <++> END)%proto);
iIntros (c) "Hc". iIntros (c) "Hc".
{ wp_apply (sort_service_fg_spec N with "Hcmp Hc"); auto. } { wp_apply (sort_service_fg_spec N with "Hcmp Hc"); auto. }
wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "Hc". wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
wp_select. wp_select.
wp_apply (recv_all_spec with "Hc"); auto. wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
iIntros (k ys) "/=". iDestruct 1 as (??) "[Hk _]". iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
iApply "HΦ"; auto with iFrame. iApply "HΦ"; auto with iFrame.
Qed. Qed.
End sort_fg_client. End sort_fg_client.