Parallel Semantics of Abstract Basic Blocks and parallelizability test.
Require Setoid.
Require Export AbstractBasicBlocksDef.
Require Import List.
Import ListNotations.
Local Open Scope list_scope.
Require Import Sorting.Permutation.
Require Import Bool.
Local Open Scope lazy_bool_scope.
Definition of the parallel semantics
Module ParallelSemantics (
L:
SeqLanguage).
Export L.
Local Open Scope list.
Section PARALLEL.
Variable ge:
genv.
Fixpoint inst_prun (
i:
inst) (
m tmp old:
mem):
option mem :=
match i with
|
nil =>
Some m
| (
x,
e)::
i' =>
match exp_eval ge e tmp old with
|
Some v' =>
inst_prun i' (
assign m x v') (
assign tmp x v')
old
|
None =>
None
end
end.
Lemma inst_run_prun i:
forall m old,
inst_run ge i m old =
inst_prun i m m old.
Proof.
induction i as [|[
y e]
i'];
cbn;
auto.
intros m old;
destruct (
exp_eval ge e m old);
cbn;
auto.
Qed.
Fixpoint prun_iw (
p:
bblock)
m old:
option mem :=
match p with
|
nil =>
Some m
|
i::
p' =>
match inst_prun i m old old with
|
Some m1 =>
prun_iw p' m1 old
|
None =>
None
end
end.
Definition prun (
p:
bblock)
m (
om:
option mem) :=
exists p',
res_eq om (
prun_iw p' m m) /\
Permutation p p'.
Lemma inst_prun_equiv i old:
forall m1 m2 tmp,
(
forall x,
m1 x =
m2 x) ->
res_eq (
inst_prun i m1 tmp old) (
inst_prun i m2 tmp old).
Proof.
induction i as [|[
x e]
i'];
cbn;
eauto.
intros m1 m2 tmp H;
destruct (
exp_eval ge e tmp old);
cbn;
auto.
eapply IHi';
unfold assign.
intros;
destruct (
R.eq_dec x x0);
auto.
Qed.
Lemma prun_iw_equiv p:
forall m1 m2 old,
(
forall x,
m1 x =
m2 x) ->
res_eq (
prun_iw p m1 old) (
prun_iw p m2 old).
Proof.
induction p as [|
i p'];
cbn;
eauto.
-
intros m1 m2 old H.
generalize (
inst_prun_equiv i old m1 m2 old H);
destruct (
inst_prun i m1 old old);
cbn.
+
intros (
m3 &
H3 &
H4);
rewrite H3;
cbn;
eauto.
+
intros H1;
rewrite H1;
cbn;
auto.
Qed.
Lemma prun_iw_app p1:
forall m1 old p2,
prun_iw (
p1++
p2)
m1 old =
match prun_iw p1 m1 old with
|
Some m2 =>
prun_iw p2 m2 old
|
None =>
None
end.
Proof.
induction p1;
cbn;
try congruence.
intros;
destruct (
inst_prun _ _ _);
cbn;
auto.
Qed.
Lemma prun_iw_app_None p1:
forall m1 old p2,
prun_iw p1 m1 old =
None ->
prun_iw (
p1++
p2)
m1 old =
None.
Proof.
intros m1 old p2 H;
rewrite prun_iw_app.
rewrite H;
auto.
Qed.
Lemma prun_iw_app_Some p1:
forall m1 old m2 p2,
prun_iw p1 m1 old =
Some m2 ->
prun_iw (
p1++
p2)
m1 old =
prun_iw p2 m2 old.
Proof.
intros m1 old m2 p2 H;
rewrite prun_iw_app.
rewrite H;
auto.
Qed.
End PARALLEL.
End ParallelSemantics.
Fixpoint notIn {
A} (
x:
A) (
l:
list A):
Prop :=
match l with
|
nil =>
True
|
a::
l' =>
x <>
a /\
notIn x l'
end.
Lemma notIn_iff A (
x:
A)
l: (~
List.In x l) <->
notIn x l.
Proof.
induction l; cbn; intuition.
Qed.
Lemma notIn_app A (
x:
A)
l1:
forall l2,
notIn x (
l1++
l2) <-> (
notIn x l1 /\
notIn x l2).
Proof.
induction l1; cbn.
- intuition.
- intros; rewrite IHl1. intuition.
Qed.
Lemma In_Permutation A (
l1 l2:
list A):
Permutation l1 l2 ->
forall x,
In x l1 ->
In x l2.
Proof.
induction 1; cbn; intuition.
Qed.
Lemma Permutation_incl A (
l1 l2:
list A):
Permutation l1 l2 ->
incl l1 l2.
Proof.
Lemma notIn_incl A (
l1 l2:
list A)
x:
incl l1 l2 ->
notIn x l2 ->
notIn x l1.
Proof.
Definition disjoint {
A:
Type} (
l l':
list A) :
Prop :=
forall x,
In x l ->
notIn x l'.
Lemma disjoint_sym_imp A (
l1 l2:
list A):
disjoint l1 l2 ->
disjoint l2 l1.
Proof.
unfold disjoint.
intros H x H1.
generalize (
H x).
rewrite <- !
notIn_iff.
intuition.
Qed.
Lemma disjoint_sym A (
l1 l2:
list A):
disjoint l1 l2 <->
disjoint l2 l1.
Proof.
Lemma disjoint_cons_l A (
x:
A) (
l1 l2:
list A):
disjoint (
x::
l1)
l2 <-> (
notIn x l2) /\ (
disjoint l1 l2).
Proof.
unfold disjoint.
cbn;
intuition subst;
auto.
Qed.
Lemma disjoint_cons_r A (
x:
A) (
l1 l2:
list A):
disjoint l1 (
x::
l2) <-> (
notIn x l1) /\ (
disjoint l1 l2).
Proof.
Lemma disjoint_app_r A (
l l1 l2:
list A):
disjoint l (
l1++
l2) <-> (
disjoint l l1 /\
disjoint l l2).
Proof.
Lemma disjoint_app_l A (
l l1 l2:
list A):
disjoint (
l1++
l2)
l <-> (
disjoint l1 l /\
disjoint l2 l).
Proof.
Lemma disjoint_incl_r A (
l1 l2:
list A):
incl l1 l2 ->
forall l,
disjoint l l2 ->
disjoint l l1.
Proof.
Lemma disjoint_incl_l A (
l1 l2:
list A):
incl l1 l2 ->
forall l,
disjoint l2 l ->
disjoint l1 l.
Proof.
Module ParallelizablityChecking (
L:
SeqLanguage).
Include ParallelSemantics L.
Section PARALLELI.
Variable ge:
genv.
Preliminary notions on frames
Lemma notIn_dec (
x:
R.t)
l : {
notIn x l } + {
In x l }.
Proof.
Fixpoint frame_assign m1 (
f:
list R.t)
m2 :=
match f with
|
nil =>
m1
|
x::
f' =>
frame_assign (
assign m1 x (
m2 x))
f' m2
end.
Lemma frame_assign_def f:
forall m1 m2 x,
frame_assign m1 f m2 x =
if notIn_dec x f then m1 x else m2 x.
Proof.
induction f as [|
y f] ;
cbn;
auto.
-
intros;
destruct (
notIn_dec x []);
cbn in *;
tauto.
-
intros;
rewrite IHf;
destruct (
notIn_dec x (
y::
f));
cbn in *.
+
destruct (
notIn_dec x f);
cbn in *;
intuition.
rewrite assign_diff;
auto.
rewrite <-
notIn_iff in *;
intuition.
+
destruct (
notIn_dec x f);
cbn in *;
intuition subst.
rewrite assign_eq;
auto.
rewrite <-
notIn_iff in *;
intuition.
Qed.
Lemma frame_assign_In m1 f m2 x:
In x f ->
frame_assign m1 f m2 x =
m2 x.
Proof.
Lemma frame_assign_notIn m1 f m2 x:
notIn x f ->
frame_assign m1 f m2 x =
m1 x.
Proof.
Definition frame_eq (
frame:
R.t ->
Prop) (
om1 om2:
option mem):
Prop :=
match om1 with
|
Some m1 =>
exists m2,
om2 =
Some m2 /\
forall x, (
frame x) ->
m1 x =
m2 x
|
None =>
om2 =
None
end.
Lemma frame_eq_list_split f1 (
f2:
R.t ->
Prop)
om1 om2:
frame_eq (
fun x =>
In x f1)
om1 om2 ->
(
forall m1 m2 x,
om1 =
Some m1 ->
om2 =
Some m2 ->
f2 x ->
notIn x f1 ->
m1 x =
m2 x) ->
frame_eq f2 om1 om2.
Proof.
unfold frame_eq;
destruct om1 as [
m1 | ];
cbn;
auto.
intros (
m2 &
H0 &
H1);
subst.
intros H.
eexists;
intuition eauto.
destruct (
notIn_dec x f1);
auto.
Qed.
Writing frames
Fixpoint inst_wframe(
i:
inst):
list R.t :=
match i with
|
nil =>
nil
|
a::
i' => (
fst a)::(
inst_wframe i')
end.
Lemma inst_wframe_correct i m' old:
forall m tmp,
inst_prun ge i m tmp old =
Some m' ->
forall x,
notIn x (
inst_wframe i) ->
m' x =
m x.
Proof.
induction i as [|[
y e]
i'];
cbn.
-
intros m tmp H x H0;
inversion_clear H;
auto.
-
intros m tmp H x (
H1 &
H2);
destruct (
exp_eval ge e tmp old);
cbn;
try congruence.
replace (
m x)
with (
assign m y v x);
eauto.
rewrite assign_diff;
auto.
Qed.
Lemma inst_prun_fequiv i old:
forall m1 m2 tmp,
frame_eq (
fun x =>
In x (
inst_wframe i)) (
inst_prun ge i m1 tmp old) (
inst_prun ge i m2 tmp old).
Proof.
Lemma inst_prun_None i m1 m2 tmp old:
inst_prun ge i m1 tmp old =
None ->
inst_prun ge i m2 tmp old =
None.
Proof.
intros H;
generalize (
inst_prun_fequiv i old m1 m2 tmp).
rewrite H;
cbn;
auto.
Qed.
Lemma inst_prun_Some i m1 m2 tmp old m1':
inst_prun ge i m1 tmp old =
Some m1' ->
res_eq (
Some (
frame_assign m2 (
inst_wframe i)
m1')) (
inst_prun ge i m2 tmp old).
Proof.
Fixpoint bblock_wframe(
p:
bblock):
list R.t :=
match p with
|
nil =>
nil
|
i::
p' => (
inst_wframe i)++(
bblock_wframe p')
end.
Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm:
core.
Lemma bblock_wframe_Permutation p p':
Permutation p p' ->
Permutation (
bblock_wframe p) (
bblock_wframe p').
Proof.
Checking that parallel semantics is deterministic
Fixpoint is_det (
p:
bblock):
Prop :=
match p with
|
nil =>
True
|
i::
p' =>
disjoint (
inst_wframe i) (
bblock_wframe p')
/\
is_det p'
end.
Lemma is_det_Permutation p p':
Permutation p p' ->
is_det p ->
is_det p'.
Proof.
Theorem is_det_correct p p':
Permutation p p' ->
is_det p ->
forall m old,
res_eq (
prun_iw ge p m old) (
prun_iw ge p' m old).
Proof.
Standard Frames
Fixpoint exp_frame (
e:
exp):
list R.t :=
match e with
|
PReg x =>
x::
nil
|
Op o le =>
list_exp_frame le
|
Old e =>
exp_frame e
end
with list_exp_frame (
le:
list_exp):
list R.t :=
match le with
|
Enil =>
nil
|
Econs e le' =>
exp_frame e ++
list_exp_frame le'
|
LOld le =>
list_exp_frame le
end.
Lemma exp_frame_correct e old1 old2:
(
forall x,
In x (
exp_frame e) ->
old1 x =
old2 x) ->
forall m1 m2, (
forall x,
In x (
exp_frame e) ->
m1 x =
m2 x) ->
(
exp_eval ge e m1 old1)=(
exp_eval ge e m2 old2).
Proof.
induction e using exp_mut with (
P0:=
fun l => (
forall x,
In x (
list_exp_frame l) ->
old1 x =
old2 x) ->
forall m1 m2, (
forall x,
In x (
list_exp_frame l) ->
m1 x =
m2 x) ->
(
list_exp_eval ge l m1 old1)=(
list_exp_eval ge l m2 old2));
cbn;
auto.
-
intros H1 m1 m2 H2;
rewrite H2;
auto.
-
intros H1 m1 m2 H2;
erewrite IHe;
eauto.
-
intros H1 m1 m2 H2;
erewrite IHe,
IHe0;
eauto;
intros; (
eapply H1 ||
eapply H2);
rewrite in_app_iff;
auto.
Qed.
Fixpoint inst_frame (
i:
inst):
list R.t :=
match i with
|
nil =>
nil
|
a::
i' => (
fst a)::(
exp_frame (
snd a) ++
inst_frame i')
end.
Lemma inst_wframe_frame i x:
In x (
inst_wframe i) ->
In x (
inst_frame i).
Proof.
induction i as [ | [y e] i']; cbn; intuition.
Qed.
Lemma inst_frame_correct i wframe old1 old2:
forall m tmp1 tmp2,
(
disjoint (
inst_frame i)
wframe) ->
(
forall x,
notIn x wframe ->
old1 x =
old2 x) ->
(
forall x,
notIn x wframe ->
tmp1 x =
tmp2 x) ->
inst_prun ge i m tmp1 old1 =
inst_prun ge i m tmp2 old2.
Proof.
Parallelizability
Fixpoint pararec (
p:
bblock) (
wframe:
list R.t):
Prop :=
match p with
|
nil =>
True
|
i::
p' =>
disjoint (
inst_frame i)
wframe
/\
pararec p' ((
inst_wframe i) ++
wframe)
end.
Lemma pararec_disjoint (
p:
bblock):
forall wframe,
pararec p wframe ->
disjoint (
bblock_wframe p)
wframe.
Proof.
Lemma pararec_det p:
forall wframe,
pararec p wframe ->
is_det p.
Proof.
Lemma pararec_correct p old:
forall wframe m,
pararec p wframe ->
(
forall x,
notIn x wframe ->
m x =
old x) ->
run ge p m =
prun_iw ge p m old.
Proof.
Definition parallelizable (
p:
bblock) :=
pararec p nil.
Theorem parallelizable_correct p m om':
parallelizable p -> (
prun ge p m om' <->
res_eq om' (
run ge p m)).
Proof.
End PARALLELI.
End ParallelizablityChecking.
We assume a datatype PseudoRegSet.t refining list R.t
This data-refinement is given by an abstract "invariant" match_frame below,
preserved by the following operations.
Module Type PseudoRegSet.
Declare Module R:
PseudoRegisters.
Parameter t:
Type.
Parameter match_frame:
t -> (
list R.t) ->
Prop.
Parameter empty:
t.
Parameter empty_match_frame:
match_frame empty nil.
Parameter add:
R.t ->
t ->
t.
Parameter add_match_frame:
forall s x l,
match_frame s l ->
match_frame (
add x s) (
x::
l).
Parameter union:
t ->
t ->
t.
Parameter union_match_frame:
forall s1 s2 l1 l2,
match_frame s1 l1 ->
match_frame s2 l2 ->
match_frame (
union s1 s2) (
l1++
l2).
Parameter is_disjoint:
t ->
t ->
bool.
Parameter is_disjoint_match_frame:
forall s1 s2 l1 l2,
match_frame s1 l1 ->
match_frame s2 l2 -> (
is_disjoint s1 s2)=
true ->
disjoint l1 l2.
End PseudoRegSet.
Lemma lazy_andb_bool_true (
b1 b2:
bool):
b1 &&&
b2 =
true <->
b1 =
true /\
b2 =
true.
Proof.
destruct b1, b2; intuition.
Qed.
Module ParallelChecks (
L:
SeqLanguage) (
S:
PseudoRegSet with Module R:=
L.LP.R).
Include ParallelizablityChecking L.
Section PARALLEL2.
Variable ge:
genv.
Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame:
core.
Now, refinement of each operation toward parallelizable
Fixpoint inst_wsframe(
i:
inst):
S.t :=
match i with
|
nil =>
S.empty
|
a::
i' =>
S.add (
fst a) (
inst_wsframe i')
end.
Lemma inst_wsframe_correct i:
S.match_frame (
inst_wsframe i) (
inst_wframe i).
Proof.
induction i; cbn; auto.
Qed.
Fixpoint exp_sframe (
e:
exp):
S.t :=
match e with
|
PReg x =>
S.add x S.empty
|
Op o le =>
list_exp_sframe le
|
Old e =>
exp_sframe e
end
with list_exp_sframe (
le:
list_exp):
S.t :=
match le with
|
Enil =>
S.empty
|
Econs e le' =>
S.union (
exp_sframe e) (
list_exp_sframe le')
|
LOld le =>
list_exp_sframe le
end.
Lemma exp_sframe_correct e:
S.match_frame (
exp_sframe e) (
exp_frame e).
Proof.
Fixpoint inst_sframe (
i:
inst):
S.t :=
match i with
|
nil =>
S.empty
|
a::
i' =>
S.add (
fst a) (
S.union (
exp_sframe (
snd a)) (
inst_sframe i'))
end.
Local Hint Resolve exp_sframe_correct:
core.
Lemma inst_sframe_correct i:
S.match_frame (
inst_sframe i) (
inst_frame i).
Proof.
induction i as [|[y e] i']; cbn; auto.
Qed.
Local Hint Resolve inst_wsframe_correct inst_sframe_correct:
core.
Fixpoint is_pararec (
p:
bblock) (
wsframe:
S.t):
bool :=
match p with
|
nil =>
true
|
i::
p' =>
S.is_disjoint (
inst_sframe i)
wsframe
&&&
is_pararec p' (
S.union (
inst_wsframe i)
wsframe)
end.
Lemma is_pararec_correct (
p:
bblock):
forall s l,
S.match_frame s l -> (
is_pararec p s)=
true -> (
pararec p l).
Proof.
induction p;
cbn;
auto.
intros s l H1 H2;
rewrite lazy_andb_bool_true in H2.
destruct H2 as [
H2 H3].
constructor 1;
eauto.
Qed.
Definition is_parallelizable (
p:
bblock) :=
is_pararec p S.empty.
Lemma is_para_correct_aux p:
is_parallelizable p =
true ->
parallelizable p.
Proof.
Theorem is_parallelizable_correct p:
is_parallelizable p =
true ->
forall m om', (
prun ge p m om' <->
res_eq om' (
run ge p m)).
Proof.
End PARALLEL2.
End ParallelChecks.
Implementing the datatype PosPseudoRegSet.t refining list R.t
Require Import PArith.
Require Import MSets.MSetPositive.
Module PosPseudoRegSet <:
PseudoRegSet with Module R:=
Pos.
Module R:=
Pos.
Definition t:=
PositiveSet.t.
Definition match_frame (
s:
t) (
l:
list R.t):
Prop
:=
forall x,
PositiveSet.In x s <->
In x l.
Definition empty:=
PositiveSet.empty.
Lemma empty_match_frame:
match_frame empty nil.
Proof.
Definition add:
R.t ->
t ->
t :=
PositiveSet.add.
Lemma add_match_frame:
forall s x l,
match_frame s l ->
match_frame (
add x s) (
x::
l).
Proof.
Definition union:
t ->
t ->
t :=
PositiveSet.union.
Lemma union_match_frame:
forall s1 s2 l1 l2,
match_frame s1 l1 ->
match_frame s2 l2 ->
match_frame (
union s1 s2) (
l1++
l2).
Proof.
Fixpoint is_disjoint (
s s':
PositiveSet.t) :
bool :=
match s with
|
PositiveSet.Leaf =>
true
|
PositiveSet.Node l o r =>
match s' with
|
PositiveSet.Leaf =>
true
|
PositiveSet.Node l' o' r' =>
if (
o &&&
o')
then false else (
is_disjoint l l' &&&
is_disjoint r r')
end
end.
Lemma is_disjoint_spec_true s:
forall s',
is_disjoint s s' =
true ->
forall x,
PositiveSet.In x s ->
PositiveSet.In x s' ->
False.
Proof.
unfold PositiveSet.In;
induction s as [ |
l IHl o r IHr];
cbn;
try discriminate.
destruct s' as [|
l' o' r'];
cbn;
try discriminate.
intros X.
assert (
H: ~(
o =
true /\
o'=
true) /\
is_disjoint l l' =
true /\
is_disjoint r r'=
true).
{
destruct o,
o', (
is_disjoint l l'), (
is_disjoint r r');
cbn in X;
intuition. }
clear X;
destruct H as (
H &
H1 &
H2).
destruct x as [
i|
i|];
cbn;
eauto.
Qed.
Lemma is_disjoint_match_frame:
forall s1 s2 l1 l2,
match_frame s1 l1 ->
match_frame s2 l2 -> (
is_disjoint s1 s2)=
true ->
disjoint l1 l2.
Proof.
End PosPseudoRegSet.