source: src/ERTL/Interference.ma @ 1241

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

changes for claudio

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