]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/untrusted/coloring.ml
Imported Upstream version 0.1
[pkg-cerco/acc-trusted.git] / extracted / untrusted / coloring.ml
1 (* Pasted from Pottier's PP compiler *)
2
3 open ERTL
4 open Untrusted_interference
5 open 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
14 type decision =
15   | Spill
16   | Color of I8051.register
17
18 (*
19 (* [print_decision] turns a decision into a string. *)
20
21 let 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
35 type coloring =
36     decision Vertex.Map.t
37
38 (* ------------------------------------------------------------------------- *)
39 (* Sets of colors. *)
40
41 module 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
48 let 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
57 let colors : ColorSet.t =
58  Untrusted_interference.hwregisterset_of_list I8051.registersAllocatable
59
60 (* This is the number of available colors. *)
61
62 let 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
74 let 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
83 let high graph v =
84   degree graph v >= k
85
86 (* [high_neighbors graph v] is the set of all high neighbors of [v]. *)
87
88 let 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
105 let 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
113 let 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
122 module Color (G : sig
123
124   val graph: graph
125   val uses: Registers.register -> int
126   val verbose: bool
127
128 end) = 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
373 end
374