source: src/ERTL/Interference.ma @ 3255

Last change on this file since 3255 was 3255, checked in by tranquil, 7 years ago
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File size: 2.2 KB
Line 
1include "ERTL/liveness.ma".
2
3inductive decision: Type[0] ≝
4  | decision_spill: nat → decision
5  | decision_colour: Register → decision.
6
7definition DeqRegister : DeqSet ≝
8mk_DeqSet Register eq_Register ?.
9#x #y % [2: #EQ destruct cases y % ]
10cases x -x try (cases y -y normalize #EQ destruct %)
11qed.
12
13unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister.
14
15definition is_src_of_move :
16∀globals.joint_statement ERTL globals → vertex → bool ≝
17λglobals,s,v.
18match 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
39definition 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.
44match v1 with
45[ inr R ⇒
46  match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ]
47| _ ⇒ false ]
48
49match 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
56definition interferes ≝ λglobals,fn,liveafter,label,v1,v2.
57interferes_asym globals fn liveafter label v1 v2 ∨
58interferes_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 *)
63record 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
72definition coloured_graph_computer ≝
73 ∀globals.
74  ∀fn:joint_internal_function ERTL globals.
75   ∀liveafter.
76    coloured_graph (interferes … fn liveafter).
Note: See TracBrowser for help on using the repository browser.