1 | include "ERTL/liveness.ma". |
---|

2 | |
---|

3 | inductive decision: Type[0] ≝ |
---|

4 | | decision_spill: nat → decision |
---|

5 | | decision_colour: Register → decision. |
---|

6 | |
---|

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 ⇒ |
---|

52 | in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧ |
---|

53 | ¬is_src_of_move … s v2 |
---|

54 | ]. |
---|

55 | |
---|

56 | definition interferes ≝ λglobals,fn,liveafter,label,v1,v2. |
---|

57 | interferes_asym globals fn liveafter label v1 v2 ∨ |
---|

58 | interferes_asym globals fn liveafter label v2 v1. |
---|

59 | |
---|

60 | (* prop_colouring is the non interferece |
---|

61 | prop_colouring 2 and 3 together say that spilled_no is the number of spilled |
---|

62 | registers *) |
---|

63 | record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝ |
---|

64 | { colouring: vertex → decision |
---|

65 | ; spilled_no: nat |
---|

66 | ; prop_colouring: ∀l. ∀v1, v2: vertex. |
---|

67 | interferes l v1 v2 → colouring v1 = colouring v2 → v1 = v2 |
---|

68 | ; prop_spilled_no: ∀v1:vertex.∀i.colouring v1 = decision_spill i → i < spilled_no |
---|

69 | ; hdw_same_colouring : ∀R.colouring (inr … R) = decision_colour R |
---|

70 | }. |
---|

71 | |
---|

72 | definition coloured_graph_computer ≝ |
---|

73 | ∀globals. |
---|

74 | ∀fn:joint_internal_function ERTL globals. |
---|

75 | ∀liveafter. |
---|

76 | coloured_graph (interferes … fn liveafter). |
---|