source: src/ERTL/Interference.ma @ 2420

Last change on this file since 2420 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 887 bytes
Line 
1include "ERTL/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 *)
10(* Wilmer: the generation of the destruct principle diverges;
11   Ctr-C make the file pass *)
12record coloured_graph (after: valuation register_lattice): Type[1] ≝
13{ colouring: vertex → decision
14; spilled_no: nat
15; prop_colouring: ∀l. ∀v1, v2: vertex.
16  lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
17; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
18   ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
19}.
20
21axiom build: ∀valuation. coloured_graph valuation.
Note: See TracBrowser for help on using the repository browser.