On the correctness of a branch displacement algorithm

TL;DR

This paper presents a formally verified algorithm for the NP-hard branch displacement problem in assembler design, ensuring correctness in selecting optimal jump instructions to minimize program size.

Contribution

We implemented and proved the correctness of a specific algorithm for the branch displacement problem within a formal verification framework.

Findings

Algorithm is proven correct

Addresses NP-hardness in assembler optimization

Applicable to multiple processor architectures

Abstract

The branch displacement problem is a well-known problem in assembler design. It revolves around the feature, present in several processor families, of having different instructions, of different sizes, for jumps of different displacements. The problem, which is provably NP-hard, is then to select the instructions such that one ends up with the smallest possible program. During our research with the CerCo project on formally verifying a C compiler, we have implemented and proven correct an algorithm for this problem. In this paper, we discuss the problem, possible solutions, our specific solutions and the proofs.