[3014] | 1 | include "ERTL/liveness.ma". |
---|
[1127] | 2 | |
---|
[1229] | 3 | inductive decision: Type[0] ≝ |
---|
[1232] | 4 | | decision_spill: nat → decision |
---|
[1229] | 5 | | decision_colour: Register → decision. |
---|
| 6 | |
---|
[3255] | 7 | definition DeqRegister : DeqSet ≝ |
---|
| 8 | mk_DeqSet Register eq_Register ?. |
---|
| 9 | #x #y % [2: #EQ destruct cases y % ] |
---|
| 10 | cases x -x try (cases y -y normalize #EQ destruct %) |
---|
| 11 | qed. |
---|
| 12 | |
---|
| 13 | unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister. |
---|
| 14 | |
---|
| 15 | definition is_src_of_move : |
---|
| 16 | ∀globals.joint_statement ERTL globals → vertex → bool ≝ |
---|
| 17 | λglobals,s,v. |
---|
| 18 | match s with |
---|
| 19 | [ sequential s _ ⇒ |
---|
| 20 | match s with |
---|
| 21 | [ step_seq s ⇒ |
---|
| 22 | match s with |
---|
| 23 | [ MOVE pr ⇒ |
---|
| 24 | match \snd pr with |
---|
| 25 | [ Reg r ⇒ |
---|
| 26 | match r with |
---|
| 27 | [ PSD r ⇒ match v with [ inl r' ⇒ eq_identifier … r r' | _ ⇒ false ] |
---|
| 28 | | HDW r ⇒ match v with [ inr r' ⇒ eq_Register r r' | _ ⇒ false ] |
---|
| 29 | ] |
---|
| 30 | | _ ⇒ false |
---|
| 31 | ] |
---|
| 32 | | _ ⇒ false |
---|
| 33 | ] |
---|
| 34 | | _ ⇒ false |
---|
| 35 | ] |
---|
| 36 | | _ ⇒ false |
---|
| 37 | ]. |
---|
| 38 | |
---|
| 39 | definition interferes_asym : |
---|
| 40 | ∀globals.joint_internal_function ERTL globals → |
---|
| 41 | valuation register_lattice → |
---|
| 42 | label → vertex → vertex → bool ≝ |
---|
| 43 | λglobals,fn,liveafter,l,v1,v2. |
---|
| 44 | match v1 with |
---|
| 45 | [ inr R ⇒ |
---|
| 46 | match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ] |
---|
| 47 | | _ ⇒ false ] |
---|
| 48 | ∨ |
---|
| 49 | match stmt_at … (joint_if_code … fn) l with |
---|
| 50 | [ None ⇒ false |
---|
| 51 | | Some s ⇒ |
---|
[3265] | 52 | ¬eliminable … (liveafter l) s ∧ |
---|
[3255] | 53 | in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧ |
---|
| 54 | ¬is_src_of_move … s v2 |
---|
| 55 | ]. |
---|
| 56 | |
---|
| 57 | definition interferes ≝ λglobals,fn,liveafter,label,v1,v2. |
---|
| 58 | interferes_asym globals fn liveafter label v1 v2 ∨ |
---|
| 59 | interferes_asym globals fn liveafter label v2 v1. |
---|
| 60 | |
---|
[1423] | 61 | (* prop_colouring is the non interferece |
---|
| 62 | prop_colouring 2 and 3 together say that spilled_no is the number of spilled |
---|
| 63 | registers *) |
---|
[3255] | 64 | record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝ |
---|
[1423] | 65 | { colouring: vertex → decision |
---|
| 66 | ; spilled_no: nat |
---|
[3255] | 67 | ; prop_colouring: ∀l. ∀v1, v2: vertex. |
---|
| 68 | interferes l v1 v2 → colouring v1 = colouring v2 → v1 = v2 |
---|
| 69 | ; prop_spilled_no: ∀v1:vertex.∀i.colouring v1 = decision_spill i → i < spilled_no |
---|
| 70 | ; hdw_same_colouring : ∀R.colouring (inr … R) = decision_colour R |
---|
[1229] | 71 | }. |
---|
| 72 | |
---|
[2739] | 73 | definition coloured_graph_computer ≝ |
---|
| 74 | ∀globals. |
---|
[3014] | 75 | ∀fn:joint_internal_function ERTL globals. |
---|
[2942] | 76 | ∀liveafter. |
---|
[3263] | 77 | list register → (* callee saved store *) |
---|
[3255] | 78 | coloured_graph (interferes … fn liveafter). |
---|