Lvc.Coherence.AllocationAlgo

Require Import CSet Le Arith.Compare_dec.

Require Import Plus Util Map CMap Status.
Require Import Val Var Env EnvTy IL Annotation Liveness Fresh Sim MoreList.
Require Import Coherence Allocation RenamedApart.

Set Implicit Arguments.

SSA-based register assignment formulated for IL


Section Fresh.
  Variable least_fresh : set var → var.
  Hypothesis least_fresh_spec : ∀ G, least_fresh G ∉ G.

Fixpoint reg_assign (st:stmt) (an: ann (set var)) (ϱ:Map [var, var])
  : status (Map [var, var]) :=
 match st, an with
    | stmtLet x e s, ann1 lv ans ⇒
      let xv := least_fresh (SetConstructs.map (findt ϱ 0) (getAnn ans\{{x}})) in
        reg_assign s ans (ϱ[x<- xv])
    | stmtIf _ s t, ann2 lv ans ant ⇒
      sdo ϱ´ <- reg_assign s ans ϱ;
        reg_assign t ant ϱ´
    | stmtApp _ _, ann0 _ ⇒ Success ϱ
    | stmtReturn _, ann0 _ ⇒ Success ϱ
    | stmtExtern x f Y s, ann1 lv ans ⇒
      let xv := least_fresh (SetConstructs.map (findt ϱ 0) (getAnn ans\{{x}})) in
      reg_assign s ans (ϱ[x<- xv])
    | stmtFun Z s t, ann2 _ ans ant ⇒
      let Z´ := fresh_list least_fresh (SetConstructs.map (findt ϱ 0) (getAnn ans\of_list Z)) (length Z) in
      sdo ϱ´ <- reg_assign s ans (ϱ[Z <-- Z´]);
        reg_assign t ant ϱ´
    | _, _ ⇒ Error "reg_assign: Annotation mismatch"
 end.

The algorithm only changes bound variables in the mapping ϱ

Lemma reg_assign_renamedApart_agree´ i s al ϱ ϱ´ LV alv G
      (sd:renamedApart s al)
      (LS:live_sound i LV s alv)
      (allocOK:reg_assign s alv ϱ = Success ϱ´)
: agree_on eq (G \ snd (getAnn al)) (findt ϱ 0) (findt ϱ´ 0).

Lemma reg_assign_renamedApart_agree i s al ϱ ϱ´ LV alv
      (sd:renamedApart s al)
      (LS:live_sound i LV s alv)
      (allocOK:reg_assign s alv ϱ = Success ϱ´)
: agree_on eq (fst (getAnn al)) (findt ϱ 0) (findt ϱ´ 0).

the algorithm produces a locally injective renaming


Lemma reg_assign_correct (ϱ:Map [var,var]) LV s alv ϱ´ al
      (LS:live_sound FunctionalAndImperative LV s alv)
      (inj:injective_on (getAnn alv) (findt ϱ 0))
      (allocOK:reg_assign s alv ϱ = Success ϱ´)
      (incl:getAnn alv ⊆ fst (getAnn al))
      (sd:renamedApart s al)
: locally_inj (findt ϱ´ 0) s alv.

Require Import Restrict RenamedApart_Liveness.

Theorem 8 from the paper.

One could prove this theorem directly by induction, however, we exploit that under the assumption of the theorem, the liveness information alv is also sound for functional liveness and we can thus rely on theorem reg_assign_correct above, which we did prove by induction.

Lemma reg_assign_correct´ s ang ϱ ϱ´ (alv:ann (set var)) Lv
  : renamedApart s ang
  → live_sound Imperative Lv s alv
  → bounded (live_globals Lv) (fst (getAnn ang))
  → ann_R Subset1 alv ang
  → LabelsDefined.noUnreachableCode s
  → injective_on (getAnn alv) (findt ϱ 0)
  → reg_assign s alv ϱ = Success ϱ´
  → locally_inj (findt ϱ´ 0) s alv.

Require Import LabelsDefined.

Bound on the number of registers used


Fixpoint largest_live_set (a:ann (set var)) : set var :=
  match a with
    | ann0 gamma ⇒ gamma
    | ann1 gamma a ⇒ max_set gamma (largest_live_set a)
    | ann2 gamma a b ⇒ max_set gamma (max_set (largest_live_set a) (largest_live_set b))
  end.

Fixpoint size_of_largest_live_set (a:ann (set var)) : nat :=
  match a with
    | ann0 gamma ⇒ SetInterface.cardinal gamma
    | ann1 gamma a ⇒ max (SetInterface.cardinal gamma) (size_of_largest_live_set a)
    | ann2 gamma a b ⇒ max (SetInterface.cardinal gamma)
                       (max (size_of_largest_live_set a) (size_of_largest_live_set b))
  end.

Lemma size_of_largest_live_set_live_set al
: SetInterface.cardinal (getAnn al) ≤ size_of_largest_live_set al.

Hint Resolve least_fresh_spec.

Hypothesis least_fresh_small : ∀ G : set var, least_fresh G ≤ SetInterface.cardinal G.

Lemma reg_assign_assignment_small (ϱ:Map [var,var]) LV s alv ϱ´ al n
      (LS:live_sound Functional LV s alv)
      (allocOK:reg_assign s alv ϱ = Success ϱ´)
      (incl:getAnn alv ⊆ fst (getAnn al))
      (sd:renamedApart s al)
      (up:lookup_set (findt ϱ 0) (fst (getAnn al)) ⊆ vars_up_to n)
: lookup_set (findt ϱ´ 0) (snd (getAnn al)) ⊆ vars_up_to (max (size_of_largest_live_set alv) n).

Theorem 8 from the paper.

One could prove this theorem directly by induction, however, we exploit that under the assumption of the theorem, the liveness information alv is also sound for functional liveness and we can thus rely on theorem reg_assign_assignment_small above, which we did prove by induction.

Lemma reg_assign_assignment_small´ s ang ϱ ϱ´ (alv:ann (set var)) Lv n
  : renamedApart s ang
  → live_sound Imperative Lv s alv
  → bounded (live_globals Lv) (fst (getAnn ang))
  → ann_R Subset1 alv ang
  → LabelsDefined.noUnreachableCode s
  → reg_assign s alv ϱ = Success ϱ´
  → lookup_set (findt ϱ 0) (fst (getAnn ang)) ⊆ vars_up_to n
  → lookup_set (findt ϱ´ 0) (fst (getAnn ang) ∪ snd (getAnn ang)) ⊆ vars_up_to (max (size_of_largest_live_set alv) n).

End Fresh.