On Deciding Constant Runtime of Linear Loops

TL;DR

This paper proves the decidability of whether certain linear loops with real eigenvalues have bounded runtime, which is crucial for program verification and safety analysis, and provides an implementation of the decision procedure.

Contribution

It establishes the decidability of constant runtime for linear loops with real eigenvalues and implements a decision procedure for practical use.

Findings

Decidability of constant runtime for loops with real eigenvalues.

Implementation of the decision procedure for practical verification.

Relevance to safety and termination analysis in program verification.

Abstract

We consider linear single-path loops of the form \[ \textbf{while} \quad \varphi \quad \textbf{do} \quad \vec{x} \gets A \vec{x} + \vec{b} \quad \textbf{end} \] where $\vec{x}$ is a vector of variables, the loop guard $\varphi$ is a conjunction of linear inequations over the variables $\vec{x}$, and the update of the loop is represented by the matrix $A$ and the vector $\vec{b}$. It is already known that termination of such loops is decidable. In this work, we consider loops where $A$ has real eigenvalues, and prove that it is decidable whether the loop's runtime (for all inputs) is bounded by a constant if the variables range over $\mathbb R$ or $\mathbb Q$. This is an important problem in automatic program verification, since safety of linear while-programs is decidable if all loops have constant runtime, and it is closely connected to the existence of multiphase-linear ranking functions, which are often used for termination and complexity analysis. To evaluate its practical applicability, we also present an implementation of our decision procedure.