Theory Sepref_Parallel
section ‹Automatic Refinement to Parallel Execution›
theory Sepref_Parallel
imports Sepref_Tool
begin
text ‹Abstractly, we define an annotation, that maps to sequnetial execution›
definition "nres_par f g x y ≡ do { r1←f x; r2←g y; RETURN (r1,r2) }"
subsection ‹Setup Boilerplate›
text ‹Boilerplate required by the IRF to set up higher-order combinator›
lemma nres_par_arity[sepref_monadify_arity]:
"nres_par ≡ λ⇩2f g x y. SP nres_par $ (λ⇩2x. f$x) $ (λ⇩2y. g$y) $ x $ y"
by (simp_all)
lemma nres_par_comb[sepref_monadify_comb]:
"nres_par$f$g$x$y ≡
Refine_Basic.bind$(EVAL$x)$(λ⇩2x. Refine_Basic.bind$(EVAL$y)$(λ⇩2y.
(SP nres_par$f$g$x$y)))"
by (simp_all)
lemma nres_par_id[id_rules]:
"nres_par ::⇩i TYPE(('a ⇒ 'b nres) ⇒ ('c ⇒ 'd nres) ⇒ 'a ⇒ 'c ⇒ ('b × 'd) nres)"
by simp
lemma nres_par_pw[refine_pw_simps]:
"nofail (nres_par f g x y) = (nofail (f x) ∧ ((∃xa. inres (f x) xa) ⟶ nofail (g y)))"
"inres (nres_par f g x y) r ⟷ (nofail (f x) ⟶
(∃ya. inres (f x) ya ∧ (nofail (g y) ⟶ (∃yb. inres (g y) yb ∧ (ya, yb) = r))))"
unfolding nres_par_def
by (simp_all add: refine_pw_simps)
lemma nres_par_vcg[refine_vcg]:
assumes "f x ≤ SPEC (λr⇩1. g y ≤ SPEC (λr⇩2. Φ (r⇩1,r⇩2)))"
shows "nres_par f g x y ≤ SPEC Φ"
using assms by (auto simp: refine_pw_simps pw_le_iff nres_par_def)
lemma nres_par_refine[refine]:
assumes "f x ≤ ⇓Rx (f' x')"
assumes "g y ≤ ⇓Ry (g' y')"
assumes "⋀rx rx' ry ry'. (rx,rx')∈Rx ⟹ (ry,ry')∈Ry ⟹ ((rx,ry), (rx',ry'))∈R"
shows "nres_par f g x y ≤⇓R (nres_par f' g' x' y')"
using assms
by (simp add: refine_pw_simps pw_le_iff nres_par_def; blast)
lemma nres_par_mono[refine_mono]:
assumes "⋀x. f x ≤ f' x"
assumes "⋀y. g y ≤ g' y"
shows "nres_par f g x y ≤ nres_par f' g' x y"
using assms
by (simp add: refine_pw_simps pw_le_iff nres_par_def; blast)
lemma nres_par_flat_mono[refine_mono]:
assumes "⋀x. flat_ge (f x) (f' x)"
assumes "⋀y. flat_ge (g y) (g' y)"
shows "flat_ge (nres_par f g x y) (nres_par f' g' x y)"
using assms
by (simp add: refine_pw_simps pw_flat_ge_iff nres_par_def; blast)
subsection ‹Refinement Rule›
text ‹Refinement rule from annotation to actual parallel execution›
lemma ht_llc_par:
assumes "llvm_htriple P⇩1 (m⇩1 x⇩1) Q⇩1"
assumes "llvm_htriple P⇩2 (m⇩2 x⇩2) Q⇩2"
shows "llvm_htriple (P⇩1**P⇩2) (llc_par m⇩1 m⇩2 x⇩1 x⇩2) (λ(r⇩1,r⇩2). Q⇩1 r⇩1 ** Q⇩2 r⇩2)"
unfolding llc_par_def
supply [vcg_rules] = ht_par[OF assms]
by (vcg)
lemma hnr_nres_par_aux:
assumes A: "hn_refine (Ax) (fi xi) (Ax') Rx CP⇩1 (f x)"
assumes B: "hn_refine (Ay) (gi yi) (Ay') Ry CP⇩2 (g y)"
shows "hn_refine (Ax ** Ay) (llc_par fi gi xi yi) (Ax' ** Ay') (Rx×⇩aRy) (λ(rxi,ryi). CP⇩1 rxi ∧ CP⇩2 ryi) (nres_par f g x y)"
proof -
note [vcg_rules] = ht_llc_par[where m⇩1=fi and m⇩2=gi, OF A[THEN hn_refineD] B[THEN hn_refineD]]
from A[THEN hn_refineD] have
NSUCCA: "∃r. inres (f x) r" if "realizable Ax"
using that
apply (cases "f x ≠ SUCCEED")
subgoal by (auto simp: refine_pw_simps pw_eq_iff)
apply (clarsimp simp: htriple_false)
done
show ?thesis
apply sepref_to_hoare
apply (rule htriple_realizable_preI; drule realizable_conjD; clarify)
supply [simp] = refine_pw_simps NSUCCA inres_def[symmetric]
apply (vcg)
done
qed
lemma hnr_nres_par[sepref_comb_rules]:
assumes FR: "P ⊢ hn_ctxt Ax x xi ** hn_ctxt Ay y yi ** F"
assumes A: "hn_refine (hn_ctxt Ax x xi) (fi xi) Ax' Rx CP⇩1 (f x)"
assumes B: "hn_refine (hn_ctxt Ay y yi) (gi yi) Ay' Ry CP⇩2 (g y)"
shows "hn_refine
P
(llc_par fi gi xi yi)
(Ax' ** Ay' ** F) (Rx×⇩aRy) (λ(rxi,ryi). CP⇩1 rxi ∧ CP⇩2 ryi)
(nres_par$(λ⇩2x. f x)$(λ⇩2y. g y)$x$y)"
apply (rule hn_refine_cons_post)
unfolding autoref_tag_defs PROTECT2_def
apply (rule hn_refine_frame[OF hnr_nres_par_aux, where F=F])
apply fact
apply fact
subgoal using FR unfolding hn_ctxt_def by (auto simp: algebra_simps)
subgoal unfolding hn_ctxt_def by (auto simp: algebra_simps)
done
end