Tree Constraint Solver (TCS) - Linear tree inequality solver for superlinear resource bounds on Java programs

该项目旨在为未加注释的面向对象Java程序的资源消耗提供可证明的正确上限。这种自动资源分析已经变得越来越流行，引起了相当大的行业兴趣，但到目前为止，大多数情况下仅限于函数式程序和以数组作为唯一基本数据结构的经典命令式程序。我们建立在成熟的基于类型的分期分析框架之上，该框架已成功地应用于函数式编程语言。面向对象的编程带来了几个新的挑战：a)数据结构是通过类隐式定义的，但不像函数数据类型声明中那样显式给出；b)命令式更新可能会导致复杂的别名；c)更一般的数据结构，如双向链表，甚至是一般的图形都是可能的。在早期的工作中，这些挑战是通过将资源约束问题简化为涉及无限多个数值变量的创新约束系统(线性树约束(LTC))来解决的。然而，在那里提出的启发式约束求解器仅限于某些特殊情况。最近的工作表明，一般的LTC是可决定的，因此在实践中也可能是容易处理的，本项目的目的是详细探讨这一点。具体地说，我们将为一般的LTC开发和实现一个有效的求解算法，该算法还提供了程序堆空间消耗的具体上限。为此，仅有可判断性是不够的，我们还需要根据闭合公式来检测约束的最小解。此外，我们将确定和证明决策问题的确切复杂性，并找到属于这一复杂性类别的新的、更好的算法。目前所获得的可判断性结果是一个很好的起点，使计划有可能实现，然后我们将利用这些结果为命令式面向对象程序设计基于类型的摊销资源分析，并在基于Java语法的原型实现的各种示例程序上进行测试。

This project aims to provide provably correct upper bounds on the resource consumption of unannotated object-oriented Java programs. Such automatic resource analysis has become increasingly popular with considerable industrial interest but was hitherto mostly confined to functional programs and classical imperative programs with arrays as the only essential data structure. We build upon the well-established framework of type-based amortized analysis, which has been applied to functional programming languages with great success. Object-oriented programming poses several new challenges: a) data structures are implicitly defined through classes, but not explicitly given as in functional datatype declarations, b) imperative updates may lead to complex aliasing, c) more general data structures like doubly-linked lists, or even general graphs are possible. In earlier work, these challenges were addressed with a reduction from the resource bound question to an innovative constraint system involving infinitely many numerical variables (”linear tree constraints (LTC)”). However, the heuristic constraint solver that was presented there was limited to certain special cases. In very recent work, it was shown that the general LTC are decidable and thus might be also tractable in practice and the aim of this project is to explore this in detail. Concretely, we will develop and implement an efficient solution algorithm for general LTC that delivers also concrete upper bounds on the heap space consumption of programs. For that, decidability alone is not sufficient, we also need to detect minimal solutions to the constraints in terms of closed formulas. Further, we will determine and prove the exact complexity of the decision problem and find a new, better algorithm that falls into this complexity class. The decidability result obtained by now is a good starting point that makes the plan likely to work out.We will then use these results to design a type-based amortized resource analysis for imperative object-oriented programs and test it on a variety of example programs with a prototype implementation based on Java syntax.