source: src/ERTL/Interference.ma @ 1230

Last change on this file since 1230 was 1230, checked in by mulligan, 8 years ago

more changes

File size: 14.2 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "common/Graphs.ma".
4include "common/Order.ma".
5include "common/Registers.ma".
6include "ERTL/ERTL.ma".
7include "ERTL/liveness.ma".
8
9include "utilities/adt/table_adt.ma".
10include "utilities/adt/priority_set_adt.ma".
11include "utilities/adt/set_adt.ma".
12include "utilities/adt/set_table_adt.ma".
13include "utilities/adt/register_table.ma".
14
15definition vertex ≝ register ⊎ Register.
16
17record graph: Type[0] ≝
18{
19  interferes: vertex → vertex → bool
20}.
21
22axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph.
23
24inductive decision: Type[0] ≝
25  | decision_spill: decision
26  | decision_colour: Register → decision.
27
28record coloured_graph (d: Type[0]): Type[1] ≝
29{
30  the_graph: graph;
31  colouring: register → d;
32  prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
33}.
34
35definition initial_colouring ≝ coloured_graph decision.
36axiom colour_initial: graph → initial_colouring.
37definition stack_colouring ≝ coloured_graph nat.
38axiom colour_stack: graph → stack_colouring.
39
40
41(* definition vertex_set ≝ set vertex. *)
42definition vertex_priority_set ≝ priority_set vertex.
43definition vertex_set_table ≝ set_table vertex (set vertex).
44definition vertex_set ≝ set vertex.
45definition Register_set_table ≝ set_table vertex (set Register).
46definition Register_set ≝ set Register.
47
48(*
49record graph: Type[0] ≝
50{
51  g_regmap     : register_table;
52  g_ivv        : vertex_set_table;
53  g_ivh        : Register_set_table;
54  g_pvv        : vertex_set_table;
55  g_pvh        : Register_set_table;
56  g_degree     : vertex_priority_set;
57  g_nmr        : vertex_priority_set
58}.
59
60definition set_ivv ≝
61  λgraph.
62  λivv: vertex_set_table.
63    let regmap ≝ g_regmap graph in
64    let ivh    ≝ g_ivh graph in
65    let pvv    ≝ g_pvv graph in
66    let pvh    ≝ g_pvh graph in
67    let degree ≝ g_degree graph in
68    let nmr    ≝ g_nmr graph in
69      mk_graph
70        regmap ivv ivh pvv pvh degree nmr.
71
72definition set_ivh ≝
73  λgraph.
74  λivh: Register_set_table.
75    let regmap ≝ g_regmap graph in
76    let ivv    ≝ g_ivv graph in
77    let pvv    ≝ g_pvv graph in
78    let pvh    ≝ g_pvh graph in
79    let degree ≝ g_degree graph in
80    let nmr    ≝ g_nmr graph in
81      mk_graph
82        regmap ivv ivh pvv pvh degree nmr.
83
84definition set_degree ≝
85  λgraph.
86  λdegree: vertex_priority_set.
87    let regmap ≝ g_regmap graph in
88    let ivv    ≝ g_ivv graph in
89    let ivh    ≝ g_ivh graph in
90    let pvv    ≝ g_pvv graph in
91    let pvh    ≝ g_pvh graph in
92    let nmr    ≝ g_nmr graph in
93      mk_graph
94        regmap ivv ivh pvv pvh degree nmr.
95
96definition set_nmr ≝
97  λgraph.
98  λnmr: vertex_priority_set.
99    let regmap ≝ g_regmap graph in
100    let ivv    ≝ g_ivv graph in
101    let ivh    ≝ g_ivh graph in
102    let pvv    ≝ g_pvv graph in
103    let pvh    ≝ g_pvh graph in
104    let degree ≝ g_degree graph in
105      mk_graph
106        regmap ivv ivh pvv pvh degree nmr.
107
108definition sg_neighboursv ≝
109  λgraph: graph.
110  λv: vertex.
111    set_tbl_find … v (g_ivv graph).
112
113definition sg_existsvv ≝
114  λgraph.
115  λv1.
116  λv2.
117  match sg_neighboursv graph v2 with
118  [ None       ⇒ false (* XXX: ok? *)
119  | Some neigh ⇒ set_member ? eq_nat v1 neigh
120  ].
121
122definition sg_neighboursh ≝
123  λgraph.
124  λv.
125    set_tbl_find ? ? v (g_ivh graph).
126
127definition sg_existsvh ≝
128  λgraph.
129  λv.
130  λh.
131  match sg_neighboursh graph v with
132  [ None       ⇒ false (* XXX: ok? *)
133  | Some neigh ⇒ set_member ? eq_Register h neigh
134  ].
135
136definition sg_degree ≝
137  λgraph.
138  λv.
139  match sg_neighboursv graph v with
140  [ None ⇒ None ?
141  | Some neigh ⇒
142    match sg_neighboursh graph v with
143    [ None ⇒ None ?
144    | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
145    ]
146  ].
147   
148definition sg_hwregs ≝
149  λgraph: graph.
150    let union ≝ λkey: vertex. set_union ? in
151    set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).
152
153axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
154
155definition sg_mkvvi ≝
156  λgraph.
157  λv1.
158  λv2.
159    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).
160
161definition sg_mkvv ≝
162  λgraph.
163  λv1.
164  λv2.
165    if eq_nat v1 v2 then
166      graph
167    else if sg_existsvv graph v1 v2 then
168      graph
169    else
170      sg_mkvvi graph v1 v2.
171
172definition sg_rmvv ≝
173  λgraph.
174  λv1.
175  λv2.
176    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).
177
178definition sg_rmvvifx ≝
179  λgraph.
180  λv1.
181  λv2.
182  if sg_existsvv graph v1 v2 then
183    sg_rmvv graph v1 v2
184  else
185    graph.
186
187definition sg_mkvhi ≝
188  λgraph.
189  λv.
190  λh.
191    set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)).
192
193definition sg_mkvh ≝
194  λgraph.
195  λv.
196  λh.
197  if sg_existsvh graph v h then
198    graph
199  else
200    sg_mkvhi graph v h.
201
202definition sg_rmvh ≝
203  λgraph.
204  λv.
205  λh.
206    set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).
207
208definition sg_rmvhifx ≝
209  λgraph.
210  λv.
211  λh.
212    if sg_existsvh graph v h then
213      sg_rmvh graph v h
214    else
215      graph.
216
217definition sg_coalesce ≝
218  λg.
219  λx.
220  λy.
221  match sg_neighboursv g x with
222  [ None       ⇒ None ?
223  | Some neigh ⇒
224    let graph ≝ set_fold ? graph (λw. λg.
225      sg_mkvv (sg_rmvv g x w) y w) neigh g
226    in
227    match sg_neighboursh g x with
228    [ None ⇒ None ?
229    | Some neigh ⇒
230      let graph ≝ set_fold ? ? (λh. λg.
231        sg_mkvh (sg_rmvh g x h) y h) neigh g
232      in
233        Some … graph
234    ]
235  ].
236
237definition sg_coalesceh ≝
238  λg.
239  λx.
240  λh.
241  match sg_neighboursv g x with
242  [ None       ⇒ None ?
243  | Some neigh ⇒
244    let graph ≝ set_fold ? graph (λw. λg.
245      sg_mkvh (sg_rmvv g x w) w h) neigh g
246    in
247    match sg_neighboursh g x with
248    [ None ⇒ None ?
249    | Some neigh ⇒
250      let graph ≝ set_fold ? ? (λk. λg.
251        sg_rmvh graph x k) neigh g
252      in
253        Some … graph
254    ]
255  ].
256
257definition sg_remove ≝
258  λg.
259  λx.
260  match sg_neighboursv g x with
261  [ None ⇒ None ?
262  | Some neigh ⇒
263    let graph ≝
264      set_fold … (λw. λgraph.
265        sg_rmvv graph x w) neigh g
266    in
267    match sg_neighboursh graph x with
268    [ None ⇒ None ?
269    | Some neigh ⇒
270      let graph ≝ set_fold … (λh. λg.
271        sg_rmvh g x h) neigh graph
272      in
273        Some ? graph
274    ]
275  ].
276
277definition ig_mkvvi ≝
278  λgraph.
279  λv1.
280  λv2.
281  let graph ≝ sg_mkvvi graph v1 v2 in
282  let graph ≝ sg_rmvvifx graph v1 v2 in
283  let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in
284  let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in
285    set_degree (set_nmr graph nmr') degree'.
286
287definition ig_rmvv ≝
288  λgraph.
289  λv1.
290  λv2.
291  let graph ≝ sg_rmvv graph v1 v2 in
292  let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in
293  let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in
294    set_degree (set_nmr graph nmr') degree'.
295
296definition ig_mkvhi ≝
297  λgraph.
298  λv.
299  λh.
300  let graph ≝ sg_mkvhi graph v h in
301  let graph ≝ sg_rmvhifx graph v h in
302  let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
303  let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
304    set_degree (set_nmr graph nmr) degree.
305
306definition ig_rmvh ≝
307  λgraph.
308  λv.
309  λh.
310  let graph ≝ sg_rmvh graph v h in
311  let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in
312  let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in
313    set_degree (set_nmr graph nmr) degree.
314
315definition pref_nmr ≝
316  λgraph.
317  λv.
318  match sg_neighboursv graph v with
319  [ None       ⇒ false (* XXX: ok? *)
320  | Some neigh ⇒
321    match sg_neighboursh graph v with
322    [ None        ⇒ false
323    | Some neigh' ⇒
324      andb (set_is_empty ? neigh) (set_is_empty ? neigh')
325    ]
326  ].
327
328definition pref_mkcheck ≝
329  λgraph.
330  λv.
331    if pref_nmr graph v then
332      let nmr' ≝ pset_remove ? v (g_nmr graph) in
333        set_nmr graph nmr'
334    else
335      graph.
336
337definition pref_mkvvi ≝
338  λgraph.
339  λv1.
340  λv2.
341    if sg_existsvv graph v1 v2 then
342      graph
343    else
344      let graph ≝ pref_mkcheck graph v1 in
345      let graph ≝ pref_mkcheck graph v2 in
346        sg_mkvvi graph v1 v2.
347
348definition pref_mkvhi ≝
349  λgraph.
350  λv.
351  λh.
352  if sg_existsvh graph v h then
353    graph
354  else
355    let graph ≝ pref_mkcheck graph v in
356      sg_mkvhi graph v h.
357
358(* XXX: look at this carefully *)
359definition pref_rmcheck ≝
360  λgraph.
361  λv.
362  if pref_nmr graph v then
363    match pset_lookup ? v (g_degree graph) with
364    [ None ⇒ graph (* XXX: ok? *)
365    | Some pref ⇒
366      let nmr ≝ pset_insert ? v pref (g_nmr graph) in
367        set_nmr graph nmr
368    ]
369  else
370    graph.
371
372definition pref_rmvv ≝
373  λgraph.
374  λv1.
375  λv2.
376  let graph ≝ sg_rmvv graph v1 v2 in
377  let graph ≝ pref_rmcheck graph v1 in
378  let graph ≝ pref_rmcheck graph v2 in
379    graph.
380
381definition pref_rmvh ≝
382  λgraph.
383  λv.
384  λh.
385  let graph ≝ sg_rmvh graph v h in
386  let graph ≝ pref_rmcheck graph v in
387    graph.
388   
389definition ig_ipp ≝ sg_neighboursv.
390definition ig_iph ≝ sg_neighboursh.
391definition ig_ppp ≝ sg_neighboursv.
392definition ig_pph ≝ sg_neighboursh.
393definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph).
394definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph).
395definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph).
396definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu.
397  rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu.
398
399definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝
400  λa: Type[0].
401  λcompare: a → a → order.
402  λf: vertex → a.
403  λgraph.
404  let folded ≝ ig_fold … (λw. λaccu.
405    let dw ≝ f w in
406      match accu with
407      [ None      ⇒ Some … 〈dw, w〉
408      | Some dv_v ⇒
409        let 〈dv, v〉 ≝ dv_v in
410          match compare dw dv with
411          [ order_lt ⇒ Some … 〈dw, w〉
412          | _        ⇒ accu
413          ]
414      ]) graph (None …)
415  in
416    match folded with
417    [ None          ⇒ None …
418    | Some ignore_v ⇒
419      let 〈ignore, v〉 ≝ ignore_v in
420        Some … v
421    ].
422   
423definition ig_ppedge ≝ vertex × vertex.
424
425definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p.
426
427definition ig_phedge ≝ vertex × Register.
428
429definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p.
430
431definition ig_create ≝
432  λregs.
433  let 〈ignore_int, table'', priority''〉 ≝
434    foldr … (λr. λv_table_priority'.
435      let 〈v, table', priority'〉 ≝ v_table_priority' in
436      let table'' ≝ rt_add r v table' in
437      let priority'' ≝ pset_insert ? v 0 priority' in
438        〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
439  in
440      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …)
441      (set_tbl_empty …) priority'' priority''.
442definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph).
443definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph).
444definition ig_mkipp ≝
445  λgraph.
446  λregs1.
447  λregs2.
448    set_fold … (λr1. λgraph.
449      let v1 ≝ ig_lookup graph r1 in
450        set_fold … (λr2. λgraph.
451          sg_mkvv graph v1 (ig_lookup graph r2)
452        ) regs2 graph
453    ) regs1 graph.
454definition ig_mkiph ≝
455  λgraph.
456  λregs.
457  λhwregs.
458    set_fold … (λr. λgraph.
459      let v ≝ ig_lookup graph r in
460        set_fold … (λh. λgraph.
461          sg_mkvh graph v h
462        ) hwregs graph
463    ) regs graph.
464definition ig_mki ≝
465  λgraph.
466  λregs1_hwregs1.
467  λregs2_hwregs2.
468  let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
469  let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
470  let graph ≝ ig_mkipp graph regs1 regs2 in
471  let graph ≝ ig_mkiph graph regs1 hwregs2 in
472  let graph ≝ ig_mkiph graph regs2 hwregs1 in
473    graph.
474definition ig_mkppp ≝
475  λgraph.
476  λr1.
477  λr2.
478  let v1 ≝ ig_lookup graph r1 in
479  let v2 ≝ ig_lookup graph r2 in
480  let graph ≝ sg_mkvv graph v1 v2 in
481    graph.
482definition ig_mkpph ≝
483  λgraph.
484  λr.
485  λh.
486  let v ≝ ig_lookup graph r in
487  let graph ≝ sg_mkvh graph v h in
488    graph.
489(*   
490(* XXX: precondition:
491  x \not\eq y
492  existsvv graph x y == false i.e. coalesce interfering edges *)
493definition ig_coalesce ≝
494  λgraph.
495  λx.
496  λy.
497  let graph ≝ sg_coalesce graph x y in
498
499let coalesce graph x y =
500
501  assert (x <> y); (* attempt to coalesce one vertex with itself *)
502  assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
503
504  (* Perform coalescing in the two subgraphs. *)
505
506  let graph = interference#coalesce graph x y in
507  let graph = preference#coalesce graph x y in
508
509  (* Remove [x] from all tables. *)
510
511  {
512    graph with
513    regmap = RegMap.coalesce x y graph.regmap;
514    ivh = Vertex.Map.remove x graph.ivh;
515    pvh = Vertex.Map.remove x graph.pvh;
516    degree = PrioritySet.remove x graph.degree;
517    nmr = PrioritySet.remove x graph.nmr;
518  }
519*)
520
521*)
522
523axiom ig_mkppp: graph → register → register → graph.
524axiom ig_mkpph: graph → register → Register → graph.
525axiom ig_coalesce: graph → vertex → vertex → graph.
526axiom ig_coalesceh: graph → vertex → Register → graph.
527axiom ig_remove: graph → vertex → graph.
528axiom ig_freeze: graph → vertex → graph.
529axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *)
530axiom ig_droph: graph → graph.
531axiom ig_lookup: graph → register → vertex.
532axiom ig_registers: graph → vertex → list register.
533axiom ig_degree: graph → vertex → nat.
534axiom ig_lowest: graph → option (vertex × nat).
535axiom ig_lowest_non_move_related: graph → option (vertex × nat).
536axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
537  graph → option vertex.
538axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A.
539axiom ig_ipp: graph → vertex → vertex_set.
540axiom ig_iph: graph → vertex → list Register.
541axiom ig_ppp: graph → vertex → vertex_set.
542axiom ig_pph: graph → vertex → list Register.
543definition ig_ppedge ≝ vertex × vertex.
544axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge.
545definition ig_phedge ≝ vertex × Register.
546axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.