Electrical Fire

Design

Primitive Graph Format

Control Layer

Control Scheduling

Proof

Here we prove that phase 3d of our scheduling algorithm will (1) terminate and (2) not get stuck.

Termination

The algorithm terminates because at each point either:

  1. The number of elements in W goes down by one, possibly increasing the size of the stack T, or
  2. The number of elements on the stack T goes down by one.

By induction, since both the size of W and the size of T are initially positive and finite, both must eventually reach zero.

Liveness

The algorithm does not get stuck if, as long as at least one of T and W isn't empty, we can choose one of the three alternatives in phase 3d. We will prove that, in fact, either alternative 2 or alternative 3 will apply.

Let LOOPS be the set of immediately nested loops in REG that contain at least one working node.

Let CLIQUES be the set of cliques obtained by scheduling LOOPS.

Lemma 1. Every short edge incoming to a node in R originates from a node in R or from the last node of some clique in CLIQUES. This holds because of conditions 1 and 5 in phase 3b and because once an edge is designated a long edge it is never changed to a short edge.

Lemma 2. Every short edge incoming to a node in W originates from either W, the current node P, the last node of some clique on the stack T, or the last node of some clique in the schedule SL, where L's header is in W. We can prove this by induction. By lemma 1, it holds in the base case when W is R - {H}, P is H, and every immediate subloop's header is in W. For the induction case, we note that:

  1. Each time we assign a new value to P, we make every outgoing edge from the old P node into a long edge.
  2. Each time we remove a node N from W that is not the header of a subloop, we assign P := N.
  3. Each time we remove a node N from W that is the header of a subloop L, we take one of L's cliques and assign its last node to P and we push the remaining cliques of L onto the stack T.
  4. Each time we pop a clique from the stack T, we assign its last node to P.

In each of the above cases, if the induction hypothesis held before our action, it will hold after it as well.

Lemma 3. Let F be the subgraph of the function's control graph consisting only of forward, exception, and return edges. F is acyclic , every node in F is reachable from the function's begin node via edges in F, and the short edges form subgraph of F. F is acyclic by constraint CYCLES1 on the control flow graph. Every node in F is reachable from the function's begin node via edges in F by constraint CONNECTED1 on the control flow graph. The short edges form a subgraph of F by the initial construction of short edges in phase 3b, where we defined every backward edge to be a long edge.

Liveness. Let us assume that we are stuck (none of the three alternatives applies) and we will show that we have scheduled all nodes in R. Let T be our current stack and W be our current subset of R - {H}. T must be empty; otherwise we could apply alternative 2 and we would not be stuck.

Let F be as defined in lemma 3. Since F is acyclic, we can number all nodes in the control graph with unique numbers such that the source of any edge E in F has a number lower than the target of E. By lemma 3, the source of any short edge has a number strictly less than the target of that edge.

If W is nonempty, let X be the node in W with the smallest number. By lemma 2, the only short edges pointing to X must be from one of the following sources:

  1. a node in W
  2. P,
  3. the last node of some clique on the stack T, or
  4. the last node of some clique in the schedule SL, where L's header is in W.

Case 1 cannot apply because X's predecessor would be in W and yet have a smaller number than X, contradicting our choice of X. Case 3 cannot apply because T is empty.

Suppose case 4 applies to X. Let L be any immediate subloop of REG that contains a node A such that A->X is a short edge, and let HL be the header of loop L. By the definition of a loop, HL dominates A, so HL's number must be less than or equal to A's number, which in turn is strictly less than X's number. Now, since case 4 applied to X, HL is itself a member of W with a number less than X, which contradicts our choice of X. Hence case 4 cannot apply.

Suppose case 2 applies to X. In this case node X is ready with respect to P, so we can choose alternative 3, contradicting the assumption that we are stuck. Thus, case 4 cannot apply to X either.

Since none of the cases can apply to X, there must be no such X, implying that W is empty and we have already scheduled all nodes in R.