RALF

RALF is a framework for end-to-end evaluation of register allocators. Built on top of gcc, RALF enables evaluation and comparison of register allocators in the setting of an industrial-strength compiler. RALF supports modular plug-and-play of register allocators without modifying the compiler implementation at all. RALF provides any plugged-in register allocator with an intermediate program representation that is independent of the data structures of the framework. In return, the register allocator provides RALF with a set of register allocation directives. The contract between RALF and a register allocator is given by requirements on the intermediate program representation and the register allocation directives. RALF checks that the produced directives satisfy the requirements, thereby helping with finding bugs in a register allocator.

• Get started with RALF here.
  
  
• Tools for RALF can be found here.
  
  
• Soundness proofs written in twelf here.
  
  
• Reports and other publications here.
  
  
• Read RALF's FAQ here.
  
  
• Find Examples and Benchmarks here.
  
  
• Contact the authors.
  

Credits:
Lead developer: V. Krishna Nandivada
Faculty Advisor: Jens Palsberg
Tools and proofs: Fernando Pereira