Automatic Verification of Register Allocation.

Summary

How to debug register allocation?

Register allocation is a complex and error prone activity. One of the problems in writing register allocation algorithms is how to verify if the code being generated is correct. In this page you can find a tool that automatically verifies if register allocation directives written according to RALF's specification are correct. In order to perform this verification, the debugger checks the target allocation directives against five rules. It is possible to prove that if all the rules are satisfied then the allocation is correct.

RALF is a framework that allows to test different register allocation algorithms. It provides the application developer with a program description format called MIRA. It compiles C programs, and generated a MIRA description for them. The application developer can use the MIRA description to determine how registers should be allocated. With such specifications in hands, he must generated a allocation description in the FORD format. RALF will generate C binaries from the FORD file. Such binaries can be executed in an ARM processor. For further description of RALF, check here. An schmematic description of the RALF architecture is given in the Figure below.

Schematic view of the RALF framework.

Mira source files have the .dat extension, and Ford source files have the .out extension. The debugger reads the (.dat) and (.out) files generated by Ralf for a given C procedure, and automatically checks their consistency according to the set of rules that it defines. A schematic view of the automatic verification process can be seen in the Figure below.

Schematic view of the debugger.

The debugger does not check the syntax of the register allocation directives, because this is already done by Ralf's parser. Syntactic errors include incorrect input files, due to incompatibility with Ford or Mira's grammar, and also the incorrect spelling of the allocation directives. Other, not so trivial syntax errors, include the use of non-existent machine registers, non-existent instructions, or non-existent temporaries.

Which register allocators have been implemented?

The sources that can be downloaded in this page contain the implementation of four register allocation algorithms. You can use such algorithms as a starting point for a different implementation, and also to get familiarized with the debugging tools. The package RegAlloc contains the implementation of the following register allocators:

How is the implementation organized?

The implementation that can be downloaded here is organized as follows:

In addition to the Java source files, the following scripts are available:

How does the MIRA/FORD visualizer works?

It is easier to find errors in register assignment directives if you can inspect the control flow graph. To make this possible, the debugging framework makes available a program that generates the representation of the control flow graph in .dot format. The (.dot) format can be visualized using some free tools such as Graphviz.

There are two ways to run the mira visualizer. If you are interested in visualizing only the control flow graph, and are not taking into consideration how are the registes allocated to temporaries, you just need the (.dat) file containing MIRA directives. In this case, in order to run the MIRA visualizer, type java RegAlloc.ControlFlowViewer file.dat. Below there is an example of .c source file, and the corresponding .dot file as opened with Omnigrafle (a shareware version of Omnigrafle can be downloaded here). The graph contains orange and blue nodes. Blue nodes denote function calls. It is important to know which instructions are function calls, because the register allocator must make sure that the caller save registers are not alive accross function calls.

An example of control flow graph generated by MIRA visualizer.

The control flow graph above has been generated from the source file below. The corresponding .dat file can be downloaded here. 

int main(int argc, char **argv) {
  int sum = 0;
  int counter = 0;

  for(counter = 1; counter < argc; counter++) {
    char *aux = argv[counter];
    while(*aux != '\0') {
      aux++;
      sum++;
    }
  }

  printf("Sum = %d\n", sum);

}

If you want to check how registers have been assigned to temporary variables, you will need both, the MIRA description (file.dat), and the FORD directives (file.out). In this case, type java RegAlloc.ControlFlowViewer file.dat file.out. The figure below shows the register allocation produced by the Iterated Register Coalescer algorithm for the program used in the previous example. Each temporary appears in the format t(r), where t is the temporary's name, and r is the machine register's name.

An example of control flow graph generated with register allocation.

How does the debugger works?

In order to call the debugger, use the script in the downloading package. Type debug mira.dat ford.out. The debugger will report inconsistencies in the allocation directives according to the five following rules:
  1. A temporary is never assigned to a machine register that is been used by another temporary.
  2. Two live ranges of different temporaries reach a joint point assigned to different registers.
  3. Two live ranges of the same temporary reach a joint point assigned to the same register.
  4. All the temporaries in the def set of an instruction are assigned to machine registers immediately after the instruction is executed.
  5. A temporary stored in a caller-save register is not alive across a function call.

The debugger can print the error messages enumerated below. A detailed description of each error can be found here.

Download
Download it This file contains the implementation of four different register allocation algorithms: the naive allocator, the Iterated Register Coalescing, the usage frequency based allocator, and the Chordal Graph based approach. Also this file contains some useful tools and libraries that can help in the implementation and debugging of other algorithms. In order to run these programs, you need Java 1.5. The source code is available, and you can use these programs as an Eclipse project by importing them into your own project.
Download it This file contains many useful shell scripts that will help to run the debugger, the control flow visualizer, and all the register allocators. Also the package provides scripts to invoke ralf with the gcc compiler.
Download it A detailed description of the translation validation between mira specifications and ford directives.

Write to me

Última atualização: 18 de Abril 2006.

Last update: April 18th, 2006.