Commit babec8f2 authored by Robbert Krebbers's avatar Robbert Krebbers

Map reduce + Misc tweaks.

parent 4c0c2c53
......@@ -15,3 +15,4 @@ theories/examples/sort_elem.v
theories/examples/loop_sort.v
theories/examples/sort_elem_client.v
theories/examples/mapper.v
theories/examples/map_reduce.v
This diff is collapsed.
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.
From osiris.utils Require Import list spin_lock contribution.
From iris.algebra Require Import gmultiset.
Definition mapper : val :=
......@@ -28,7 +26,7 @@ Definition start_mappers : val :=
Definition mapper_service_loop : val :=
rec: "go" "n" "c" "xs" "ys" :=
if: "n" = #0 then "ys" else
if: recv "c" then
if: recv "c" then (* send item to mapper *)
if: lisnil "xs" then
send "c" #false;;
"go" ("n" - #1) "c" "xs" "ys"
......@@ -36,24 +34,22 @@ Definition mapper_service_loop : val :=
send "c" #true;;
send "c" (lhead "xs");;
"go" "n" "c" (ltail "xs") "ys"
else
else (* receive item from mapper *)
let: "zs" := recv "c" in
"go" "n" "c" "xs" (lapp "zs" "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
let: "c" := start_chan (λ: "c", start_mappers "n" "f" "l" "c") in
mapper_service_loop "n" "c" "xs" (lnil #()).
Class mapperG Σ A `{Countable A} := {
mapper_contributionG :> contributionG Σ (gmultisetUR A);
mapper_lockG :> lockG Σ;
mapper_contributionG :> contributionG Σ (gmultisetUR A)
}.
Section mapper.
Context `{Countable A, Countable B}.
Context `{!heapG Σ, !proto_chanG Σ, mapperG Σ A} (N : namespace).
Context `{Countable A} {B : Type}.
Context `{!heapG Σ, !proto_chanG Σ, !lockG Σ, !mapperG Σ A} (N : namespace).
Context (IA : A val iProp Σ) (IB : B val iProp Σ) (f : A list B).
Local Open Scope nat_scope.
......@@ -77,12 +73,12 @@ Section mapper.
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 :
Lemma mapper_spec γ (vf : val) lk c q :
( x v,
{{{ IA x v }}} ff v {{{ ws, RET (llist ws); [ list] y;w f x;ws, IB y w }}}) -
{{{ IA x v }}} vf v {{{ ws, RET (llist ws); [ list] y;w f x;ws, IB y w }}}) -
{{{ is_lock N lk (mapper_lock_inv γ c)
unlocked N lk q client γ ( : gmultiset A) }}}
mapper ff #lk c
mapper vf #lk c
{{{ RET #(); True }}}.
Proof.
iIntros "#Hf !>" (Φ) "(#Hlk & Hu & Hγ) HΦ". iLöb as "IH".
......@@ -119,12 +115,12 @@ Section mapper.
iIntros "Hu". by wp_apply ("IH" with "[$] [$]").
Qed.
Lemma start_mappers_spec γ (n : nat) (ff : val) lk c q :
Lemma start_mappers_spec γ (n : nat) (vf : val) lk c q :
( x v,
{{{ IA x v }}} ff v {{{ ws, RET (llist ws); [ list] y;w f x;ws, IB y w }}}) -
{{{ IA x v }}} vf v {{{ ws, RET (llist ws); [ list] y;w f x;ws, IB y w }}}) -
{{{ is_lock N lk (mapper_lock_inv γ c) unlocked N lk q
n * client γ (:gmultiset A) }}}
start_mappers #n ff #lk c
client γ (:gmultiset A) ^ n }}}
start_mappers #n vf #lk c
{{{ RET #(); True }}}.
Proof.
iIntros "#Hf !>" (Φ) "(#Hlk & Hu & Hγs) HΦ".
......@@ -137,20 +133,19 @@ Section mapper.
wp_apply ("IH" with "[$] [$] [$]").
Qed.
Lemma mapper_service_loop_spec (n : nat) c vs xs ws X_send xs_recv :
(n = 0 X_send = xs = [])
Lemma mapper_service_loop_spec (n : nat) c vs xs ws X ys :
(n = 0 X = xs = [])
{{{
c mapper_protocol n (X_send : gmultiset A) @ N
([ list] x;v xs;vs, IA x v) ([ list] y;w xs_recv = f;ws, IB y w)
c mapper_protocol n X @ N
([ list] x;v xs;vs, IA x v) ([ list] y;w ys;ws, IB y w)
}}}
mapper_service_loop #n c (llist vs) (llist ws)
{{{ ys ws, RET (llist ws);
ys (xs ++ elements X_send) = f
[ list] y;w ys ++ (xs_recv = f);ws, IB y w
{{{ ys' ws', RET (llist ws');
ys' (xs ++ elements X) = f [ list] y;w ys' ++ ys;ws', IB y w
}}}.
Proof.
iIntros (Hn Φ) "(Hc & HIA & HIB) HΦ".
iLöb as "IH" forall (n vs xs ws X_send xs_recv Hn Φ); wp_rec; wp_pures; simpl.
iLöb as "IH" forall (n vs xs ws X ys Hn Φ); wp_rec; wp_pures; simpl.
case_bool_decide; wp_pures; simplify_eq/=.
{ destruct Hn as [-> ->]; first lia.
iApply ("HΦ" $! []); simpl; auto. }
......@@ -164,28 +159,28 @@ Section mapper.
wp_send with "[$HIAx]".
wp_apply (ltail_spec with "[//]"); iIntros (_).
wp_apply ("IH" with "[] Hc HIA HIB"); first done.
iIntros (ys ws').
iIntros (ys' ws').
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x w) as (HH) "HIBfx".
- wp_recv (x w) as (Hx) "HIBfx".
wp_apply (lapp_spec with "[//]"); iIntros (_).
wp_apply ("IH" $! _ _ _ _ _ (_ :: _) with "[] Hc HIA [HIBfx HIB]"); first done.
wp_apply ("IH" $! _ _ _ _ _ (_ ++ _) with "[] Hc HIA [HIBfx HIB]"); first done.
{ simpl; iFrame. }
iIntros (ys ws'); iDestruct 1 as (Hys) "HIB"; simplify_eq/=.
iApply ("HΦ" $! (ys ++ f x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X_send)
iIntros (ys' ws'); iDestruct 1 as (Hys) "HIB"; simplify_eq/=.
iApply ("HΦ" $! (ys' ++ f x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
rewrite (comm disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
+ by rewrite -assoc_L.
Qed.
Lemma mapper_service_spec (n : nat) (ff : val) vs xs :
Lemma mapper_service_spec (n : nat) (vf : val) vs xs :
0 < n
( x v,
{{{ IA x v }}} ff v {{{ ws, RET (llist ws); [ list] y;w f x;ws, IB y w }}}) -
{{{ IA x v }}} vf v {{{ ws, RET (llist ws); [ list] y;w f x;ws, IB y w }}}) -
{{{ [ list] x;v xs;vs, IA x v }}}
mapper_service #n ff (llist vs)
mapper_service #n vf (llist vs)
{{{ ys ws, RET (llist ws); ys xs = f [ list] y;w ys;ws, IB y w }}}.
Proof.
iIntros (?) "#Hf !>"; iIntros (Φ) "HI HΦ". wp_lam; wp_pures.
......@@ -193,7 +188,7 @@ Section mapper.
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 (contribution_init_pow (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. }
......
......@@ -17,8 +17,7 @@ Definition sort_service : val :=
rec: "go" "c" :=
let: "cmp" := recv "c" in
let: "xs" := recv "c" in
if: llength !"xs" #1 then
send "c" #() else
if: llength !"xs" #1 then send "c" #() else
let: "ys_zs" := lsplit !"xs" in
let: "ys" := ref (Fst "ys_zs") in
let: "zs" := ref (Snd "ys_zs") in
......
......@@ -9,7 +9,7 @@ Definition send_all : val :=
rec: "go" "c" "xs" :=
match: "xs" with
SOME "p" => send "c" #cont;; send "c" (Fst "p");; "go" "c" (Snd "p")
| NONE => send "c" #stop
| NONE => #()
end.
Definition recv_all : val :=
......@@ -23,6 +23,7 @@ Definition sort_elem_client : val :=
let: "c" := start_chan sort_elem_service_top in
send "c" "cmp";;
send_all "c" "xs";;
send "c" #stop;;
recv_all "c".
Section sort_elem_client.
......@@ -32,11 +33,11 @@ Section sort_elem_client.
Lemma send_all_spec c p xs' xs vs :
{{{ c sort_elem_head_protocol I R xs' <++> p @ N [ list] x;v xs;vs, I x v }}}
send_all c (llist vs)
{{{ RET #(); c sort_elem_tail_protocol I R (xs' ++ xs) [] <++> p @ N }}}.
{{{ RET #(); c sort_elem_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
Proof.
iIntros (Φ) "[Hc HI] HΦ".
iInduction xs as [|x xs] "IH" forall (xs' vs); destruct vs as [|v vs]=>//.
{ wp_lam; wp_pures. wp_select. iApply "HΦ". rewrite right_id_L. iFrame. }
{ wp_lam; wp_pures. iApply "HΦ". rewrite right_id_L. iFrame. }
iDestruct "HI" as "[HIxv HI]". wp_lam; wp_pures.
wp_select. wp_send with "[$HIxv]". wp_apply ("IH" with "Hc HI").
by rewrite -assoc_L.
......@@ -77,6 +78,7 @@ Section sort_elem_client.
rewrite /sort_elem_top_protocol.
wp_send (A I R) with "[$Hcmp]".
wp_apply (send_all_spec with "[$HI $Hc]"); iIntros "Hc".
wp_select.
wp_apply (recv_all_spec _ _ _ [] with "[$Hc]"); auto.
iIntros (ys ws) "/=". iDestruct 1 as (??) "[_ HI]".
iApply "HΦ"; auto.
......
......@@ -21,10 +21,10 @@ Typeclasses Opaque client.
Instance: Params (@client) 5.
(** MOVE *)
Fixpoint bi_mult {PROP : bi} (n : nat) (P : PROP) : PROP :=
match n with O => emp | S n => P bi_mult n P end%I.
Arguments bi_mult {_} _ _%I.
Notation "n * P" := (bi_mult n P) : bi_scope.
Fixpoint bi_pow {PROP : bi} (n : nat) (P : PROP) : PROP :=
match n with O => emp | S n => P bi_pow n P end%I.
Arguments bi_pow {_} _ _%I.
Notation "P ^ n" := (bi_pow n P) : bi_scope.
Section contribution.
Context `{contributionG Σ A}.
......@@ -122,7 +122,6 @@ Section contribution.
rewrite -pair_op -Cinl_op Some_op left_id. apply (cancel_local_update _ _ _).
Qed.
Lemma update_client γ n x y x' y' :
(x,y) ~l~> (x',y')
server γ n x - client γ y == server γ n x' client γ y'.
......@@ -141,7 +140,7 @@ Section contribution.
Qed.
(** Derived *)
Lemma contribution_initN n : (|==> γ, server γ n ε n * client γ ε)%I.
Lemma contribution_init_pow n : (|==> γ, server γ n ε (client γ ε)^n)%I.
Proof.
iMod (contribution_init) as (γ) "Hs". iExists γ.
iInduction n as [|n] "IH"; first by iFrame.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment