source: src/ERTL/Interference.ma @ 1232

Last change on this file since 1232 was 1232, checked in by mulligan, 9 years ago

big changes: got what was implemented in the ertl to ltl pass type checking again

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