Required reading: Kempe's graph-coloring algorithm, by Andrew W. Appel, 2016. Suggested reading: Formal Verification of Coalescing Graph-Coloring Register Allocation, by Sandrine Blazy, Benoit Robillard, and Andrew W. Appel. ESOP 2010: 19th European Symposium on Programming, pp. 145-164, March 2010. Coloring an undirected graph means, assigning a color to each node, so that any two nodes directly connected by an edge have different colors. The chromatic number of a graph is the minimum number of colors needed to color the graph. Graph coloring is NP-complete, so there is no polynomial-time algorithm; but we need to do it anyway, for applications such as register allocation in compilers. So therefore we often use incomplete algorithms: ones that work only on certain classes of graphs, or ones that color most but not all of the nodes. Those algorithms are often good enough for important applications. In this chapter we will study Kempe's algorithm for K-coloring a graph. It was invented by Alfred Kempe in 1879, for use in his attempt to prove the four-color theorem (that every planar graph is 4-colorable). His 4-color proof had a bug; but his algorithm continues to be useful: a (major) variation of it was used in the successful 1976 proof of the 4-color theorem, and in 1979 Kempe's algorithm was adapted by Gregory Chaitin for application to register allocation. It is the Kempe-Chaitin algorithm that we'll prove here. We implement a program to K-color an undirected graph, perhaps leaving some nodes uncolored. In a register-allocation problem, the graph nodes correspond to variables in a program, the colors correspond to registers, and the graph edges are interference constraints: two nodes connected by an edge cannot be assigned the same color. Nodes left uncolored are "spilled," that is, a register allocator would implement such nodes in memory locations instead of in registers. We desire to have as few uncolored nodes as possible, but this desire is not formally specified. In this exercise we show a simple and unsophisticated algorithm; the program described by Blazy et al. (cited above) is more sophisticated in several ways, such as the use of "register coalescing" to get better results and the use of worklists to make it run faster. Our algorithm does, at least, make use of efficient data structures for representing undirected graphs, adjacency sets, and so on.

Preliminaries: Representing Graphs

In the Trie chapter we saw how to represent efficient maps (lookup tables) where the keys are positive numbers in Coq. Those tries are implemented in the Coq standard library as FMaps, functional maps, and we will use them directly from the standard library. FMaps represent partial functions, that is, mapping keys to option(t) for whatever t. We will also use FSets, efficient sets of keys; you can think of those as FMaps from keys to unit, where None means absent and Some tt means present; but their implementation is a bit more efficient.

The nodes in our graph will be named by positive numbers. FSets and FMaps are interfaces for sets and maps over an element type. One instance is when the element type is positive, with a particular comparison operator corresponding to easy lookup in tries. The Coq module for this element type (with its total order) is PositiveOrderedTypeBits. We'll use E as an abbreviation for this module name.

The Module Type FSetInterface.S gives the API of "functional sets." One instance of this, PositiveSet, has keys = positive numbers. We abbreviate this as Module S.

And similarly for functional maps over positives

Lemmas About Sets and Maps

In order to reason about a graph coloring algorithm, we need to prove lemmas such as, "if you remove an element (one domain->range binding) from a finite map, then the result is a new finite map whose domain has fewer elements." (Duh!) But to prove this, we need to build up some definitions and lemmas. We start by importing some modules that have some already-proved properties of FMaps.

E.lt is a comparison predicate on positive numbers. It is not the usual less-than operator; it is a different ordering that is more compatible with the order that a Positive Trie arranges its keys. In the application of certain lemmas about maps and sets, we will need the facts that E.lt is a StrictOrder (irreflexive and transitive) and respects a congruence over equality (is Proper for eq ==> eq ==> iff). As shown here, we just have to dig up these facts from a submodule of a submodule of a submodule of M.

The domain of a map is the set of elements that map to Some(_). To calculate the domain, we can use M.fold, an operation that comes with the FMaps abstract data type. It takes a map m, function f and base value b, and calculates f x₁ y₁ (f x₂ y₂ (f x₃ y₃ (... (f xn yn b)...))), where (xi,yi) are the individual elements of m. That is, M.find xi m = Some yi, for each i. So, to compute the domain, we just use an f function that adds xi to a set; mapping this over all the nodes will add all the keys in m to the set S.empty.

Example: Make a map from node (represented as positive) to set of node (represented as S.t), in which nodes 3,9,2 each map to the empty set, and no other nodes map to anything.

equivlistA

Suppose two lists al,bl both contain the same elements, not necessarily in the same order. That is, ∀ x:A, In x al ↔ In x bl. In fact from this definition you can see that al or bl might even have different numbers of repetitions of certain elements. Then we say the lists are "equivalent." We can generalize this. Suppose instead of In x al, which says that the value x is in the list al, we use a different equivalence relation on that A. That is, InA eqA x al says that some element of al is equivalent to x, using the equivalence relation eqA. For example:

