Register Allocation by Proof Transformation

Register Allocation by Proof Transformation, Atsushi Ohori. ESOP 2003.

This paper presents a proof-theoretical framework for register allocation that accounts for the entire process of register allocation. Liveness analysis is proof reconstruction (similar to type inference), and register allocation is proof transformation from a proof system with unrestricted variable accesses to the one with restricted variable access. In our framework, the set of registers acts as the ``working set'' of the live variables at each instruction step, which changes during the execution of the code. This eliminates the ad-hoc notion of ``spilling''. The necessary memory-register moves are systematically incorporated in the proof transformation process. Its correctness is a simple corollary of our construction; the resulting proof is equivalent to the proof of the original code modulo the treatment of structural rules. This yields a simple yet powerful register allocation algorithm. The algorithm has been implemented, demonstrating the feasibility of the framework.

The idea that making uses of the structural rules explicit gives you proof terms to model register-memory moves is very pretty. Another fun thing to do would be to take a continuation calculus and apply the ideas here to see if it produces a good low-level IR.

EDIT: Ehud asked for some further exposition, so here goes.

At a high level, you can think of the need to do register allocation as arising from a mismatch between a programming language and the hardware. In a language, we refer to data using variables, and in any given expression, we can use as many variables as we like. However, when a CPU does stuff, it wants the data to be in registers -- and it has only a small, finite set of them. So when a program is compiled, some variables can be represented by registers, and the rest must be represented by locations in memory (usually on the stack). Whenever the CPU needs to use a variable in memory, there must be explicit code to move it from memory into a register.

The idea in this paper is to take the typing derivation of a program with an unbounded variable set, and then divide the context into two parts, one representing the register file and the other representing variables in memory. In terms of the implementation, moves between these two zones correspond to register-memory moves; and in terms of logic, this is a use of the structural rule of Exchange, which permutes the order of variables in a context.

So this gives us a high-level, machine-independent characterization of the register allocation problem: take a one-zone derivation and convert it to a two-zone derivation. But it gets even better: as long as the register allocation algorithm only adds uses of the structural rules in its transformation, we know that the meaning of the original program is unchanged -- so this method also yields a simple way of proving that a register allocation pass is semantics-preserving. (The fact that this is an easy proof is one indication of the power of this idea.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Previously on LtU

Here, here and indirectly here, though none of the times generated much discussion.

Maybe the homepage provides

Maybe the homepage provides better visibility - one advantage of being a contributing editor (hint, hint...)

But this sounds like deep stuff, so I expect most people will skip this. A summary might help get the discussion going.


Can somebody who has read the paper (doesn't seem to be available freely yet) comment on whether this has any efficiency benefits? Or is it simply cleaner/easier to prove correct?

Short answer: we don't know

The paper didn't have any benchmarks, so we don't know how it will perform for sure -- the main contribution of this paper is really a framework that shows how to easily prove correctness. As a guess, I would expect the performance of his example algorithm to be roughly comparable to linear scan register allocation. That is, the generated code should be pretty good, but not up to the level of a state-of-the-art register allocation algorithm.

P.S. The link is to citeseer, which should have a free pdf download. If that doesn't work, try this link from his homepage.