Changeset 1193


Ignore:
Timestamp:
Sep 6, 2011, 3:49:31 PM (8 years ago)
Author:
mulligan
Message:

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1187 r1193  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
    149 definition RegisterForbidden: list Register ≝
    150   [ RegisterSST; RegisterST0; RegisterST1;
    151     RegisterSPL; RegisterSPH ].
    152149definition RegisterParams: list Register ≝
    153150  [ Register30; Register31; Register32; Register33;
     
    177174   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
    178175   RegisterST2; RegisterST3; RegisterSST].
     176(* registers minus forbidden *)
     177definition RegistersAllocatable ≝
     178  [Register00; Register01; Register02; Register03; Register04;
     179   Register05; Register06; Register07; Register10; Register11;
     180   Register12; Register13; Register14; Register15; Register16;
     181   Register17; Register20; Register21; Register22; Register23;
     182   Register24; Register25; Register26; Register27; Register30;
     183   Register31; Register32; Register33; Register34; Register35;
     184   Register36; Register37].
    179185
    180186definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  • src/ASM/Util.ma

    r1161 r1193  
    4747  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    4848  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     49  ].
     50
     51let rec forall
     52  (A: Type[0]) (f: A → bool) (l: list A)
     53    on l ≝
     54  match l with
     55  [ nil        ⇒ true
     56  | cons hd tl ⇒ f hd ∧ forall A f tl
    4957  ].
    5058
  • src/utilities/Colouring.ma

    r1192 r1193  
    11include "ASM/I8051.ma".
    22include "utilities/Interference.ma".
     3include "utilities/RegisterSet.ma".
    34
    45inductive decision: Type[0] ≝
     
    67  | decision_colour: Register → decision.
    78
    8 definition colouring ≝
     9definition colouring ≝ vertex_map decision.
     10
     11(* XXX: was set data structure previously *)
     12definition colour_set ≝ rs_set.
     13
     14definition add_colour ≝
     15  λrs: register_set.
     16  λc: colouring.
     17  λr: vertex.
     18  λcs: colour_set rs.
     19  match vm_find … r c with
     20  [ None ⇒ cs (* XXX: correct, or should we assert false? *)
     21  | Some decision ⇒
     22    match decision with
     23    [ decision_spill ⇒ cs
     24    | decision_colour colour ⇒ rs_insert rs colour cs
     25    ]
     26  ].
     27
     28definition colours ≝ λrs. rs_from_list rs RegistersAllocatable.
     29
     30definition k ≝ |RegistersAllocatable|.
     31
     32definition forbidden_colours ≝
     33  λrs.
     34  λgraph.
     35  λcolouring.
     36  λv.
     37    vs_fold ? (add_colour rs colouring) (ig_ipp graph v) (rs_from_list rs (ig_iph graph v)).
     38   
     39definition high ≝
     40  λgraph.
     41  λv.
     42    geb (ig_degree graph v) k.
     43
     44definition high_neighbours ≝
     45  λgraph.
     46  λv.
     47    vs_filter (high graph) (ig_ipp graph v).
     48
     49definition georgepp ≝
     50  λrs.
     51  λgraph.
     52  λab.
     53  let 〈a, b〉 ≝ ab in
     54    vs_subset … (high_neighbours graph a) (ig_ipp graph b) ∧
     55      rs_subset rs (rs_from_list rs (ig_iph graph a)) (rs_from_list rs (ig_iph graph b)).
     56
     57
     58
  • src/utilities/Interference.ma

    r1192 r1193  
    88(* vertex sets *)
    99axiom vertex_set: Type[0].
     10axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
     11axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
     12axiom vs_subset: vertex_set → vertex_set → bool.
    1013
    1114(* vertex maps *)
    12 axiom vertex_map: Type[0].
     15axiom vertex_map: Type[0] → Type[0].
     16axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    1317
    1418definition interference_graph ≝ graph label.
     
    3539  interference_graph → option vertex.
    3640axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    37 axiom ig_ipp: interference_graph → vertex → list vertex.
     41axiom ig_ipp: interference_graph → vertex → vertex_set.
    3842axiom ig_iph: interference_graph → vertex → list Register.
    39 axiom ig_ppp: interference_graph → vertex → list vertex.
     43axiom ig_ppp: interference_graph → vertex → vertex_set.
    4044axiom ig_pph: interference_graph → vertex → list Register.
    4145definition ig_ppedge ≝ vertex × vertex.
  • src/utilities/RegisterSet.ma

    r1075 r1193  
    1111  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
     13  rs_subset: rs_set → rs_set → bool;
    1314  rs_to_list: rs_set → list Register;
    1415  rs_from_list: list Register → rs_set
     
    4546  λs: list Register.
    4647    nub_by ? eq_Register (r @ s).
     48
     49definition rs_list_set_subset ≝
     50  λr: list Register.
     51  λs: list Register.
     52    forall … (λx. member … eq_Register x s) r.
    4753 
    4854definition rs_list_set_from_list ≝
     
    5561                  rs_list_set_insert rs_list_set_exists
    5662                  rs_list_set_union
     63                  rs_list_set_subset
    5764                  (λx. x) rs_list_set_from_list.
Note: See TracChangeset for help on using the changeset viewer.