The predicate equivlistA eqA al bl says that lists al and bl have equivalent sets of elements, using the equivalence relation eqA. For example:

SortA_equivlistA_eqlistA

Suppose two lists al,bl are "equivalent:" they contain the same set of elements (modulo an equivalence relation eqA on elements, perhaps in different orders, and perhaps with different numbers of repetitions). That is, suppose equivlistA eqA al bl. And suppose list al is sorted, in some strict total order (respecting the same equivalence relation eqA). And suppose list bl is sorted. Then the lists must be equal (modulo eqA). Just to make this easier to think about, suppose eqA is just ordinary equality. Then if al and bl contain the same set of elements (perhaps reordered), and each list is sorted (by less-than, not by less-or-equal), then they must be equal. Obviously. That's what the theorem SortA_equivlistA_eqlistA says, in the Coq library:

That is, suppose eqA is an equivalence relation on type A, that is, eqA is reflexive, symmetric, and transitive. And suppose ltA is a strict order, that is, irreflexive and transitive. And suppose ltA respects the equivalence relation, that is, if eqA x x' and eqA y y', then ltA x y ↔ ltA x' y'. THEN, if l is sorted (using the comparison ltA), and l' is sorted, and l,l' contain equivalent sets of elements, then l,l' must be equal lists, modulo the equivalence relation. To make this easier to think about, let's use ordinary equality for eqA. We will be making sets and maps over the "node" type, E.t, but that's just type positive. Therefore, the equivalence E.eq: E.t → E.t → Prop is just the same as eq.

And therefore, eqlistA E.eq al bl means the same as al=bl.

So now, the theorem: if al and bl are sorted, and contain "the same" elements, then they are equal:

If list l is sorted, and you apply List.filter to remove the elements on which f is false, then the result is still sorted. Obviously.

S.remove and S.elements

The FSets interface (and therefore our Module S) provides these two functions:

In module S, of course, S.elt=positive, as these are sets of positive numbers. Now, this relationship between S.remove and S.elements will soon be useful:

That is, if i is in the set s, then the elements of S.remove i s is the list that you get by filtering i out of S.elements s. Go ahead and prove it!

Exercise: 3 stars, standard (Sremove_elements)

Lists of (key,value) Pairs

The elements of a finite map from positives to type A (that is, the M.elements of a M.t A) is a list of pairs (positive×A).

Let's start with a little lemma about lists of pairs: Suppose l: list (positive×A). Then j is in map fst l iff there is some e such that (j,e) is in l.

Exercise: 2 stars, standard (InA_map_fst_key)

Exercise: 3 stars, standard (Sorted_lt_key)

The function M.lt_key compares two elements of an M.elements list, that is, two pairs of type positive×A, by just comparing their first elements using E.lt. Therefore, an elements list (of type list(positive×A) is Sorted by M.lt_key iff its list-of-first-elements is Sorted by E.lt.

Cardinality

The cardinality of a set is the number of distinct elements. The cardinality of a finite map is, essentially, the cardinality of its domain set.

Exercise: 4 stars, standard (cardinal_map)

Hint: To prove this theorem, I used these lemmas. You might find a different way.

Exercise: 4 stars, standard (Sremove_cardinal_less)

We have a lemma SortA_equivlistA_eqlistA that talks about arbitrary equivalence relations and arbitrary total-order relations (as long as they are compatible. Here is a specialization to a particular equivalence (M.eq_key_elt) and order (M.lt_key).

Exercise: 4 stars, standard (Mremove_elements)

Exercise: 3 stars, standard (Mremove_cardinal_less)

Look at the proof of Sremove_cardinal_less, if you succeeded in that, for an idea of how to do this one.

Exercise: 2 stars, standard (two_little_lemmas)

Exercise: 3 stars, standard (Sin_domain)

To reason about M.fold, used in the definition of Mdomain, a useful theorem is WP.fold_rec_bis.

Now Begins the Graph Coloring Program

A node has "low degree" if the cardinality of its adjacency set is less than K

Some Proofs in Support of Termination

We need to prove some lemmas related to the termination of the algorithm before we can actually define the Function.

Exercise: 3 stars, standard (subset_nodes_sub)

Exercise: 3 stars, standard (select_terminates)

The Rest of the Algorithm

Proof of Correctness of the Algorithm.

We want to show that any coloring produced by the color function actually respects the interference constraints. This property is called coloring_ok.

Exercise: 2 stars, standard (adj_ext)

Exercise: 3 stars, standard (in_colors_of_1)

Exercise: 4 stars, standard (color_correct)

That concludes the proof that the algorithm is correct.

Trying Out the Algorithm on an Actual Test Case

That is our graph coloring: Node 4 is colored with color 1, node 2 with color 3, nodes 6 and 1 with 2, and node 5 with color 1.