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 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.
This work was partially supported by Grant-in-aid for scientific research on priority area “informatics” A01-08, grant no:14019403.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. Briggs, K.D. Cooper, and L. Torczon. Improvements to graph coloring register allocation. ACM Trans. Program. Lang. Syst., 16(3):428–455, 1994.
G. J. Chaitin. Register allocation & spilling via graph coloring. In Proc. ACM Symposium on Compiler Construction, pages 98–105, 1982.
G. J. Chaitin, M.A. Auslander, A.K. Chandra, J. Cocke, M.E. Hopkins, and P.W. Markstein. Register allocation via coloring. Computer Languages, 6(1):47–57, 1981.
R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, and F.K. Zadeck. Effciently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst., 13(4):451–490, 1991.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.
G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In Proc. ACM POPL Symposium, 1998.
G. Necula and P. Lee. Proof-carrying code. In Proc. ACM POPL Symposium, pages 106–119, 1998.
A. Ohori. The logical abstract machine: a Curry-Howard isomorphism for machine code. In Proc. International Symposium on Functional and Logic Programming, Springer LNCS 1722, pages 300–318, 1999.
H. Ono and Y. Komori. Logics without the contraction rule. Journal of Symbolic Logic, 50(1):169–201, 1985.
M. Poletto and V. Sarkar. Linear scan register allocation. ACM Trans. Program. Lang. Syst., 21(5):895–913, 1999.
R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proc. ACM POPL Symposium, pages 149–160, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ohori, A. (2003). Register Allocation by Proof Transformation. In: Degano, P. (eds) Programming Languages and Systems. ESOP 2003. Lecture Notes in Computer Science, vol 2618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36575-3_27
Download citation
DOI: https://doi.org/10.1007/3-540-36575-3_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00886-6
Online ISBN: 978-3-540-36575-4
eBook Packages: Springer Book Archive