source: src/ERTL/Interference.ma @ 3018

Last change on this file since 3018 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
RevLine 
[3014]1include "ERTL/liveness.ma".
[1127]2
[1229]3inductive decision: Type[0] ≝
[1232]4  | decision_spill: nat → decision
[1229]5  | decision_colour: Register → decision.
6
[1423]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 *)
[2942]10record coloured_graph (before: valuation register_lattice): Type[1] ≝
[1423]11{ colouring: vertex → decision
12; spilled_no: nat
[2845]13; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
[2942]14  lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2
[2286]15; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
[2942]16   ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
[1229]17}.
18
[2739]19definition coloured_graph_computer ≝
20 ∀globals.
[3014]21  ∀fn:joint_internal_function ERTL globals.
[2942]22   ∀liveafter.
23    coloured_graph (livebefore globals fn liveafter).
Note: See TracBrowser for help on using the repository browser.