source: src/ERTLptr/Interference.ma @ 2944

Last change on this file since 2944 was 2942, checked in by sacerdot, 8 years ago

Many changes:

  1. Coloured graphs are now specified in terms of livebefore
  2. Type of livebefore changed so that it is now a valuation transformer
  3. Several axioms can now be inhabited in ERTLptrToLTLProof

Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

File size: 932 bytes
Line 
1include "ERTLptr/liveness.ma".
2
3inductive 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 *)
10record 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 exist-guarded 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
19definition coloured_graph_computer ≝
20 ∀globals.
21  ∀fn:joint_internal_function ERTLptr globals.
22   ∀liveafter.
23    coloured_graph (livebefore globals fn liveafter).
Note: See TracBrowser for help on using the repository browser.