Telma Lopes Marques
Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
Jasmin is a low-level programming language and a compiler, both supporting the development of high-assurance cryptography libraries. It features high-level abstractions and low-level features that allow the programmer to have almost total control over the performances of the code. The Jasmin compiler is also certified with the help of Rocq, which ensures that the security properties implemented in the source code are also guaranteed in the produced assembly code.
Among the compilation passes, register allocation is about deciding which variables are stored in which registers during the execution, while trying to minimize the number of memory swaps, called spilling, as they are costly in time.
Optimal register allocation is an NP-complete problem, as it very often relies on graph-coloring algorithms. Pre-coloring also adds a difficulty to the problem, because it forces some variables to be stored in certain registers depending on the architecture’s calling conventions and the instructions’ restrictions. As a result, the Jasmin compiler uses a heuristic to complete this pass, which in turn makes the algorithm not exact and compilable programs might be rejected by the compiler for unknown reasons.
This talk presents the register allocation problem in the Jasmin compiler, and an algorithm based on constraint programming to try and obtain an exact solution and, optionally, the optimal one. The advantage of using constraint programming lies in the fact that if the model is correct, running it through a solver gives either a solution or a proof that it is unsatisfiable, therefore making the register allocation algorithm exact. For that, the problem is modelled as a constraint optimization problem, using propositional formulas to represent the constraints related to spilling, and global and basic binary constraints for other constraints. The current models aim to minimize the number of spills, but the objective function can be changed to optimize different metrics.