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 memoryregister 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.
Swipe to navigate through the chapters of this book
- Register Allocation by Proof Transformation
- Springer Berlin Heidelberg
- Sequence number
Neuer Inhalt/© ITandMEDIA