Register allocation by proof transformation

Atsushi Ohori

Research output: Contribution to journalConference articlepeer-review

6 Citations (Scopus)


This paper presents a proof-theoretical framework 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 a proof system with restricted variable access. In our framework, the set of registers acts as a "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". Memory-register moves are systematically incorporated in our proof transformation process. Its correctness is a direct corollary of our construction; the resulting proof is equivalent to the proof of the original code modulo treatment of structural rules. The framework serves as a basis for reasoning about formal properties of register allocation process, and it also yields a clean and systematic register allocation algorithm. The algorithm has been implemented, demonstrating the feasibility of the framework.

Original languageEnglish
Pages (from-to)161-187
Number of pages27
JournalScience of Computer Programming
Issue number1-3
Publication statusPublished - 2004 Mar
Event12th European Symposium on Programming - Warsaw, Poland
Duration: 2003 Apr 52003 Apr 13


  • Liveness analysis
  • Proof transformation
  • Register allocation
  • Structural rules

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Register allocation by proof transformation'. Together they form a unique fingerprint.

Cite this