source: extracted/untrusted/coloring.ml @ 2968

Last change on this file since 2968 was 2740, checked in by sacerdot, 7 years ago

Graph colouring terminated up to Uses that will be implemented
in Matita.

File size: 11.4 KB
Line 
1(* Pasted from Pottier's PP compiler *)
2
3open ERTL
4open Untrusted_interference
5open Printf
6
7(* ------------------------------------------------------------------------- *)
8(* Decisions. *)
9
10(* A decision is of the form either [Spill] -- the vertex could
11   not be colored and should be spilled into a stack slot -- or
12   [Color] -- the vertex was assigned a hardware register. *)
13
14type decision =
15  | Spill
16  | Color of I8051.register
17
18(*
19(* [print_decision] turns a decision into a string. *)
20
21let print_decision = function
22  | Spill ->
23      "spilled"
24  | Color hwr ->
25      Printf.sprintf "colored $%s" (I8051.print_register hwr)
26*)
27
28(* ------------------------------------------------------------------------- *)
29(* Colorings. *)
30
31(* A coloring is a partial function of graph vertices to decisions.
32   Vertices that are not in the domain of the coloring are waiting for
33   a decision to be made. *)
34
35type coloring =
36    decision Vertex.Map.t
37
38(* ------------------------------------------------------------------------- *)
39(* Sets of colors. *)
40
41module ColorSet =
42  HwRegisterSet
43
44(* [add_color coloring r colors] returns the union of the set [colors] with
45   the element [color], if the vertex [r] was assigned color [color], and
46   returns [colors] if [r] was spilled. *)
47
48let add_color coloring r colors =
49  match Vertex.Map.find r coloring with
50  | Spill ->
51      colors
52  | Color color ->
53      ColorSet.add color colors
54
55(* These are the colors that we work with. *)
56
57let colors : ColorSet.t =
58 Untrusted_interference.hwregisterset_of_list I8051.registersAllocatable
59
60(* This is the number of available colors. *)
61
62let k : int =
63  ColorSet.cardinal colors
64
65(* ------------------------------------------------------------------------- *)
66(* Choices of colors. *)
67
68(* [forbidden_colors graph coloring v] is the set of colors that cannot be
69   assigned to [v] considering [coloring], a coloring of every vertex in
70   [graph] except [v]. *)
71(* This takes into account [v]'s possible interferences with hardware
72   registers, which are viewed as forbidden colors. *)
73
74let forbidden_colors graph coloring v =
75  Vertex.Set.fold (add_color coloring) (ipp graph v) (iph graph v)
76
77(* ------------------------------------------------------------------------- *)
78(* Low and high vertices. *)
79
80(* A vertex is low (or insignificant) if its degree is less than [k].
81   It is high (or significant) otherwise. *)
82
83let high graph v =
84  degree graph v >= k
85
86(* [high_neighbors graph v] is the set of all high neighbors of [v]. *)
87
88let high_neighbors graph v =
89  Vertex.Set.filter (high graph) (ipp graph v)
90
91(* ------------------------------------------------------------------------- *)
92(* George's conservative coalescing criterion. *)
93
94(* According to this criterion, two vertices [a] and [b] can be
95   coalesced, suppressing [a] and keeping [b], if the following
96   two conditions hold:
97
98     1. (pseudo-registers) every high neighbor of [a] is a neighbor of [b];
99     2. (hardware registers) every hardware register that interferes with
100        [a] also interferes with [b].
101
102   This means that, after all low vertices have been removed, any color that
103   is suitable for [b] is also suitable for [a]. *)
104
105let georgepp graph (a, b) =
106  Vertex.Set.subset (high_neighbors graph a) (ipp graph b) &&
107  HwRegisterSet.subset (iph graph a) (iph graph b)
108
109(* According to this criterion, a vertex [a] and a hardware register
110   [c] can be coalesced (that is, [a] can be assigned color [c]) if
111   every high neighbor of [a] interferes with [c]. *)
112
113let georgeph graph (a, c) =
114  Vertex.Set.fold (fun neighbor accu ->
115    accu &&
116    HwRegisterSet.mem c (iph graph neighbor)
117  ) (high_neighbors graph a) true
118
119(* ------------------------------------------------------------------------- *)
120(* Here is the coloring algorithm. *)
121
122module Color (G : sig
123
124  val graph: graph
125  val uses: Registers.register -> int
126  val verbose: bool
127
128end) = struct
129
130  (* The cost function heuristically evaluates how much it might cost
131     to spill vertex [v]. Here, the cost is the ratio of the number of
132     uses of the pseudo-registers represented by [v] by the degree of
133     [v]. One could also take into account the number of nested loops
134     that the uses appear within, but that is not done here. *)
135
136  let cost graph v =
137    let uses =
138      Pset.fold (fun r uses ->
139        G.uses r + uses
140      ) (registers graph v) 0
141    in
142    (float_of_int uses) /. (float_of_int (degree graph v))
143
144  (* The algorithm maintains a transformed graph as it runs. It is
145     obtained from the original graph by removing, coalescing, and
146     freezing vertices. *)
147
148  (* Each of the functions that follow returns a coloring of the graph
149     that it is passed. These functions correspond to the various
150     states of the algorithm (simplification, coalescing, freezing,
151     spilling, selection). The function [simplification] is the
152     initial state. *)
153
154  (* [simplification] removes non-move-related nodes of low degree. *)
155
156  let rec simplification graph : coloring =
157
158    match lowest_non_move_related graph with
159
160    | Some (v, d) when d < k ->
161
162        (* We found a non-move-related node [v] of low degree. Color
163           the rest of the graph, then color [v]. This is what I call
164           selection. *)
165
166(*
167        if G.verbose then
168          printf "Simplifying low vertex: %s.\n%!" (print_vertex graph v);
169*)
170
171        selection graph v
172
173    | _ ->
174
175        (* There are no non-move-related nodes of low degree.
176           Could not simplify further. Start coalescing. *)
177
178        coalescing graph
179
180  (* [coalescing] looks for a preference edge that can be collapsed.
181     It is called after [simplification], so it is known, at this
182     point, that all nodes of low degree are move-related. *)
183
184  and coalescing graph : coloring =
185
186    (* Find a preference edge between two vertices that passes
187       George's criterion.
188
189       [pppick] examines all preference edges in the graph, so its use
190       is inefficient. It would be more efficient instead to examine
191       only areas of the graph that have changed recently. More
192       precisely, it is useless to re-examine a preference edge that
193       did not pass George's criterion the last time it was examined
194       and whose neighborhood has not been modified by simplification,
195       coalescing or freezing. Indeed, in that case, and with a
196       sufficiently large definition of ``neighborhood'', this edge is
197       guaranteed to again fail George's criterion. It would be
198       possible to modify the [Interference.graph] data structure so
199       as to keep track of which neighborhoods have been modified and
200       provide a specialized, more efficient version of [pppick]. This
201       is not done here. *)
202
203    match pppick graph (georgepp graph) with
204
205    | Some (a, b) ->
206
207(*
208        if G.verbose then
209          printf "Coalescing %s with %s.\n%!" (print_vertex graph a) (print_vertex graph b);
210*)
211
212        (* Coalesce [a] with [b] and color the remaining graph. *)
213
214        let coloring = simplification (coalesce graph a b) in
215
216        (* Assign [a] the same color as [b]. *)
217
218        Vertex.Map.add a (Vertex.Map.find b coloring) coloring
219
220    | None ->
221
222        (* Find a preference edge between a vertex and a hardware
223           register that passes George's criterion. Like [pppick],
224           [phpick] is slow. *)
225
226        match phpick graph (georgeph graph) with
227
228        | Some (a, c) ->
229
230(*
231            if G.verbose then
232              printf "Coalescing %s with $%s.\n%!" (print_vertex graph a) (I8051.print_register c);
233*)
234
235            (* Coalesce [a] with [c] and color the remaining graph. *)
236
237            let coloring = simplification (coalesceh graph a c) in
238
239            (* Assign [a] the color [c]. *)
240
241            Vertex.Map.add a (Color c) coloring
242
243        | None ->
244
245            (* Could not coalesce further. Start freezing. *)
246
247            freezing graph
248
249  (* [freezing] begins after [simplification] and [coalescing] are
250     finished, so it is known, at this point, that all nodes of low
251     degree are move-related and no coalescing is possible. [freezing]
252     looks for a node of low degree (which must be move-related) and
253     removes the preference edges that it carries. This potentially
254     opens new opportunities for simplification and coalescing. *)
255
256  and freezing graph : coloring =
257
258    match lowest graph with
259
260    | Some (v, d) when d < k ->
261
262        (* We found a move-related node [v] of low degree.
263           Freeze it and start over. *)
264
265(*
266        if G.verbose then
267          printf "Freezing low vertex: %s.\n%!" (print_vertex graph v);
268*)
269
270        simplification (freeze graph v)
271
272    | _ ->
273
274        (* Could not freeze further. Start spilling. *)
275
276        spilling graph
277
278  (* [spilling] begins after [simplification], [coalescing], and
279     [freezing] are finished, so it is known, at this point, that
280     there are no nodes of low degree.
281
282     Thus, we are facing a potential spill. However, we do optimistic
283     coloring: we do not spill a vertex right away, but proceed
284     normally, just as if we were doing simplification. So, we pick a
285     vertex [v], remove it, and check whether a color can be assigned
286     to [v] only after coloring what remains of the graph.
287
288     It is crucial to pick a vertex that has few uses in the code. It
289     would also be good to pick one that has high degree, as this will
290     help color the rest of the graph. Thus, we pick a vertex that has
291     minimum cost, where the cost is obtained as the ratio of the
292     number of uses of the pseudo-registers represented by this vertex
293     in the code by the degree of the vertex. One could also take into
294     account the number of nested loops that the uses appear within,
295     but that is not done here.
296
297     The use of [minimum] is inefficient, because this function
298     examines all vertices in the graph. It would be possible to
299     augment the [Interference.graph] data structure so as to keep
300     track of the cost associated with each vertex and provide
301     efficient access to a minimum cost vertex. This is not done
302     here. *)
303
304  and spilling graph : coloring =
305
306    match minimum (cost graph) graph with
307    | Some v ->
308       
309(*
310        if G.verbose then
311          printf "Spilling high vertex: %s.\n%!" (print_vertex graph v);
312*)
313       
314        selection graph v
315
316    | None ->
317
318        (* The graph is empty. Return an empty coloring. *)
319
320        Vertex.Map.empty
321
322  (* [selection] removes the vertex [v] from the graph, colors the
323     remaining graph, then selects a color for [v].
324
325     If [v] is low, that is, if [v] has degree less than [k], then at
326     least one color must still be available for [v], regardless of
327     how the remaining graph was colored.
328
329     If [v] was a potential spill, then it is not certain that a color
330     is still available. If one is, though, then we are rewarded for
331     being optimistic. If none is, then [v] becomes an actual
332     spill. *)
333
334  and selection graph v : coloring =
335
336    (* Remove [v] from the graph and color what remains. *)
337
338    let coloring = simplification (remove graph v) in
339
340    (* Determine which colors are allowed. *)
341
342    let allowed = ColorSet.diff colors (forbidden_colors graph coloring v) in
343
344    (* Make a decision.
345
346       We pick a color randomly among those that are allowed. One could
347       attempt to use biased coloring, that is, to pick a color that seems
348       desirable (or not undesirable) according to the preference edges
349       found in the initial graph. But that is probably not worth the
350       trouble. *)
351
352    let decision =
353      try
354        Color (ColorSet.choose allowed)
355      with Not_found ->
356        Spill
357    in
358
359(*
360    if G.verbose then
361      printf "Decision concerning %s: %s.\n%!" (print_vertex graph v) (print_decision decision);
362*)
363
364    (* Record our decision and return. *)
365
366    Vertex.Map.add v decision coloring
367
368  (* Run the algorithm. *)
369
370  let coloring =
371    simplification G.graph
372
373end
374
Note: See TracBrowser for help on using the repository browser.