-
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.
-
Resource Analysis driven by (Conditional) Termination Proofs
Authors:
Elvira Albert,
Miquel Bofill,
Cristina Borralleras,
Enrique Martin-Martin,
Albert Rubio
Abstract:
When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that t…
▽ More
When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools. Under consideration for acceptance in TPLP.
△ Less
Submitted 23 July, 2019;
originally announced July 2019.
-
A Formal, Resource Consumption-Preserving Translation of Actors to Haskell
Authors:
Elvira Albert,
Nikolaos Bezirgiannis,
Frank de Boer,
Enrique Martin-Martin
Abstract:
We present a formal translation of an actor-based language with cooperative scheduling to the functional language Haskell. The translation is proven correct with respect to a formal semantics of the source language and a high-level operational semantics of the target, i.e. a subset of Haskell. The main correctness theorem is expressed in terms of a simulation relation between the operational seman…
▽ More
We present a formal translation of an actor-based language with cooperative scheduling to the functional language Haskell. The translation is proven correct with respect to a formal semantics of the source language and a high-level operational semantics of the target, i.e. a subset of Haskell. The main correctness theorem is expressed in terms of a simulation relation between the operational semantics of actor programs and their translation. This allows us to then prove that the resource consumption is preserved over this translation, as we establish an equivalence of the cost of the original and Haskell-translated execution traces.
△ Less
Submitted 10 August, 2016; v1 submitted 9 August, 2016;
originally announced August 2016.
-
Rewriting and narrowing for constructor systems with call-time choice semantics
Authors:
Francisco J. López-Fraguas,
Enrique Martin-Martin,
Juan Rodríguez-Hortalá,
Jaime Sánchez-Hernández
Abstract:
Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non trivial issue…
▽ More
Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper we develop thoroughly the theory for the first order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics co** with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing (..)
To appear in Theory and Practice of Logic Programming (TPLP).
△ Less
Submitted 10 October, 2012; v1 submitted 12 September, 2012;
originally announced September 2012.
