Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[NOT READY TO MERGE] Adding support for metrics to the register allocation pass of the compiler #264

Draft
wants to merge 19 commits into
base: master
Choose a base branch
from
Draft

[NOT READY TO MERGE] Adding support for metrics to the register allocation pass of the compiler #264

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
c821320
remove extraneous Search command
pratapsingh1729 May 3, 2022
34513c0
add isReg to FlatImp semantics, other files still broken
pratapsingh1729 May 4, 2022
da28f4a
start fixing other files to add isReg, low-hanging fruit first
pratapsingh1729 May 4, 2022
143d485
fix FlatToRiscvFunctions.v, could be a little tidier though
pratapsingh1729 May 10, 2022
9720664
progress on RegAlloc.v, not done yet
pratapsingh1729 May 16, 2022
d157885
fixed but slow version of regalloc proof; TODO improve performance
pratapsingh1729 Jun 14, 2022
803a137
perf improvements for RegAlloc.v
pratapsingh1729 Jun 21, 2022
276bb7b
fix LowerPipeline.v
pratapsingh1729 Jul 12, 2022
db9c19b
start work on Spilling.v (#1)
pratapsingh1729 Jul 12, 2022
7779d35
Merge branch 'regalloc-metrics' of https://github.com/pratapsingh1729…
pratapsingh1729 Jul 12, 2022
6670dcd
finish Spilling pass except some admits relating to SInteract
pratapsingh1729 Jul 20, 2022
7d1d671
FlattenExpr pass with admits for metrics goals, because bedrock2 sema…
pratapsingh1729 Jul 20, 2022
67d485f
Merge branch 'master' into regalloc-metrics
pratapsingh1729 Jul 20, 2022
cdbdbc0
Merge branch 'regalloc-metrics' of https://github.com/pratapsingh1729…
pratapsingh1729 Jul 20, 2022
402f67f
cleaning up
pratapsingh1729 Jul 20, 2022
ca1bd2a
update submodules
pratapsingh1729 Jul 20, 2022
f8af06b
fix merge issues
pratapsingh1729 Jul 20, 2022
8329197
make compilerExamples/SoftmulCompile.v compatible with new FlatImp.ex…
pratapsingh1729 Jul 21, 2022
24eb5f5
work on spilling pass, current costs for call and interact don't work
pratapsingh1729 Aug 11, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
186 changes: 138 additions & 48 deletions compiler/src/compiler/FlatImp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ Inductive bbinop: Type :=

Section Syntax.
Context {varname: Type}.

Inductive bcond: Type :=
| CondBinary (op: bbinop) (x y: varname)
| CondNez (x: varname)
Expand Down Expand Up @@ -268,13 +268,116 @@ Module exec.
{env_ok: map.ok env}
{ext_spec_ok: ext_spec.ok ext_spec}.

Variable (isReg: varname -> bool).

Variable (e: env).

Local Notation metrics := MetricLog.

(* COQBUG(unification finds Type instead of Prop and fails to downgrade *)
Implicit Types post : trace -> mem -> locals -> metrics -> Prop.


(* Helper functions for computing costs of instructions *)
Definition cost_SLoad x a mc :=
match (isReg x, isReg a) with
| (false, false) => (addMetricInstructions 3 (addMetricLoads 5 (addMetricStores 1 mc)))
| (false, true) => (addMetricInstructions 2 (addMetricLoads 3 (addMetricStores 1 mc)))
| ( true, false) => (addMetricInstructions 2 (addMetricLoads 4 mc))
| ( true, true) => (addMetricInstructions 1 (addMetricLoads 2 mc))
end.

Definition cost_SStore a v mc :=
match (isReg a, isReg v) with
| (false, false) => (addMetricInstructions 3 (addMetricLoads 5 (addMetricStores 1 mc)))
| (false, true) => (addMetricInstructions 2 (addMetricLoads 3 (addMetricStores 1 mc)))
| ( true, false) => (addMetricInstructions 2 (addMetricLoads 3 (addMetricStores 1 mc)))
| ( true, true) => (addMetricInstructions 1 (addMetricLoads 1 (addMetricStores 1 mc)))
end.

Definition cost_SInlinetable x i mc :=
match (isReg x, isReg i) with
| (false, false) => (addMetricInstructions 5 (addMetricLoads 7 (addMetricStores 1 (addMetricJumps 1 mc))))
| (false, true) => (addMetricInstructions 4 (addMetricLoads 5 (addMetricStores 1 (addMetricJumps 1 mc))))
| ( true, false) => (addMetricInstructions 4 (addMetricLoads 6 (addMetricJumps 1 mc)))
| ( true, true) => (addMetricInstructions 3 (addMetricLoads 4 (addMetricJumps 1 mc)))
end.

Definition cost_SStackalloc x mc :=
match isReg x with
| false => (addMetricInstructions 2 (addMetricLoads 2 (addMetricStores 1 mc)))
| true => (addMetricInstructions 1 (addMetricLoads 1 mc))
end.

Definition cost_SLit x mc :=
match isReg x with
| false => (addMetricInstructions 9 (addMetricLoads 9 (addMetricStores 1 mc)))
| true => (addMetricInstructions 8 (addMetricLoads 8 mc))
end.

Definition cost_SOp x y z mc :=
match (isReg x, isReg y, isReg z) with
| (false, false, false) => (addMetricInstructions 5 (addMetricLoads 7 (addMetricStores 1 mc)))
| (false, false, true) | (false, true, false) => (addMetricInstructions 4 (addMetricLoads 5 (addMetricStores 1 mc)))
| (false, true, true) => (addMetricInstructions 3 (addMetricLoads 3 (addMetricStores 1 mc)))
| ( true, false, false) => (addMetricInstructions 4 (addMetricLoads 6 mc))
| ( true, false, true) | ( true, true, false) => (addMetricInstructions 3 (addMetricLoads 4 mc))
| ( true, true, true) => (addMetricInstructions 2 (addMetricLoads 2 mc))
end.

Definition cost_SSet x y mc :=
match (isReg x, isReg y) with
| (false, false) => (addMetricInstructions 3 (addMetricLoads 4 (addMetricStores 1 mc)))
| (false, true) => (addMetricInstructions 2 (addMetricLoads 2 (addMetricStores 1 mc)))
| ( true, false) => (addMetricInstructions 2 (addMetricLoads 3 mc))
| ( true, true) => (addMetricInstructions 1 (addMetricLoads 1 mc))
end.

Definition cost_SIf bcond mc :=
match bcond with
| CondBinary _ x y =>
match (isReg x, isReg y) with
| (false, false) => (addMetricInstructions 4 (addMetricLoads 6 (addMetricJumps 1 mc)))
| (false, true) | ( true, false) => (addMetricInstructions 3 (addMetricLoads 4 (addMetricJumps 1 mc)))
| ( true, true) => (addMetricInstructions 2 (addMetricLoads 2 (addMetricJumps 1 mc)))
end
| CondNez x =>
match isReg x with
| false => (addMetricInstructions 3 (addMetricLoads 4 (addMetricJumps 1 mc)))
| true => (addMetricInstructions 2 (addMetricLoads 2 (addMetricJumps 1 mc)))
end
end.

Definition cost_SLoop_true bcond mc :=
match bcond with
| CondBinary _ x y =>
match (isReg x, isReg y) with
| (false, false) => (addMetricInstructions 4 (addMetricLoads 6 (addMetricJumps 1 mc)))
| (false, true) | ( true, false) => (addMetricInstructions 3 (addMetricLoads 4 (addMetricJumps 1 mc)))
| ( true, true) => (addMetricInstructions 2 (addMetricLoads 2 (addMetricJumps 1 mc)))
end
| CondNez x =>
match isReg x with
| false => (addMetricInstructions 3 (addMetricLoads 4 (addMetricJumps 1 mc)))
| true => (addMetricInstructions 2 (addMetricLoads 2 (addMetricJumps 1 mc)))
end
end.

Definition cost_SLoop_false bcond mc :=
match bcond with
| CondBinary _ x y =>
match (isReg x, isReg y) with
| (false, false) => (addMetricInstructions 3 (addMetricLoads 5 (addMetricJumps 1 mc)))
| (false, true) | ( true, false) => (addMetricInstructions 2 (addMetricLoads 3 (addMetricJumps 1 mc)))
| ( true, true) => (addMetricInstructions 1 (addMetricLoads 1 (addMetricJumps 1 mc)))
end
| CondNez x =>
match isReg x with
| false => (addMetricInstructions 2 (addMetricLoads 3 (addMetricJumps 1 mc)))
| true => (addMetricInstructions 1 (addMetricLoads 1 (addMetricJumps 1 mc)))
end
end.

(* alternative semantics which allow non-determinism *)
Inductive exec:
stmt varname ->
Expand All @@ -290,9 +393,10 @@ Module exec.
exists l', map.putmany_of_list_zip resvars resvals l = Some l' /\
forall m', map.split m' mKeep mReceive ->
post (((mGive, action, argvals), (mReceive, resvals)) :: t) m' l'
(addMetricInstructions 1
(addMetricStores 1
(addMetricLoads 2 mc)))) ->
(addMetricInstructions 100
(addMetricJumps 100
(addMetricStores 100
(addMetricLoads 100 mc))))) ->
exec (SInteract resvars action argvars) t m l mc post
| call: forall t m l mc binds fname args params rets fbody argvs st0 post outcome,
map.get e fname = Some (params, rets, fbody) ->
Expand All @@ -310,72 +414,52 @@ Module exec.
| load: forall t m l mc sz x a o v addr post,
map.get l a = Some addr ->
load sz m (word.add addr (word.of_Z o)) = Some v ->
post t m (map.put l x v)
(addMetricLoads 2
(addMetricInstructions 1 mc)) ->
post t m (map.put l x v) (cost_SLoad x a mc)->
exec (SLoad sz x a o) t m l mc post
| store: forall t m m' mc l sz a o addr v val post,
map.get l a = Some addr ->
map.get l v = Some val ->
store sz m (word.add addr (word.of_Z o)) val = Some m' ->
post t m' l
(addMetricLoads 1
(addMetricInstructions 1
(addMetricStores 1 mc))) ->
post t m' l (cost_SStore a v mc) ->
exec (SStore sz a v o) t m l mc post
| inlinetable: forall sz x table i v index t m l mc post,
(* compiled riscv code uses x as a tmp register and this shouldn't overwrite i *)
x <> i ->
map.get l i = Some index ->
load sz (map.of_list_word table) index = Some v ->
post t m (map.put l x v)
(addMetricLoads 4
(addMetricInstructions 3
(addMetricJumps 1 mc))) ->
post t m (map.put l x v) (cost_SInlinetable x i mc) ->
exec (SInlinetable sz x table i) t m l mc post
| stackalloc: forall t mSmall l mc x n body post,
n mod (bytes_per_word width) = 0 ->
(forall a mStack mCombined,
anybytes a n mStack ->
map.split mCombined mSmall mStack ->
exec body t mCombined (map.put l x a) (addMetricLoads 1 (addMetricInstructions 1 mc))
exec body t mCombined (map.put l x a) (cost_SStackalloc x mc)
(fun t' mCombined' l' mc' =>
exists mSmall' mStack',
anybytes a n mStack' /\
map.split mCombined' mSmall' mStack' /\
post t' mSmall' l' mc')) ->
exec (SStackalloc x n body) t mSmall l mc post
| lit: forall t m l mc x v post,
post t m (map.put l x (word.of_Z v))
(addMetricLoads 8
(addMetricInstructions 8 mc)) ->
post t m (map.put l x (word.of_Z v)) (cost_SLit x mc) ->
exec (SLit x v) t m l mc post
| op: forall t m l mc x op y y' z z' post,
map.get l y = Some y' ->
map.get l z = Some z' ->
post t m (map.put l x (interp_binop op y' z'))
(addMetricLoads 2
(addMetricInstructions 2 mc)) ->
post t m (map.put l x (interp_binop op y' z')) (cost_SOp x y z mc) ->
exec (SOp x op y z) t m l mc post
| set: forall t m l mc x y y' post,
map.get l y = Some y' ->
post t m (map.put l x y')
(addMetricLoads 1
(addMetricInstructions 1 mc)) ->
post t m (map.put l x y') (cost_SSet x y mc) ->
exec (SSet x y) t m l mc post
| if_true: forall t m l mc cond bThen bElse post,
eval_bcond l cond = Some true ->
exec bThen t m l
(addMetricLoads 2
(addMetricInstructions 2
(addMetricJumps 1 mc))) post ->
exec bThen t m l (cost_SIf cond mc) post ->
exec (SIf cond bThen bElse) t m l mc post
| if_false: forall t m l mc cond bThen bElse post,
eval_bcond l cond = Some false ->
exec bElse t m l
(addMetricLoads 2
(addMetricInstructions 2
(addMetricJumps 1 mc))) post ->
exec bElse t m l (cost_SIf cond mc) post ->
exec (SIf cond bThen bElse) t m l mc post
| loop: forall t m l mc cond body1 body2 mid1 mid2 post,
(* This case is carefully crafted in such a way that recursive uses of exec
Expand All @@ -388,20 +472,15 @@ Module exec.
(forall t' m' l' mc',
mid1 t' m' l' mc' ->
eval_bcond l' cond = Some false ->
post t' m' l'
(addMetricLoads 1
(addMetricInstructions 1
(addMetricJumps 1 mc')))) ->
post t' m' l' (cost_SLoop_false cond mc')) ->
(forall t' m' l' mc',
mid1 t' m' l' mc' ->
eval_bcond l' cond = Some true ->
exec body2 t' m' l' mc' mid2) ->
(forall t'' m'' l'' mc'',
mid2 t'' m'' l'' mc'' ->
exec (SLoop body1 cond body2) t'' m'' l''
(addMetricLoads 2
(addMetricInstructions 2
(addMetricJumps 1 mc''))) post) ->
(cost_SLoop_true cond mc'') post) ->
exec (SLoop body1 cond body2) t m l mc post
| seq: forall t m l mc s1 s2 mid post,
exec s1 t m l mc mid ->
Expand Down Expand Up @@ -448,15 +527,15 @@ Module exec.
Lemma loop_cps: forall body1 cond body2 t m l mc post,
exec body1 t m l mc (fun t m l mc => exists b,
eval_bcond l cond = Some b /\
(b = false -> post t m l (addMetricLoads 1 (addMetricInstructions 1 (addMetricJumps 1 mc)))) /\
(b = false -> post t m l (cost_SLoop_false cond mc)) /\
(b = true -> exec body2 t m l mc (fun t m l mc =>
exec (SLoop body1 cond body2) t m l
(addMetricLoads 2 (addMetricInstructions 2 (addMetricJumps 1 mc))) post))) ->
(cost_SLoop_true cond mc) post))) ->
exec (SLoop body1 cond body2) t m l mc post.
Proof.
intros. eapply loop. 1: eapply H. all: cbv beta; intros; simp.
- congruence.
- replace b with false in * by congruence. clear b. eauto.
- replace b with false in * by congruence. clear b. eauto.
- replace b with true in * by congruence. clear b. eauto.
- assumption.
Qed.
Expand Down Expand Up @@ -604,14 +683,16 @@ Section FlatImp2.
{env_ok: map.ok env}
{ext_spec_ok: ext_spec.ok ext_spec}.

Variable (isReg: varname -> bool).

Definition SimState: Type := trace * mem * locals * MetricLog.
Definition SimExec(e: env)(c: stmt varname): SimState -> (SimState -> Prop) -> Prop :=
fun '(t, m, l, mc) post =>
exec e c t m l mc (fun t' m' l' mc' => post (t', m', l', mc')).
exec isReg e c t m l mc (fun t' m' l' mc' => post (t', m', l', mc')).

Lemma modVarsSound: forall e s initialT (initialSt: locals) initialM (initialMc: MetricLog) post,
exec e s initialT initialM initialSt initialMc post ->
exec e s initialT initialM initialSt initialMc
exec isReg e s initialT initialM initialSt initialMc post ->
exec isReg e s initialT initialM initialSt initialMc
(fun finalT finalM finalSt _ => map.only_differ initialSt (modVars s) finalSt).
Proof.
induction 1;
Expand All @@ -631,7 +712,7 @@ Section FlatImp2.
- eapply exec.stackalloc; try eassumption.
intros.
eapply exec.weaken.
+ eapply exec.intersect.
+ eapply exec.intersect; try eassumption.
* eapply H0; eassumption.
* eapply H1; eassumption.
+ simpl. intros. simp.
Expand All @@ -651,7 +732,7 @@ Section FlatImp2.
+ intros. simp. eauto.
+ intros. simp. simpl. map_solver locals_ok.
+ intros. simp. simpl in *.
eapply exec.intersect; [eauto|].
eapply exec.intersect; try eassumption; [eauto|].
eapply exec.weaken.
* eapply H3; eassumption.
* simpl. intros. map_solver locals_ok.
Expand All @@ -669,3 +750,12 @@ Section FlatImp2.
Qed.

End FlatImp2.

Definition isRegZ (var : Z) : bool :=
Z.leb var 31.

Definition isRegStr (var : String.string) : bool :=
String.prefix "reg_" var.



3 changes: 2 additions & 1 deletion compiler/src/compiler/FlatToRiscvCommon.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,8 @@ Section WithParameters.
exists pos, map.get finfo f = Some pos /\ pos mod 4 = 0.

Local Notation stmt := (stmt Z).

Local Notation exec := (exec isRegZ).

(* note: [e_impl_reduced] and [funnames] will shrink one function at a time each time
we enter a new function body, to make sure functions cannot call themselves, while
[e_impl] and [e_pos] remain the same throughout because that's mandated by
Expand Down
Loading