Last change
on this file since 3195 was
3014,
checked in by tranquil, 7 years ago

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

File size:
926 bytes

Line  

1  include "ERTL/liveness.ma". 

2  

3  inductive decision: Type[0] ≝ 

4   decision_spill: nat → decision 

5   decision_colour: Register → decision. 

6  

7  (* prop_colouring is the non interferece 

8  prop_colouring 2 and 3 together say that spilled_no is the number of spilled 

9  registers *) 

10  record coloured_graph (before: valuation register_lattice): Type[1] ≝ 

11  { colouring: vertex → decision 

12  ; spilled_no: nat 

13  ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 

14  lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2 

15  ; prop_spilled_no: (*CSC: the existguarded premise is just to make the proof more general *) 

16  ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no 

17  }. 

18  

19  definition coloured_graph_computer ≝ 

20  ∀globals. 

21  ∀fn:joint_internal_function ERTL globals. 

22  ∀liveafter. 

23  coloured_graph (livebefore globals fn liveafter). 

Note: See
TracBrowser
for help on using the repository browser.