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.


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).

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).


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.

Lemma prun_iw_app_None p1: forall m1 old p2,
   prun_iw p1 m1 old = None ->
   prun_iw (p1++p2) m1 old = None.

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.

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.

Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2).


Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2.

Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2.

Lemma notIn_incl A (l1 l2: list A) x: incl l1 l2 -> notIn x l2 -> notIn x l1.


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.

Lemma disjoint_sym A (l1 l2: list A): disjoint l1 l2 <-> disjoint l2 l1.


Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2).

Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2).

Lemma disjoint_app_r A (l l1 l2: list A): disjoint l (l1++l2) <-> (disjoint l l1 /\ disjoint l l2).

Lemma disjoint_app_l A (l l1 l2: list A): disjoint (l1++l2) l <-> (disjoint l1 l /\ disjoint l2 l).

Lemma disjoint_incl_r A (l1 l2: list A): incl l1 l2 -> forall l, disjoint l l2 -> disjoint l l1.

Lemma disjoint_incl_l A (l1 l2: list A): incl l1 l2 -> forall l, disjoint l2 l -> disjoint l1 l.


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 }.

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.

Lemma frame_assign_In m1 f m2 x:
   In x f -> frame_assign m1 f m2 x = m2 x.

Lemma frame_assign_notIn m1 f m2 x:
   notIn x f -> frame_assign m1 f m2 x = m1 x.

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.

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.

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).

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.

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).

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').

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'.

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).

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).

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).


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.

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.

Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p.

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.

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)).

End PARALLELI.

End ParallelizablityChecking.

We assume a datatype PseudoRegSet.t refining list R.t

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.




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.


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).

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).

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).

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).

Definition is_parallelizable (p: bblock) := is_pararec p S.empty.

Lemma is_para_correct_aux p: is_parallelizable p = true -> parallelizable p.

Theorem is_parallelizable_correct p:
  is_parallelizable p = true -> forall m om', (prun ge p m om' <-> res_eq om' (run ge p m)).

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.

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).

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).

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.

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.

End PosPseudoRegSet.