Linear Tree Constraints

TL;DR

This paper addresses the decidability of linear tree constraints used in resource analysis of object-oriented programs, providing a comprehensive decision procedure for the entire relevant constraint class.

Contribution

We solve the open problem of decidability for the full class of linear tree constraints in resource analysis, extending previous fragment-based results.

Findings

Decidability of the entire class of linear tree constraints established.

A new decision procedure for solving these constraints is introduced.

The results enable more effective resource analysis for object-oriented programs.

Abstract

Linear tree constraints were introduced by Hofmann and Rodriguez in the context of amortized resource analysis for object oriented programs. More precisely, they gave a reduction from inference of resource types to constraint solving. Thus, once we have found an algorithm to solve the constraints generated from a program, we can read off the resource consumption from their solutions. These constraints have the form of pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. We are interested in the question if a system of such constraints is simultaneously satisfiable. Bauer and Hofmann have recently identified a fragment of the tree constraint problem (UTC) that is still sufficient for program analysis and they proved that the list case of UTC is decidable, whereas the case with trees of degree at least two remained open. In this paper, we solve this problem. We give a decision procedure that covers the entire range of constraints needed for resource analysis.