## 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". 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 language | English |
---|---|

Pages (from-to) | 161-187 |

Number of pages | 27 |

Journal | Science of Computer Programming |

Volume | 50 |

Issue number | 1-3 |

DOIs | |

Publication status | Published - 2004 Mar |

Event | 12th European Symposium on Programming - Warsaw, Poland Duration: 2003 Apr 5 → 2003 Apr 13 |

## Keywords

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

## ASJC Scopus subject areas

- Software