Header menu link for other important links
X
A Framework for End-to-End Verification and Evaluation of Register Allocators
, Magno Quintão Pereira Fernando, Palsberg Jens
Published in Springer Berlin Heidelberg
2007
Pages: 153 - 169
Abstract

This paper presents a framework for designing, verifying, and evaluating register allocation algorithms. The proposed framework has three main components. The first component is MIRA, a language for describing programs prior to register allocation. The second component is FORD, a language that describes the results produced by the register allocator. The third component is a type checker for the output of a register allocator which helps to find bugs. To illustrate the effectiveness of the framework, we present RALF, a tool that allows a register allocator to be integrated into the gcc compiler for the StrongARM architecture. RALF simplifies the development of register allocators by sheltering the programmer from the internal complexity of gcc. MIRA and FORD’s features are sufficient to implement most of the register allocators currently in use and are independent of any particular register allocation algorithm or compiler. To demonstrate the generality of our framework, we have used RALF to evaluate eight different register allocators, including iterated register coalescing, linear scan, a chordal based allocator, and two integer linear programming approaches.

About the journal
JournalData powered by TypesetInternational Static Analysis Symposium
PublisherData powered by TypesetSpringer Berlin Heidelberg
Open AccessNo