Register allocation by proof transformation

Research output: Chapter in Book/Report/Conference proceedingChapter

3 Citations (Scopus)

Abstract

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". The necessary 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 yields a clean and powerful register allocation algorithm. The algorithm has been implemented, demonstrating the feasibility of the framework.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsPierpaolo Degano
PublisherSpringer Verlag
Pages399-413
Number of pages15
ISBN (Print)3540008861
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2618
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this