-
Termination Analysis of Programs with Multiphase Control-Flow
Authors:
Jesús J. Domenech,
Samir Genaim
Abstract:
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase rankin…
▽ More
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasoning on these phases separately. In this paper we discuss techniques for proving termination of such programs, in particular: (1) using multiphase ranking functions, where we will discuss theoretical aspects of such ranking functions for several kinds of program representations; and (2) using control-flow refinement, in particular partial evaluation of Constrained Horn Clauses, to simplify the control-flow allowing, among other things, to prove termination with simpler ranking functions.
△ Less
Submitted 9 September, 2021;
originally announced September 2021.
-
A Transformational Approach to Resource Analysis with Typed-norms Inference
Authors:
Elvira Albert,
Samir Genaim,
Raúl Gutiérrez,
Enrique Martin-Martin
Abstract:
In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are map**s from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This art…
▽ More
In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are map**s from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice.
Under consideration in Theory and Practice of Logic Programming (TPLP).
△ Less
Submitted 6 August, 2019;
originally announced August 2019.
-
Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
Authors:
Jesús J. Doménech,
John P. Gallagher,
Samir Genaim
Abstract:
Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as…
▽ More
Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation; in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers. Under consideration for acceptance in TPLP.
△ Less
Submitted 31 July, 2019; v1 submitted 29 July, 2019;
originally announced July 2019.
-
Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets
Authors:
Amir M. Ben-Amram,
Jesús J. Doménech,
Samir Genaim
Abstract:
Multiphase ranking functions (M$Φ$RFs) are tuples $\langle f_1,\ldots,f_d \rangle$ of linear functions that are often used to prove termination of loops in which the computation progresses through a number of "phases". Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (Single-Path Constraint loops). The decision problem existence of…
▽ More
Multiphase ranking functions (M$Φ$RFs) are tuples $\langle f_1,\ldots,f_d \rangle$ of linear functions that are often used to prove termination of loops in which the computation progresses through a number of "phases". Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (Single-Path Constraint loops). The decision problem existence of a M$Φ$RF asks to determine whether a given SLC loop admits a M$Φ$RF, and the corresponding bounded decision problem restricts the search to M$Φ$RFs of depth $d$, where the parameter $d$ is part of the input. The algorithmic and complexity aspects of the bounded problem have been completely settled in a recent work. In this paper we make progress regarding the existence problem, without a given depth bound. In particular, we present an approach that reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking M$Φ$RFs to that of seeking recurrent sets (used to prove non-termination). It also helps in identifying classes of loops for which M$Φ$RFs are sufficient. Our research has led to a new representation for single-path loops, the difference polyhedron replacing the customary transition polyhedron. This representation yields new insights on M$Φ$RFs and SLC loops in general. For example, a result on bounded SLC loops becomes straightforward.
△ Less
Submitted 13 January, 2019; v1 submitted 18 November, 2018;
originally announced November 2018.
-
On Multiphase-Linear Ranking Functions
Authors:
Amir M. Ben-Amram,
Samir Genaim
Abstract:
Multiphase ranking functions ($\mathit{MΦRFs}$) were proposed as a means to prove the termination of a loop in which the computation progresses through a number of "phases", and the progress of each phase is described by a different linear ranking function. Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (single-path loops). We pro…
▽ More
Multiphase ranking functions ($\mathit{MΦRFs}$) were proposed as a means to prove the termination of a loop in which the computation progresses through a number of "phases", and the progress of each phase is described by a different linear ranking function. Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (single-path loops). We provide a complete polynomial-time solution to the problem of existence and of synthesis of $\mathit{MΦRF}$ of bounded depth (number of phases), when variables range over rational or real numbers; a complete solution for the (harder) case that variables are integer, with a matching lower-bound proof, showing that the problem is coNP-complete; and a new theorem which bounds the number of iterations for loops with $\mathit{MΦRFs}$. Surprisingly, the bound is linear, even when the variables involved change in non-linear way. We also consider a type of lexicographic ranking functions, $\mathit{LLRFs}$, more expressive than types of lexicographic functions for which complete solutions have been given so far. We prove that for the above type of loops, lexicographic functions can be reduced to $\mathit{MΦRFs}$, and thus the questions of complexity of detection and synthesis, and of resulting iteration bounds, are also answered for this class.
△ Less
Submitted 23 March, 2017; v1 submitted 22 March, 2017;
originally announced March 2017.
-
EasyInterface: A toolkit for rapid development of GUIs for research prototype tools
Authors:
Jesús Doménech,
Samir Genaim,
Einar Broch Johnsen,
Rudolf Schlatte
Abstract:
In this paper we describe EasyInterface, an open-source toolkit for rapid development of web-based graphical user interfaces (GUIs). This toolkit addresses the need of researchers to make their research prototype tools available to the community, and integrating them in a common environment, rapidly and without being familiar with web programming or GUI libraries in general. If a tool can be execu…
▽ More
In this paper we describe EasyInterface, an open-source toolkit for rapid development of web-based graphical user interfaces (GUIs). This toolkit addresses the need of researchers to make their research prototype tools available to the community, and integrating them in a common environment, rapidly and without being familiar with web programming or GUI libraries in general. If a tool can be executed from a command-line and its output goes to the standard output, then in few minutes one can make it accessible via a web-interface or within Eclipse. Moreover, the toolkit defines a text-based language that can be used to get more sophisticated GUIs, e.g., syntax highlighting, dialog boxes, user interactions, etc. EasyInterface was originally developed for building a common frontend for tools developed in the Envisage project.
△ Less
Submitted 1 February, 2017;
originally announced February 2017.
-
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
Authors:
Amir M. Ben-Amram,
Samir Genaim
Abstract:
In this paper we turn the spotlight on a class of lexicographic ranking functions introduced by Bradley, Manna and Sipma in a seminal CAV 2005 paper, and establish for the first time the complexity of some problems involving the inference of such functions for linear-constraint loops (without precondition). We show that finding such a function, if one exists, can be done in polynomial time in a wa…
▽ More
In this paper we turn the spotlight on a class of lexicographic ranking functions introduced by Bradley, Manna and Sipma in a seminal CAV 2005 paper, and establish for the first time the complexity of some problems involving the inference of such functions for linear-constraint loops (without precondition). We show that finding such a function, if one exists, can be done in polynomial time in a way which is sound and complete when the variables range over the rationals (or reals). We show that when variables range over the integers, the problem is harder -- deciding the existence of a ranking function is coNP-complete. Next, we study the problem of minimizing the number of components in the ranking function (a.k.a. the dimension). This number is interesting in contexts like computing iteration bounds and loop parallelization. Surprisingly, and unlike the situation for some other classes of lexicographic ranking functions, we find that even deciding whether a two-component ranking function exists is harder than the unrestricted problem: NP-complete over the rationals and $Σ^P_2$-complete over the integers.
△ Less
Submitted 20 April, 2015;
originally announced April 2015.
-
Challenges and Recommendations for Preparing HPC Applications for Exascale
Authors:
Erika Abraham,
Costas Bekas,
Ivona Brandic,
Samir Genaim,
Einar Broch Johnsen,
Ivan Kondov,
Sabri Pllana,
Achim Streit
Abstract:
While the HPC community is working towards the development of the first Exaflop computer (expected around 2020), after reaching the Petaflop milestone in 2008 still only few HPC applications are able to fully exploit the capabilities of Petaflop systems. In this paper we argue that efforts for preparing HPC applications for Exascale should start before such systems become available. We identify ch…
▽ More
While the HPC community is working towards the development of the first Exaflop computer (expected around 2020), after reaching the Petaflop milestone in 2008 still only few HPC applications are able to fully exploit the capabilities of Petaflop systems. In this paper we argue that efforts for preparing HPC applications for Exascale should start before such systems become available. We identify challenges that need to be addressed and recommend solutions in key areas of interest, including formal modeling, static analysis and optimization, runtime analysis and optimization, and autonomic computing. Furthermore, we outline a conceptual framework for porting HPC applications to future Exascale computing systems and propose steps for its implementation.
△ Less
Submitted 9 June, 2015; v1 submitted 24 March, 2015;
originally announced March 2015.
-
Inference of Field-Sensitive Reachability and Cyclicity
Authors:
Damiano Zanardini,
Samir Genaim
Abstract:
In heap-based languages, knowing that a variable x points to an acyclic data structure is useful for analyzing termination: this information guarantees that the depth of the data structure to which x points is greater than the depth of the structure pointed to by x.fld, and allows bounding the number of iterations of a loop which traverses the data structure on fld. In general, proving termination…
▽ More
In heap-based languages, knowing that a variable x points to an acyclic data structure is useful for analyzing termination: this information guarantees that the depth of the data structure to which x points is greater than the depth of the structure pointed to by x.fld, and allows bounding the number of iterations of a loop which traverses the data structure on fld. In general, proving termination needs acyclicity, unless program-specific or non-automated reasoning is performed. However, recent work could prove that certain loops terminate even without inferring acyclicity, because they traverse data structures "acyclically". Consider a double-linked list: if it is possible to demonstrate that every cycle involves both the "next" and the "prev" field, then a traversal on "next" terminates since no cycle will be traversed completely. This paper develops a static analysis inferring field-sensitive reachability and cyclicity information, which is more general than existing approaches. Propositional formulae are computed, which describe which fields may or may not be traversed by paths in the heap. Consider a tree with edges "left" and "right" to the left and right sub-trees, and "parent" to the parent node: termination of a loop traversing leaf-up cannot be guaranteed by state-of-the-art analyses. Instead, propositional formulae computed by this analysis indicate that cycles must traverse "parent" and at least one between "left" and "right": termination is guaranteed as no cycle is traversed completely. This paper defines the necessary abstract domains and builds an abstract semantics on them. A prototypical implementation provides the expected result on relevant examples.
△ Less
Submitted 19 May, 2014; v1 submitted 27 June, 2013;
originally announced June 2013.
-
Proving Termination Starting from the End
Authors:
Pierre Ganty,
Samir Genaim
Abstract:
We present a novel technique for proving program termination which introduces a new dimension of modularity. Existing techniques use the program to incrementally construct a termination proof. While the proof keeps changing, the program remains the same. Our technique goes a step further. We show how to use the current partial proof to partition the transition relation into those behaviors known t…
▽ More
We present a novel technique for proving program termination which introduces a new dimension of modularity. Existing techniques use the program to incrementally construct a termination proof. While the proof keeps changing, the program remains the same. Our technique goes a step further. We show how to use the current partial proof to partition the transition relation into those behaviors known to be terminating from the current proof, and those whose status (terminating or not) is not known yet. This partition enables a new and unexplored dimension of incremental reasoning on the program side. In addition, we show that our approach naturally applies to conditional termination which searches for a precondition ensuring termination. We further report on a prototype implementation that advances the state-of-the-art on the grounds of termination and conditional termination.
△ Less
Submitted 19 February, 2013;
originally announced February 2013.
-
Ranking Functions for Linear-Constraint Loops
Authors:
Amir M. Ben-Amram,
Samir Genaim
Abstract:
In this paper we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such functions implies termination, these problems are not equivalent to termination. When the variables range over the rationals (or reals), it is known that both problems…
▽ More
In this paper we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such functions implies termination, these problems are not equivalent to termination. When the variables range over the rationals (or reals), it is known that both problems are PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity has not yet been determined. We show that both problems are coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear and lexicographical-linear ranking functions, both for the general case and the special PTIME cases. Moreover, in the rational setting, our algorithm for synthesizing lexicographical-linear ranking functions extends existing ones, because our class of ranking functions is more general, yet it has polynomial time complexity.
△ Less
Submitted 9 July, 2013; v1 submitted 20 August, 2012;
originally announced August 2012.
-
Reachability-based Acyclicity Analysis by Abstract Interpretation
Authors:
Samir Genaim,
Damiano Zanardini
Abstract:
In programming languages with dynamic use of memory, such as Java, knowing that a reference variable x points to an acyclic data structure is valuable for the analysis of termination and resource usage (e.g., execution time or memory consumption). For instance, this information guarantees that the depth of the data structure to which x points is greater than the depth of the data structure pointed…
▽ More
In programming languages with dynamic use of memory, such as Java, knowing that a reference variable x points to an acyclic data structure is valuable for the analysis of termination and resource usage (e.g., execution time or memory consumption). For instance, this information guarantees that the depth of the data structure to which x points is greater than the depth of the data structure pointed to by x.f for any field f of x. This, in turn, allows bounding the number of iterations of a loop which traverses the structure by its depth, which is essential in order to prove the termination or infer the resource usage of the loop. The present paper provides an Abstract-Interpretation-based formalization of a static analysis for inferring acyclicity, which works on the reduced product of two abstract domains: reachability, which models the property that the location pointed to by a variable w can be reached by dereferencing another variable v (in this case, v is said to reach w); and cyclicity, modeling the property that v can point to a cyclic data structure. The analysis is proven to be sound and optimal with respect to the chosen abstraction.
△ Less
Submitted 13 February, 2013; v1 submitted 11 June, 2012;
originally announced June 2012.
-
Worst-Case Groundness Analysis Using Definite Boolean Functions
Authors:
Samir Genaim,
Michael Codish,
Jacob M. Howe
Abstract:
This note illustrates theoretical worst-case scenarios for groundness analyses obtained through abstract interpretation over the abstract domains of definite (Def) and positive (Pos) Boolean functions. For Def, an example is given for which any Def-based abstract interpretation for groundness analysis follows a chain which is exponential in the number of argument positions as well as in the numb…
▽ More
This note illustrates theoretical worst-case scenarios for groundness analyses obtained through abstract interpretation over the abstract domains of definite (Def) and positive (Pos) Boolean functions. For Def, an example is given for which any Def-based abstract interpretation for groundness analysis follows a chain which is exponential in the number of argument positions as well as in the number of clauses but sub-exponential in the size of the program. For Pos, we strengthen a previous result by illustrating an example for which any Pos-based abstract interpretation for groundness analysis follows a chain which is exponential in the size of the program. It remains an open problem to determine if the worst case for Def is really as bad as that for Pos.
△ Less
Submitted 26 May, 2004;
originally announced May 2004.
-
Inferring Termination Conditions for Logic Programs using Backwards Analysis
Authors:
Samir Genaim,
Michael Codish
Abstract:
This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalises traditional termination analysis where an analyser tries to verify termination for a specified mode. Our contribution is a methodology in which components of traditional termination analysis are combined with backwards analysis to obtain an analyser for termination inference. We id…
▽ More
This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalises traditional termination analysis where an analyser tries to verify termination for a specified mode. Our contribution is a methodology in which components of traditional termination analysis are combined with backwards analysis to obtain an analyser for termination inference. We identify a condition on the components of the analyser which guarantees that termination inference will infer all modes which can be checked to terminate. The application of this methodology to enhance a traditional termination analyser to perform also termination inference is demonstrated.
△ Less
Submitted 12 December, 2003;
originally announced December 2003.
