Showing 1–45 of 45 results for author: Hermenegildo, M

Checkification: A Practical Approach for Testing Static Analysis Truths

Authors: Daniela Ferreiro, Ignacio Casso, Jose F. Morales, Pedro López-García, Manuel V. Hermenegildo

Abstract: Static analysis is an essential component of many modern software development tools. Unfortunately, the ever-increasing complexity of static analyzers makes their coding error-prone. Even analysis tools based on rigorous mathematical techniques, such as abstract interpretation, are not immune to bugs. Ensuring the correctness and reliability of software analyzers is critical if they are to be inse… ▽ More Static analysis is an essential component of many modern software development tools. Unfortunately, the ever-increasing complexity of static analyzers makes their coding error-prone. Even analysis tools based on rigorous mathematical techniques, such as abstract interpretation, are not immune to bugs. Ensuring the correctness and reliability of software analyzers is critical if they are to be inserted in production compilers and development environments. While compiler validation has seen notable success, formal validation of static analysis tools remains relatively unexplored. In this paper, we propose a method for testing abstract interpretation-based static analyzers. Broadly, it consists in checking, over a suite of benchmarks, that the properties inferred statically are satisfied dynamically. The main advantage of our approach lies in its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework, and its blended static/dynamic assertion checking approach. We demonstrate that in this setting, the analysis can be tested with little effort by combining the following components already present in the framework: 1) the static analyzer, which outputs its results as the original program source with assertions interspersed; 2) the assertion run-time checking mechanism, which instruments a program to ensure that no assertion is violated at run time; 3) the random test case generator, which generates random test cases satisfying the properties present in assertion preconditions; and 4) the unit-test framework, which executes those test cases. We have applied our approach to the CiaoPP static analyzer, resulting in the identification of many bugs with reasonable overhead. Most of these bugs have been either fixed or confirmed, helping us detect a range of errors not only related to analysis soundness but also within other aspects of the framework. △ Less

Submitted 7 May, 2025; v1 submitted 21 January, 2025; originally announced January 2025.

Comments: Accepted for publication in Theory and Practice of Logic Programming (TPLP). Extended, revised version of our work published in LOPSTR 2020

Abstract Environment Trimming

Authors: Daniel Jurjo-Rivas, Jose F. Morales, Pedro López-García, Manuel V. Hermenegildo

Abstract: Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many useful program properties. Such properties include modes, determinacy, non-failure, cost, etc. This has motivated significant work on developing abstract domains to improve the precision and performance of sharing analy… ▽ More Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many useful program properties. Such properties include modes, determinacy, non-failure, cost, etc. This has motivated significant work on developing abstract domains to improve the precision and performance of sharing analyses. Much of this work has centered around the family of set-sharing domains, because of the high precision they offer. However, this comes at a price: their scalability to a wide set of realistic programs remains challenging and this hinders their wider adoption. In this work, rather than defining new sharing abstract domains, we focus instead on developing techniques which can be incorporated in the analyzers to address aspects that are known to affect the efficiency of these domains, such as the number of variables, without affecting precision. These techniques are inspired in others used in the context of compiler optimizations, such as expression reassociation and variable trimming. We present several such techniques and provide an extensive experimental evaluation of over 1100 program modules taken from both production code and classical benchmarks. This includes the Spectector cache analyzer, the s(CASP) system, the libraries of the Ciao system, the LPdoc documenter, the PLAI analyzer itself, etc. The experimental results are quite encouraging: we have obtained significant speed-ups, and, more importantly, the number of modules that require a timeout was cut in half. As a result, many more programs can be analyzed precisely in reasonable times. △ Less

Submitted 19 August, 2024; originally announced August 2024.

Comments: 61 pages, 10 figures, 7 tables, submitted to ICLP 2024

Journal ref: Theory and Practice of Logic Programming 24 (2024) 863-884

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants

Authors: Louis Rustenholz, Pedro Lopez-Garcia, José F. Morales, Manuel V. Hermenegildo

Abstract: Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-li… ▽ More Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours. △ Less

Submitted 29 August, 2024; v1 submitted 26 June, 2024; originally announced June 2024.

Comments: Preprint of a paper accepted at SAS 2024

Demonstrating (Hybrid) Active Logic Documents and the Ciao Prolog Playground, and an Application to Verification Tutorials

Authors: Daniela Ferreiro, José F. Morales, Salvador Abreu, Manuel V. Hermenegildo

Abstract: Active Logic Documents (ALD) are web pages which incorporate embedded Prolog engines that run locally within the browser. ALD offers both a very easy way to add click-to-run capabilities to any kind of teaching materials, independently of the tool used to generate them, as well as a tool-set for generating web-based materials with embedded examples and exercises. Both leverage on (components of)… ▽ More Active Logic Documents (ALD) are web pages which incorporate embedded Prolog engines that run locally within the browser. ALD offers both a very easy way to add click-to-run capabilities to any kind of teaching materials, independently of the tool used to generate them, as well as a tool-set for generating web-based materials with embedded examples and exercises. Both leverage on (components of) the Ciao Prolog Playground. We present a demonstration of the ALD approach and the Ciao Prolog Playground, as well as a recent extension to ALDs to facilitate the integration of other tools into the system for creating Hybrid Active Logic Documents (HALD). We also present a concrete application of these technologies to the creation of tutorials for a program verification tool. △ Less

Submitted 30 August, 2023; originally announced August 2023.

Comments: In Proceedings ICLP 2023, arXiv:2308.14898

Journal ref: EPTCS 385, 2023, pp. 324-329

Fifty Years of Prolog and Beyond

Authors: Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, Jose F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu, Giovanni Ciatto

Abstract: Both logic programming in general, and Prolog in particular, have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50 years, supported by many Prolog implementations. Many implementations are still actively developed, while new ones keep appearing. Often, the features added by diffe… ▽ More Both logic programming in general, and Prolog in particular, have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A large body of research has been gathered over the last 50 years, supported by many Prolog implementations. Many implementations are still actively developed, while new ones keep appearing. Often, the features added by different systems were motivated by the interdisciplinary needs of programmers and implementors, yielding systems that, while sharing the "classic" core language, and, in particular, the main aspects of the ISO-Prolog standard, also depart from each other in other aspects. This obviously poses challenges for code portability. The field has also inspired many related, but quite different languages that have created their own communities. This article aims at integrating and applying the main lessons learned in the process of evolution of Prolog. It is structured into three major parts. Firstly, we overview the evolution of Prolog systems and the community approximately up to the ISO standard, considering both the main historic developments and the motivations behind several Prolog implementations, as well as other logic programming languages influenced by Prolog. Then, we discuss the Prolog implementations that are most active after the appearance of the standard: their visions, goals, commonalities, and incompatibilities. Finally, we perform a SWOT analysis in order to better identify the potential of Prolog, and propose future directions along which Prolog might continue to add useful features, interfaces, libraries, and tools, while at the same time improving compatibility between implementations. △ Less

Submitted 14 March, 2022; v1 submitted 26 January, 2022; originally announced January 2022.

Comments: 87 pages, 2 figures. This article has been accepted for publication in Theory and Practice of Logic Programming (TPLP)

Parallel Logic Programming: A Sequel

Authors: Agostino Dovier, Andrea Formisano, Gopal Gupta, Manuel V. Hermenegildo, Enrico Pontelli, Ricardo Rocha

Abstract: Multi-core and highly-connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel log… ▽ More Multi-core and highly-connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel logic programming, published in 2001, has served since as a fundamental reference to researchers and developers. The contents are quite valid today, but at the same time the field has continued evolving at a fast pace in the years that have followed. Many of these achievements and ongoing research have been driven by the rapid pace of technological innovation, that has led to advances such as very large clusters, the wide diffusion of multi-core processors, the game-changing role of general-purpose graphic processing units, and the ubiquitous adoption of cloud computing. This has been paralleled by significant advances within logic programming, such as tabling, more powerful static analysis and verification, the rapid growth of Answer Set Programming, and in general, more mature implementations and systems. This survey provides a review of the research in parallel logic programming covering the period since 2001, thus providing a natural continuation of the previous survey. The goal of the survey is to serve not only as a reference for researchers and developers of logic programming systems, but also as engaging reading for anyone interested in logic and as a useful source for researchers in parallel systems outside logic programming. Under consideration in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 24 January, 2022; v1 submitted 22 November, 2021; originally announced November 2021.

Regular Path Clauses and Their Application in Solving Loops

Authors: Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro López-García, José F. Morales

Abstract: A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships between the values of variables, or program properties such as cost, on successive loop iterations. Recurrence solvers are capable of computing closed forms for some recurrences, thus deriving precise relationships capt… ▽ More A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships between the values of variables, or program properties such as cost, on successive loop iterations. Recurrence solvers are capable of computing closed forms for some recurrences, thus deriving precise relationships capturing the complete loop execution. However, many recurrences extracted from loops cannot be solved, due to their having multiple recursive cases or multiple arguments. In the literature, several techniques for approximating the solution of unsolvable recurrences have been proposed. The approach presented in this paper is to define transformations based on regular path expressions and loop counters that (i) transform multi-path loops to single-path loops, giving rise to recurrences with a single recursive case, and (ii) transform multi-argument recurrences to single-argument recurrences, thus enabling the use of recurrence solvers on the transformed recurrences. Using this approach, precise solutions can sometimes be obtained that are not obtained by approximation methods. △ Less

Submitted 9 September, 2021; originally announced September 2021.

Comments: In Proceedings HCVS 2021, arXiv:2109.03988

ACM Class: B.5.2

Journal ref: EPTCS 344, 2021, pp. 22-35

Analysis and Transformation of Constrained Horn Clauses for Program Verification

Authors: Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti

Abstract: This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialisation-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn claus… ▽ More This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialisation-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialisation and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques. △ Less

Submitted 2 August, 2021; originally announced August 2021.

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP)

VeriFly: On-the-fly Assertion Checking via Incrementality

Authors: Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, Victor Perez-Carrasco, Jose F. Morales, Pedro lopez-Garcia, Manuel V. Hermenegildo

Abstract: Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers this means being able to have relevant properties such as modes, types, determinacy, non-failure, sharing, constraints, cost, etc., checked and errors flagged without having to actually run the program. Such global static an… ▽ More Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers this means being able to have relevant properties such as modes, types, determinacy, non-failure, sharing, constraints, cost, etc., checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. In our static analysis and verification framework this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. We describe how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text -- the tool's VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the-shelf "on-the-fly" syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses. This paper is under consideration for acceptance in TPLP. △ Less

Submitted 17 August, 2021; v1 submitted 13 June, 2021; originally announced June 2021.

Comments: Paper presented at the 37th International Conference on Logic Programming (ICLP 2021), 16 pages

Report number: CLIP-1/2021.0

From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation

Authors: John P. Gallagher, Manuel Hermenegildo, Bishoksan Kafle, Maximiliano Klemen, Pedro López García, José Morales

Abstract: We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as constrained Horn clause programs directly encoding the rules. We then specialise an interpreter with respect to a given source program to achieve a compilation of the source language to Horn clauses (an instance of the first… ▽ More We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as constrained Horn clause programs directly encoding the rules. We then specialise an interpreter with respect to a given source program to achieve a compilation of the source language to Horn clauses (an instance of the first Futamura projection). The process is described in detail for an interpreter for a subset of C, directly encoding the rules of big-step operational semantics for C. A similar translation based on small-step semantics could be carried out, but we show an approach to obtaining a small-step representation using a linear interpreter for big-step Horn clauses. This interpreter is again specialised to achieve the translation from big-step to small-step style. The linear small-step program can be transformed back to a big-step non-linear program using a third interpreter. A regular path expression is computed for the linear program using Tarjan's algorithm, and this regular expression then guides an interpreter to compute a program path. The transformation is realised by specialisation of the path interpreter. In all of the transformation phases, we use an established partial evaluator and exploit standard logic program transformation to remove redundant data structures and arguments in predicates and rename predicates to make clear their link to statements in the original source program. △ Less

Submitted 6 August, 2020; originally announced August 2020.

Comments: In Proceedings VPT/HCVS 2020, arXiv:2008.02483

Journal ref: EPTCS 320, 2020, pp. 50-64

Towards a General Framework for Static Cost Analysis of Parallel Logic Programs

Authors: Maximiliano Klemen, Pedro Lopez-Garcia, John P. Gallagher, Jose F. Morales, Manuel V. Hermenegildo

Abstract: The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a wide variety of applications such as internet of things, cloud computing, health, transportation, and robots. At the same time, parallel computing, with (heterogeneous) multi-core platforms in particular, has become the… ▽ More The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a wide variety of applications such as internet of things, cloud computing, health, transportation, and robots. At the same time, parallel computing, with (heterogeneous) multi-core platforms in particular, has become the dominant paradigm in computer architecture. Predicting resource usage on such platforms poses a difficult challenge. Most work on static resource analysis has focused on sequential programs, and relatively little progress has been made on the analysis of parallel programs, or more specifically on parallel logic programs. We propose a novel, general, and flexible framework for setting up cost equations/relations which can be instantiated for performing resource usage analysis of parallel logic programs for a wide range of resources, platforms and execution models. The analysis estimates both lower and upper bounds on the resource usage of a parallel program (without executing it) as functions on input data sizes. In addition, it also infers other meaningful information to better exploit and assess the potential and actual parallelism of a system. We develop a method for solving cost relations involving the max function that arise in the analysis of parallel programs. Finally, we instantiate our general framework for the analysis of logic programs with Independent And-Parallelism, report on an implementation within the CiaoPP system, and provide some experimental results. To our knowledge, this is the first approach to the cost analysis of parallel logic programs. △ Less

Submitted 30 July, 2019; originally announced July 2019.

Comments: 19 pages, 3 tables; submitted to ICLP'19, accepted as technical communication

Report number: CLIP-1/2019.0

Computing Abstract Distances in Logic Programs

Authors: Ignacio Casso, Jose F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo

Abstract: Abstract interpretation is a well-established technique for performing static analyses of logic programs. However, choosing the abstract domain, widening, fixpoint, etc. that provides the best precision-cost trade-off remains an open problem. This is in a good part because of the challenges involved in measuring and comparing the precision of different analyses. We propose a new approach for measu… ▽ More Abstract interpretation is a well-established technique for performing static analyses of logic programs. However, choosing the abstract domain, widening, fixpoint, etc. that provides the best precision-cost trade-off remains an open problem. This is in a good part because of the challenges involved in measuring and comparing the precision of different analyses. We propose a new approach for measuring such precision, based on defining distances in abstract domains and extending them to distances between whole analyses of a given program, thus allowing comparing precision across different analyses. We survey and extend existing proposals for distances and metrics in lattices or abstract domains, and we propose metrics for some common domains used in logic program analysis, as well as extensions of those metrics to the space of whole program analysis. We implement those metrics within the CiaoPP framework and apply them to measure the precision of different analyses over both benchmarks and a realistic program. △ Less

Submitted 30 July, 2019; originally announced July 2019.

Comments: 21 pages, 8 figures; submitted to ICLP'19, accepted as technical communication

Report number: CLIP-2/2019.0

Multivariant Assertion-based Guidance in Abstract Interpretation

Authors: Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo

Abstract: Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic techniques have been studied to prevent precision loss, typically at the expense of larger resource consumption. In both cases (i.e., when analysis produces inaccurate results and when… ▽ More Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic techniques have been studied to prevent precision loss, typically at the expense of larger resource consumption. In both cases (i.e., when analysis produces inaccurate results and when resource consumption is too high), it is necessary to have some means for users to provide information to guide analysis and thus improve precision and/or performance. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance/context-sensitivity, and can handle different run-time semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating analysis. We also provide some formal results on the effects of such assertions on the analysis results. △ Less

Submitted 17 December, 2018; v1 submitted 15 August, 2018; originally announced August 2018.

Comments: Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)

Report number: LOPSTR/2018/29

An Approach to Static Performance Guarantees for Programs with Run-time Checks

Authors: Maximiliano Klemen, Nataliia Stulova, Pedro Lopez-Garcia, José F. Morales, Manuel V. Hermenegildo

Abstract: Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. This is specially true in dynamic languages such as Prolog. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). Several approaches have been proposed for… ▽ More Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. This is specially true in dynamic languages such as Prolog. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). Several approaches have been proposed for reducing such overhead, such as eliminating the checks that can statically be proved to always succeed, and/or optimizing the way in which the (remaining) checks are performed. However, there are cases in which it is not possible to remove all checks statically (e.g., open libraries which must check their interfaces, complex properties, unknown code, etc.) and in which, even after optimizations, these remaining checks still may introduce an unacceptable level of overhead. It is thus important for programmers to be able to determine the additional cost due to the run-time checks and compare it to some notion of admissible cost. The common practice used for estimating run-time checking overhead is profiling, which is not exhaustive by nature. Instead, we propose a method that uses static analysis to estimate such overhead, with the advantage that the estimations are functions parameterized by input data sizes. Unlike profiling, this approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input grows. Our method also extends an existing assertion verification framework to express "admissible" overheads, and statically and automatically checks whether the instrumented program conforms with such specifications. Finally, we present an experimental evaluation of our approach that suggests that our method is feasible and promising. △ Less

Submitted 6 April, 2018; originally announced April 2018.

Comments: 15 pages, 3 tables; submitted to ICLP'18, accepted as technical communication

Report number: CLIP-1/2018.0

Incremental and Modular Context-sensitive Analysis

Authors: Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo

Abstract: Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated within a few components, and it is desirable to reuse as much as possible previous analysis results. This has been achieved to date through incremental global analysis fixpoint algori… ▽ More Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated within a few components, and it is desirable to reuse as much as possible previous analysis results. This has been achieved to date through incremental global analysis fixpoint algorithms that achieve cost reductions at fine levels of granularity, such as changes in program lines. However, these fine-grained techniques are not directly applicable to modular programs, nor are they designed to take advantage of modular structures. This paper describes, implements, and evaluates an algorithm that performs efficient context-sensitive analysis incrementally on modular partitions of programs. The experimental results show that the proposed modular algorithm shows significant improvements, in both time and memory consumption, when compared to existing non-modular, fine-grain incremental analysis techniques. Furthermore, thanks to the proposed inter-modular propagation of analysis information, our algorithm also outperforms traditional modular analysis even when analyzing from scratch. △ Less

Submitted 18 December, 2020; v1 submitted 5 April, 2018; originally announced April 2018.

Comments: 56 pages, 27 figures. To be published in Theory and Practice of Logic Programming. v3 corresponds to the extended version of the ICLP2018 Technical Communication. v4 is the revised version submitted to Theory and Practice of Logic Programming. v5 (this one) is the final author version to be published in TPLP

Report number: CLIP-2/2018 version 4 (July 2019) ACM Class: D.2.4; F.3.1; I.2.2; I.2.3

Journal ref: Theory and Practice of Logic Programming 21 (2021) 196-243

Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption

Authors: Pedro Lopez-Garcia, Luthfi Darmawan, Maximiliano Klemen, Umer Liqat, Francisco Bueno, Manuel V. Hermenegildo

Abstract: Many applications require conformance with specifications that constrain the use of resources, such as execution time, energy, bandwidth, etc. We have presented a configurable framework for static resource usage verification where specifications can include lower and upper bound, data size-dependent resource usage functions. To statically check such specifications, our framework infers the same ty… ▽ More Many applications require conformance with specifications that constrain the use of resources, such as execution time, energy, bandwidth, etc. We have presented a configurable framework for static resource usage verification where specifications can include lower and upper bound, data size-dependent resource usage functions. To statically check such specifications, our framework infers the same type of resource usage functions, which safely approximate the actual resource usage of the program, and compares them against the specification. We review how this framework supports several languages and compilation output formats by translating them to an intermediate representation based on Horn clauses and using the configurability of the framework to describe the resource semantics of the input language. We provide a more detailed formalization and extend the framework so that both resource usage specification and analysis/verification output can include preconditions expressing intervals for the input data sizes for which assertions are applicable, proved, or disproved. Most importantly, we also extend the classes of functions that can be checked. We provide results from an implementation within the Ciao/CiaoPP framework, and report on a tool built by instantiating this framework for the verification of energy consumption specifications for imperative/embedded programs. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 12 March, 2018; originally announced March 2018.

Comments: Under consideration for publication in Theory and Practice of Logic Programming (TPLP)

Exploiting Term Hiding to Reduce Run-time Checking Overhead

Authors: Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo

Abstract: One of the most attractive features of untyped languages is the flexibility in term creation and manipulation. However, with such power comes the responsibility of ensuring the correctness of these operations. A solution is adding run-time checks to the program via assertions, but this can introduce overheads that are in many cases impractical. While static analysis can greatly reduce such overhea… ▽ More One of the most attractive features of untyped languages is the flexibility in term creation and manipulation. However, with such power comes the responsibility of ensuring the correctness of these operations. A solution is adding run-time checks to the program via assertions, but this can introduce overheads that are in many cases impractical. While static analysis can greatly reduce such overheads, the gains depend strongly on the quality of the information inferred. Reusable libraries, i.e., library modules that are pre-compiled independently of the client, pose special challenges in this context. We propose a technique which takes advantage of module systems which can hide a selected set of functor symbols to significantly enrich the shape information that can be inferred for reusable libraries, as well as an improved run-time checking approach that leverages the proposed mechanisms to achieve large reductions in overhead, closer to those of static languages, even in the reusable-library context. While the approach is general and system-independent, we present it for concreteness in the context of the Ciao assertion language and combined static/dynamic checking framework. Our method maintains the full expressiveness of the assertion language in this context. In contrast to other approaches it does not introduce the need to switch the language to a (static) type system, which is known to change the semantics in languages like Prolog. We also study the approach experimentally and evaluate the overhead reduction achieved in the run-time checks. △ Less

Submitted 15 October, 2017; v1 submitted 18 May, 2017; originally announced May 2017.

Comments: 26 pages, 10 figures, 2 tables; an extension of the paper version accepted to PADL'18 (includes proofs, extra figures and examples omitted due to space reasons)

ACM Class: D.1.6; D.2.4; D.2.11; D.3.3; F.3.1; F.3.2

A General Framework for Static Profiling of Parametric Resource Usage

Authors: Pedro Lopez-Garcia, Maximiliano Klemen, Umer Liqat, Manuel V. Hermenegildo

Abstract: Traditional static resource analyses estimate the total resource usage of a program, without executing it. In this paper we present a novel resource analysis whose aim is instead the static profiling of accumulated cost, i.e., to discover, for selected parts of the program, an estimate or bound of the resource usage accumulated in each of those parts. Traditional resource analyses are parametric i… ▽ More Traditional static resource analyses estimate the total resource usage of a program, without executing it. In this paper we present a novel resource analysis whose aim is instead the static profiling of accumulated cost, i.e., to discover, for selected parts of the program, an estimate or bound of the resource usage accumulated in each of those parts. Traditional resource analyses are parametric in the sense that the results can be functions on input data sizes. Our static profiling is also parametric, i.e., our accumulated cost estimates are also parameterized by input data sizes. Our proposal is based on the concept of cost centers and a program transformation that allows the static inference of functions that return bounds on these accumulated costs depending on input data sizes, for each cost center of interest. Such information is much more useful to the software developer than the traditional resource usage functions, as it allows identifying the parts of a program that should be optimized, because of their greater impact on the total cost of program executions. We also report on our implementation of the proposed technique using the CiaoPP program analysis framework, and provide some experimental results. This paper is under consideration for acceptance in TPLP. △ Less

Submitted 17 October, 2016; v1 submitted 9 August, 2016; originally announced August 2016.

Comments: Paper presented at the 32nd International Conference on Logic Programming (ICLP 2016), New York City, USA, 16-21 October 2016, 22 pages, LaTeX

Semantic Code Browsing

Authors: Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo

Abstract: Programmers currently enjoy access to a very high number of code repositories and libraries of ever increasing size. The ensuing potential for reuse is however hampered by the fact that searching within all this code becomes an increasingly difficult task. Most code search engines are based on syntactic techniques such as signature matching or keyword extraction. However, these techniques are inac… ▽ More Programmers currently enjoy access to a very high number of code repositories and libraries of ever increasing size. The ensuing potential for reuse is however hampered by the fact that searching within all this code becomes an increasingly difficult task. Most code search engines are based on syntactic techniques such as signature matching or keyword extraction. However, these techniques are inaccurate (because they basically rely on documentation) and at the same time do not offer very expressive code query languages. We propose a novel approach that focuses on querying for semantic characteristics of code obtained automatically from the code itself. Program units are pre-processed using static analysis techniques, based on abstract interpretation, obtaining safe semantic approximations. A novel, assertion-based code query language is used to express desired semantic characteristics of the code as partial specifications. Relevant code is found by comparing such partial specifications with the inferred semantics for program elements. Our approach is fully automatic and does not rely on user annotations or documentation. It is more powerful and flexible than signature matching because it is parametric on the abstract domain and properties, and does not require type definitions. Also, it reasons with relations between properties, such as implication and abstraction, rather than just equality. It is also more resilient to syntactic code differences. We describe the approach and report on a prototype implementation within the Ciao system. Under consideration for acceptance in TPLP. △ Less

Submitted 8 August, 2016; originally announced August 2016.

Comments: Paper presented at the 32nd International Conference on Logic Programming (ICLP 2016), New York City, USA, 16-21 October 2016, 15 pages, LaTeX, 4 PDF figures, 2 tables

Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)

Authors: Manuel V. Hermenegildo, Pedro Lopez-Garcia

Abstract: This volume constitutes the pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), held on 6-8th September 2016 in Edinburgh, Scotland UK, and co-located with the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016) and the 23rd Static Analysis Symposium (SAS 2016). After discussion at the sym… ▽ More This volume constitutes the pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), held on 6-8th September 2016 in Edinburgh, Scotland UK, and co-located with the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016) and the 23rd Static Analysis Symposium (SAS 2016). After discussion at the symposium papers will go through a second round of refereeing and selection for the formal proceedings. △ Less

Submitted 1 September, 2016; v1 submitted 8 August, 2016; originally announced August 2016.

Comments: Papers selected for presentation at LOPSTR 2016

ENTRA: Whole-Systems Energy Transparency

Authors: Kerstin Eder, John P. Gallagher, Pedro Lopez-Garcia, Henk Muller, Zorana Bankovic, Kyriakos Georgiou, Remy Haemmerle, Manuel V. Hermenegildo, Bishoksan Kafle, Steve Kerrison, Maja Kirkeby, Maximiliano Klemen, Xueliang Li, Umer Liqat, Jeremy Morse, Morten Rhiger, Mads Rosendahl

Abstract: Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient hardware can be designed, it is software that controls the hardware; for a given system the potential for energy savings is likely to be much greater at the higher levels of abstraction in the system stack. Thus the greatest savings are expected from energy-aware softw… ▽ More Promoting energy efficiency to a first class system design goal is an important research challenge. Although more energy-efficient hardware can be designed, it is software that controls the hardware; for a given system the potential for energy savings is likely to be much greater at the higher levels of abstraction in the system stack. Thus the greatest savings are expected from energy-aware software development, which is the vision of the EU ENTRA project. This article presents the concept of energy transparency as a foundation for energy-aware software development. We show how energy modelling of hardware is combined with static analysis to allow the programmer to understand the energy consumption of a program without executing it, thus enabling exploration of the design space taking energy into consideration. The paper concludes by summarising the current and future challenges identified in the ENTRA project. △ Less

Submitted 18 June, 2016; v1 submitted 13 June, 2016; originally announced June 2016.

Comments: Revised preprint submitted to MICPRO on 27 May 2016, 23 pages, 3 figures

Inferring Energy Bounds via Static Program Analysis and Evolutionary Modeling of Basic Blocks

Authors: Umer Liqat, Zorana Bankovic, Pedro Lopez-Garcia, Manuel V. Hermenegildo

Abstract: The ever increasing number and complexity of energy-bound devices (such as the ones used in Internet of Things applications, smart phones, and mission critical systems) pose an important challenge on techniques to optimize their energy consumption and to verify that they will perform their function within the available energy budget. In this work we address this challenge from the software point o… ▽ More The ever increasing number and complexity of energy-bound devices (such as the ones used in Internet of Things applications, smart phones, and mission critical systems) pose an important challenge on techniques to optimize their energy consumption and to verify that they will perform their function within the available energy budget. In this work we address this challenge from the software point of view and propose a novel parametric approach to estimating tight bounds on the energy consumed by program executions that are practical for their application to energy verification and optimization. Our approach divides a program into basic (branchless) blocks and estimates the maximal and minimal energy consumption for each block using an evolutionary algorithm. Then it combines the obtained values according to the program control flow, using static analysis, to infer functions that give both upper and lower bounds on the energy consumption of the whole program and its procedures as functions on input data sizes. We have tested our approach on (C-like) embedded programs running on the XMOS hardware platform. However, our method is general enough to be applied to other microprocessor architectures and programming languages. The bounds obtained by our prototype implementation can be tight while remaining on the safe side of budgets in practice, as shown by our experimental evaluation. △ Less

Submitted 22 September, 2017; v1 submitted 12 January, 2016; originally announced January 2016.

Comments: Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854). Improved version of the one presented at the HIP3ES 2016 workshop (v1): more experimental results (added benchmark to Table 1, added figure for new benchmark, added Table 3), improved Fig. 1, added Fig. 4

Report number: LOPSTR/2017/31

Towards Energy Consumption Verification via Static Analysis

Authors: Pedro Lopez-Garcia, Remy Haemmerle, Maximiliano Klemen, Umer Liqat, Manuel V. Hermenegildo

Abstract: In this paper we leverage an existing general framework for resource usage verification and specialize it for verifying energy consumption specifications of embedded programs. Such specifications can include both lower and upper bounds on energy usage, and they can express intervals within which energy usage is to be certified to be within such bounds. The bounds of the intervals can be given in g… ▽ More In this paper we leverage an existing general framework for resource usage verification and specialize it for verifying energy consumption specifications of embedded programs. Such specifications can include both lower and upper bounds on energy usage, and they can express intervals within which energy usage is to be certified to be within such bounds. The bounds of the intervals can be given in general as functions on input data sizes. Our verification system can prove whether such energy usage specifications are met or not. It can also infer the particular conditions under which the specifications hold. To this end, these conditions are also expressed as intervals of functions of input data sizes, such that a given specification can be proved for some intervals but disproved for others. The specifications themselves can also include preconditions expressing intervals for input data sizes. We report on a prototype implementation of our approach within the CiaoPP system for the XC language and XS1-L architecture, and illustrate with an example how embedded software developers can use this tool, and in particular for determining values for program parameters that ensure meeting a given energy budget while minimizing the loss in quality of service. △ Less

Submitted 31 December, 2015; originally announced December 2015.

Comments: Presented at HIP3ES, 2015 (arXiv: 1501.03064)

Report number: HIP3ES/2015/04 ACM Class: F.3.2; D.3.4; D.2.8

Inferring Parametric Energy Consumption Functions at Different Software Levels: ISA vs. LLVM IR

Authors: Umer Liqat, Kyriakos Georgiou, Steve Kerrison, Pedro Lopez-Garcia, John P. Gallagher, Manuel V. Hermenegildo, Kerstin Eder

Abstract: The static estimation of the energy consumed by program executions is an important challenge, which has applications in program optimization and verification, and is instrumental in energy-aware software development. Our objective is to estimate such energy consumption in the form of functions on the input data sizes of programs. We have developed a tool for experimentation with static analysis wh… ▽ More The static estimation of the energy consumed by program executions is an important challenge, which has applications in program optimization and verification, and is instrumental in energy-aware software development. Our objective is to estimate such energy consumption in the form of functions on the input data sizes of programs. We have developed a tool for experimentation with static analysis which infers such energy functions at two levels, the instruction set architecture (ISA) and the intermediate code (LLVM IR) levels, and reflects it upwards to the higher source code level. This required the development of a translation from LLVM IR to an intermediate representation and its integration with existing components, a translation from ISA to the same representation, a resource analyzer, an ISA-level energy model, and a mapping from this model to LLVM IR. The approach has been applied to programs written in the XC language running on XCore architectures, but is general enough to be applied to other languages. Experimental results show that our LLVM IR level analysis is reasonably accurate (less than 6.4% average error vs. hardware measurements) and more powerful than analysis at the ISA level. This paper provides insights into the trade-off of precision versus analyzability at these levels. △ Less

Submitted 4 November, 2015; originally announced November 2015.

Comments: 22 pages, 4 figures, 2 tables

ACM Class: F.3.2; D.3.4; D.2.8

Practical Run-time Checking via Unobtrusive Property Caching

Authors: Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo

Abstract: The use of annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are to be generated, has become frequent in dynamic programing languages. However, the frameworks proposed to support such run-time testing generally incur high time and/or space overheads over standard program execution. We present an approach for reducing this overhead that is… ▽ More The use of annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are to be generated, has become frequent in dynamic programing languages. However, the frameworks proposed to support such run-time testing generally incur high time and/or space overheads over standard program execution. We present an approach for reducing this overhead that is based on the use of memoization to cache intermediate results of check evaluation, avoiding repeated checking of previously verified properties. Compared to approaches that reduce checking frequency, our proposal has the advantage of being exhaustive (i.e., all tests are checked at all points) while still being much more efficient than standard run-time checking. Compared to the limited previous work on memoization, it performs the task without requiring modifications to data structure representation or checking code. While the approach is general and system-independent, we present it for concreteness in the context of the Ciao run-time checking framework, which allows us to provide an operational semantics with checks and caching. We also report on a prototype implementation and provide some experimental results that support that using a relatively small cache leads to significant decreases in run-time checking overhead. △ Less

Submitted 23 July, 2015; v1 submitted 21 July, 2015; originally announced July 2015.

Comments: 30 pages, 1 table, 170 figures; added appendix with plots; To appear in Theory and Practice of Logic Programming (TPLP), Proceedings of ICLP 2015

ACM Class: D.1.6; D.2.4; F.3.1; F.3.2

Journal ref: Theory and Practice of Logic Programming 15 (2015) 726-741

Proceedings of the Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES) 2015

Authors: Francisco Corbera, Andrés Rodríguez, Rafael Asenjo, Angeles Navarro, Antonio Vilches, Maria Garzaran, Ismat Chaib Draa, Jamel Tayeb, Smail Niar, Mikael Desertot, Daniel Gregorek, Robert Schmidt, Alberto Garcia-Ortiz, Pedro Lopez-Garcia, Rémy Haemmerlé, Maximiliano Klemen, Umer Liqat, Manuel V. Hermenegildo, Radim Vavřík, Albert Saà-Garriga, David Castells-Rufas, Jordi Carrabina

Abstract: Proceedings of the Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES) 2015. Amsterdam, January 21st. Collocated with HIPEAC 2015 Conference. Proceedings of the Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES) 2015. Amsterdam, January 21st. Collocated with HIPEAC 2015 Conference. △ Less

Submitted 13 January, 2015; originally announced January 2015.

Description and Optimization of Abstract Machines in a Dialect of Prolog

Authors: Jose F. Morales, Manuel Carro, Manuel Hermenegildo

Abstract: In order to achieve competitive performance, abstract machines for Prolog and related languages end up being large and intricate, and incorporate sophisticated optimizations, both at the design and at the implementation levels. At the same time, efficiency considerations make it necessary to use low-level languages in their implementation. This makes them laborious to code, optimize, and, especial… ▽ More In order to achieve competitive performance, abstract machines for Prolog and related languages end up being large and intricate, and incorporate sophisticated optimizations, both at the design and at the implementation levels. At the same time, efficiency considerations make it necessary to use low-level languages in their implementation. This makes them laborious to code, optimize, and, especially, maintain and extend. Writing the abstract machine (and ancillary code) in a higher-level language can help tame this inherent complexity. We show how the semantics of most basic components of an efficient virtual machine for Prolog can be described using (a variant of) Prolog. These descriptions are then compiled to C and assembled to build a complete bytecode emulator. Thanks to the high level of the language used and its closeness to Prolog, the abstract machine description can be manipulated using standard Prolog compilation and optimization techniques with relative ease. We also show how, by applying program transformations selectively, we obtain abstract machine implementations whose performance can match and even exceed that of state-of-the-art, highly-tuned, hand-crafted emulators. △ Less

Submitted 20 November, 2014; originally announced November 2014.

Comments: 56 pages, 46 figures, 5 tables, To appear in Theory and Practice of Logic Programming (TPLP)

ACM Class: D.1.6; D.3.3; D.3.4

Journal ref: Theory and Practice of Logic Programming 16 (2016) 1-58

Towards Assertion-based Debugging of Higher-Order (C)LP Programs

Authors: Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo

Abstract: Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers detect errors and validate programs. However, these assertion-based extensions to (C)LP have not been integrated well with higher order to date. Our work contribut… ▽ More Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers detect errors and validate programs. However, these assertion-based extensions to (C)LP have not been integrated well with higher order to date. Our work contributes to filling this gap by extending the assertion-based approach to error detection and program validation to the higher-order context, within (C)LP. It is based on an extension of properties and assertions as used in (C)LP in order to be able to fully describe arguments that are predicates. △ Less

Submitted 2 June, 2014; v1 submitted 14 May, 2014; originally announced May 2014.

Comments: 2 pages, to be published as a technical communication in the on-line addendum of the special issue(s) of the TPLP journal for ICLP14. To appear in Theory and Practice of Logic Programming (TPLP). arXiv admin note: substantial text overlap with arXiv:1404.4246; corrected the header publication info and submission, revision and acceptance dates

Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types

Authors: Alejandro Serrano, Pedro Lopez-Garcia, Manuel V. Hermenegildo

Abstract: We present a novel general resource analysis for logic programs based on sized types. Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic p… ▽ More We present a novel general resource analysis for logic programs based on sized types. Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic predicates. Using these sized types, the resource analysis can infer both lower and upper bounds on the resources used by all the procedures in a program as functions on input term (and subterm) sizes, overcoming limitations of existing resource analyses and enhancing their precision. Our new resource analysis has been developed within the abstract interpretation framework, as an extension of the sized types abstract domain, and has been integrated into the Ciao preprocessor, CiaoPP. The abstract domain operations are integrated with the setting up and solving of recurrence equations for inferring both size and resource usage functions. We show that the analysis is an improvement over the previous resource analysis present in CiaoPP and compares well in power to state of the art systems. △ Less

Submitted 16 May, 2014; originally announced May 2014.

Comments: To appear in Theory and Practice of Logic Programming (TPLP), improved version of arXiv:1308.3940 (which was conference version)

Journal ref: Theory and Practice of Logic Programming 14 (2014) 739-754

An Approach to Assertion-based Debugging of Higher-Order (C)LP Programs

Authors: Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo

Abstract: Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers detect errors and validate programs. However, these assertion-based extensions to (C)LP have not been integrated well with higher-order to date. This paper contrib… ▽ More Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers detect errors and validate programs. However, these assertion-based extensions to (C)LP have not been integrated well with higher-order to date. This paper contributes to filling this gap by extending the assertion-based approach to error detection and program validation to the higher-order context within (C)LP. We propose an extension of properties and assertions as used in (C)LP in order to be able to fully describe arguments that are predicates. The extension makes the full power of the assertion language available when describing higher-order arguments. We provide syntax and semantics for (higher-order) properties and assertions, as well as for programs which contain such assertions, including the notions of error and partial correctness and provide some formal results. We also discuss several alternatives for performing run-time checking of such programs. △ Less

Submitted 16 April, 2014; originally announced April 2014.

Comments: 24 pages, 1 figure. A 2-page extended abstract to be published as a technical communication in the on-line addendum of the special issue(s) of the TPLP journal for ICLP14

Report number: CLIP-1/2014.0 ACM Class: D.1.6; D.2.4; D.3.3; F.3.1; F.3.2

Towards an Abstract Domain for Resource Analysis of Logic Programs Using Sized Types

Authors: Alejandro Serrano, Pedro López-García, Manuel Hermenegildo

Abstract: We present a novel general resource analysis for logic programs based on sized types.Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic pr… ▽ More We present a novel general resource analysis for logic programs based on sized types.Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic predicates. Using these sized types, the resource analysis can infer both lower and upper bounds on the resources used by all the procedures in a program as functions on input term (and subterm) sizes, overcoming limitations of existing analyses and enhancing their precision. Our new resource analysis has been developed within the abstract interpretation framework, as an extension of the sized types abstract domain, and has been integrated into the Ciao preprocessor, CiaoPP. The abstract domain operations are integrated with the setting up and solving of recurrence equations for both, inferring size and resource usage functions. We show that the analysis is an improvement over the previous resource analysis present in CiaoPP and compares well in power to state of the art systems. △ Less

Submitted 19 August, 2013; originally announced August 2013.

Comments: Part of WLPE 2013 proceedings (arXiv:1308.2055)

Report number: WLPE/2013/5

The Ciao clp(FD) Library. A Modular CLP Extension for Prolog

Authors: Emilio Jesús Gallego Arias, Rémy Haemmerlé, Manuel V. Hermenegildo, José F. Morales

Abstract: We present a new free library for Constraint Logic Programming over Finite Domains, included with the Ciao Prolog system. The library is entirely written in Prolog, leveraging on Ciao's module system and code transformation capabilities in order to achieve a highly modular design without compromising performance. We describe the interface, implementation, and design rationale of each modular compo… ▽ More We present a new free library for Constraint Logic Programming over Finite Domains, included with the Ciao Prolog system. The library is entirely written in Prolog, leveraging on Ciao's module system and code transformation capabilities in order to achieve a highly modular design without compromising performance. We describe the interface, implementation, and design rationale of each modular component. The library meets several design goals: a high level of modularity, allowing the individual components to be replaced by different versions; high-efficiency, being competitive with other FD implementations; a glass-box approach, so the user can specify new constraints at different levels; and a Prolog implementation, in order to ease the integration with Ciao's code analysis components. The core is built upon two small libraries which implement integer ranges and closures. On top of that, a finite domain variable datatype is defined, taking care of constraint reexecution depending on range changes. These three libraries form what we call the FD kernel of the library. This FD kernel is used in turn to implement several higher-level finite domain constraints, specified using indexicals. Together with a labeling module this layer forms what we name \emph{the FD solver}. A final level integrates the clp(FD) paradigm with our FD solver. This is achieved using attributed variables and a compiler from the clp(FD) language to the set of constraints provided by the solver. It should be noted that the user of the library is encouraged to work in any of those levels as seen convenient: from writing a new range module to enriching the set of FD constraints by writing new indexicals. △ Less

Submitted 31 January, 2013; originally announced January 2013.

Comments: Appeared in CICLOPS 2012. 15 Pages, 5 Figures

Reversible Language Extensions and their Application in Debugging

Authors: Zoé Drey, José F. Morales, Manuel V. Hermenegildo

Abstract: A range of methodologies and techniques are available to guide the design and implementation of language extensions and domain-specific languages. A simple yet powerful technique is based on source-to-source transformations interleaved across the compilation passes of a base language. Despite being a successful approach, it has the main drawback that the input source code is lost in the process. W… ▽ More A range of methodologies and techniques are available to guide the design and implementation of language extensions and domain-specific languages. A simple yet powerful technique is based on source-to-source transformations interleaved across the compilation passes of a base language. Despite being a successful approach, it has the main drawback that the input source code is lost in the process. When considering the whole workflow of program development (warning and error reporting, debugging, or even program analysis), program translations are no more powerful than a glorified macro language. In this paper, we propose an augmented approach to language extensions for Prolog, where symbolic annotations are included in the target program. These annotations allow selectively reversing the translated code. We illustrate the approach by showing that coupling it with minimal extensions to a generic Prolog debugger allows us to provide users with a familiar, source-level view during the debugging of programs which use a variety of language extensions, such as functional notation, DCGs, or CLP{Q,R}. △ Less

Submitted 31 January, 2013; originally announced January 2013.

Comments: Appeared in CICLOPS 2012. 15 Pages, 7 Figures

Lightweight compilation of (C)LP to JavaScript

Authors: Jose F. Morales, Rémy Haemmerlé, Manuel Carro, Manuel V. Hermenegildo

Abstract: We present and evaluate a compiler from Prolog (and extensions) to JavaScript which makes it possible to use (constraint) logic programming to develop the client side of web applications while being compliant with current industry standards. Targeting JavaScript makes (C)LP programs executable in virtually every modern computing device with no additional software requirements from the point of vie… ▽ More We present and evaluate a compiler from Prolog (and extensions) to JavaScript which makes it possible to use (constraint) logic programming to develop the client side of web applications while being compliant with current industry standards. Targeting JavaScript makes (C)LP programs executable in virtually every modern computing device with no additional software requirements from the point of view of the user. In turn, the use of a very high-level language facilitates the development of high-quality, complex software. The compiler is a back end of the Ciao system and supports most of its features, including its module system and its rich language extension mechanism based on packages. We present an overview of the compilation process and a detailed description of the run-time system, including the support for modular compilation into separate JavaScript code. We demonstrate the maturity of the compiler by testing it with complex code such as a CLP(FD) library written in Prolog with attributed variables. Finally, we validate our proposal by measuring the performance of some LP and CLP(FD) benchmarks running on top of major JavaScript engines. △ Less

Submitted 10 October, 2012; originally announced October 2012.

ACM Class: D.3.4; D.1.6

Journal ref: Theory and Practice of Logic Programming, 12(4-5): 755-773, 2012

Parallel Backtracking with Answer Memoing for Independent And-Parallelism

Authors: Pablo Chico de Guzmán, Amadeo Casas, Manuel Carro, Manuel V. Hermenegildo

Abstract: Goal-level Independent and-parallelism (IAP) is exploited by scheduling for simultaneous execution two or more goals which will not interfere with each other at run time. This can be done safely even if such goals can produce multiple answers. The most successful IAP implementations to date have used recomputation of answers and sequentially ordered backtracking. While in principle simplifying the… ▽ More Goal-level Independent and-parallelism (IAP) is exploited by scheduling for simultaneous execution two or more goals which will not interfere with each other at run time. This can be done safely even if such goals can produce multiple answers. The most successful IAP implementations to date have used recomputation of answers and sequentially ordered backtracking. While in principle simplifying the implementation, recomputation can be very inefficient if the granularity of the parallel goals is large enough and they produce several answers, while sequentially ordered backtracking limits parallelism. And, despite the expected simplification, the implementation of the classic schemes has proved to involve complex engineering, with the consequent difficulty for system maintenance and extension, while still frequently running into the well-known trapped goal and garbage slot problems. This work presents an alternative parallel backtracking model for IAP and its implementation. The model features parallel out-of-order (i.e., non-chronological) backtracking and relies on answer memoization to reuse and combine answers. We show that this approach can bring significant performance advantages. Also, it can bring some simplification to the important engineering task involved in implementing the backtracking mechanism of previous approaches. △ Less

Submitted 24 July, 2011; originally announced July 2011.

Comments: 19 pages, 15 figures, uses tlp style

Journal ref: Theory and Practice of Logic Programming (2011) volume 11, issue 4-5, pages 555-574

An overview of Ciao and its design philosophy

Authors: M. V. Hermenegildo, F. Bueno, M. Carro, P. López-García, E. Mera, J. F. Morales, G. Puebla

Abstract: We provide an overall description of the Ciao multiparadigm programming system emphasizing some of the novel aspects and motivations behind its design and implementation. An important aspect of Ciao is that, in addition to supporting logic programming (and, in particular, Prolog), it provides the programmer with a large number of useful features from different programming paradigms and styles, and… ▽ More We provide an overall description of the Ciao multiparadigm programming system emphasizing some of the novel aspects and motivations behind its design and implementation. An important aspect of Ciao is that, in addition to supporting logic programming (and, in particular, Prolog), it provides the programmer with a large number of useful features from different programming paradigms and styles, and that the use of each of these features (including those of Prolog) can be turned on and off at will for each program module. Thus, a given module may be using, e.g., higher order functions and constraints, while another module may be using assignment, predicates, Prolog meta-programming, and concurrency. Furthermore, the language is designed to be extensible in a simple and modular way. Another important aspect of Ciao is its programming environment, which provides a powerful preprocessor (with an associated assertion language) capable of statically finding non-trivial bugs, verifying that programs comply with specifications, and performing many types of optimizations (including automatic parallelization). Such optimizations produce code that is highly competitive with other dynamic languages or, with the (experimental) optimizing compiler, even that of static languages, all while retaining the flexibility and interactive development of a dynamic language. This compilation architecture supports modularity and separate compilation throughout. The environment also includes a powerful auto-documenter and a unit testing framework, both closely integrated with the assertion system. The paper provides an informal overview of the language and program development environment. It aims at illustrating the design philosophy rather than at being exhaustive, which would be impossible in a single journal paper, pointing instead to previous Ciao literature. △ Less

Submitted 27 February, 2011; originally announced February 2011.

Comments: Number of pages: 30, Number of figures: 14, Number of tables: 0. Accepted for publication in TPLP (CUP)

Certificate size reduction in Abstraction-Carrying Code

Authors: Elvira Albert, Puri Arenas, Germán Puebla, Manuel Hermenegildo

Abstract: Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one ite… ▽ More Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. Interestingly, the fact that the reduced certificate omits (parts of) the abstraction has implications in the design of the checker. We provide the sufficient conditions which allow us to ensure that 1) if the checker succeeds in validating the certificate, then the certificate is valid for the program (correctness) and 2) the checker will succeed for any reduced certificate which is valid (completeness). Our approach has been implemented and benchmarked within the ciaopp system. The experimental results show that our proposal is able to greatly reduce the size of certificates in practice.To appear in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 13 October, 2010; originally announced October 2010.

Comments: 35 pages, 1 figure, 2 tables

Introduction to the 26th International Conference on Logic Programming Special Issue

Authors: Manuel Hermenegildo, Torsten Schaub

Abstract: This is the preface to the 26th International Conference on Logic Programming Special Issue This is the preface to the 26th International Conference on Logic Programming Special Issue △ Less

Submitted 10 August, 2010; originally announced August 2010.

Comments: 6 pages

Towards Parameterized Regular Type Inference Using Set Constraints

Authors: F. Bueno, J. Navas, M. Hermenegildo

Abstract: We propose a method for inferring \emph{parameterized regular types} for logic programs as solutions for systems of constraints over sets of finite ground Herbrand terms (set constraint systems). Such parameterized regular types generalize \emph{parametric} regular types by extending the scope of the parameters in the type definitions so that such parameters can relate the types of different pre… ▽ More We propose a method for inferring \emph{parameterized regular types} for logic programs as solutions for systems of constraints over sets of finite ground Herbrand terms (set constraint systems). Such parameterized regular types generalize \emph{parametric} regular types by extending the scope of the parameters in the type definitions so that such parameters can relate the types of different predicates. We propose a number of enhancements to the procedure for solving the constraint systems that improve the precision of the type descriptions inferred. The resulting algorithm, together with a procedure to establish a set constraint system from a logic program, yields a program analysis that infers tighter safe approximations of the success types of the program than previous comparable work, offering a new and useful efficiency vs. precision trade-off. This is supported by experimental results, which show the feasibility of our analysis. △ Less

Submitted 9 February, 2010; originally announced February 2010.

Journal ref: WLPE 2009 Proceedings

Efficient Local Unfolding with Ancestor Stacks

Authors: G. Puebla, E. Albert, M. Hermenegildo

Abstract: The most successful unfolding rules used nowadays in the partial evaluation of logic programs are based on well quasi orders (wqo) applied over (covering) ancestors, i.e., a subsequence of the atoms selected during a derivation. Ancestor (sub)sequences are used to increase the specialization power of unfolding while still guaranteeing termination and also to reduce the number of atoms for which… ▽ More The most successful unfolding rules used nowadays in the partial evaluation of logic programs are based on well quasi orders (wqo) applied over (covering) ancestors, i.e., a subsequence of the atoms selected during a derivation. Ancestor (sub)sequences are used to increase the specialization power of unfolding while still guaranteeing termination and also to reduce the number of atoms for which the wqo has to be checked. Unfortunately, maintaining the structure of the ancestor relation during unfolding introduces significant overhead. We propose an efficient, practical local unfolding rule based on the notion of covering ancestors which can be used in combination with a wqo and allows a stack-based implementation without losing any opportunities for specialization. Using our technique, certain non-leftmost unfoldings are allowed as long as local unfolding is performed, i.e., we cover depth-first strategies. △ Less

Submitted 20 November, 2009; originally announced November 2009.

Comments: Number of pages: 32 Number of figures: 7 Number of Tables: 3

A Program Transformation for Continuation Call-Based Tabled Execution

Authors: Pablo Chico de Guzman, Manuel Carro, Manuel V. Hermenegildo

Abstract: The advantages of tabled evaluation regarding program termination and reduction of complexity are well known --as are the significant implementation, portability, and maintenance efforts that some proposals (especially those based on suspension) require. This implementation effort is reduced by program transformation-based continuation call techniques, at some efficiency cost. However, the tradi… ▽ More The advantages of tabled evaluation regarding program termination and reduction of complexity are well known --as are the significant implementation, portability, and maintenance efforts that some proposals (especially those based on suspension) require. This implementation effort is reduced by program transformation-based continuation call techniques, at some efficiency cost. However, the traditional formulation of this proposal by Ramesh and Cheng limits the interleaving of tabled and non-tabled predicates and thus cannot be used as-is for arbitrary programs. In this paper we present a complete translation for the continuation call technique which, using the runtime support needed for the traditional proposal, solves these problems and makes it possible to execute arbitrary tabled programs. We present performance results which show that CCall offers a useful tradeoff that can be competitive with state-of-the-art implementations. △ Less

Submitted 25 January, 2009; originally announced January 2009.

Comments: Part of the proceedings of CICLOPS 2008

ACM Class: D.1.6, D.3.3

Towards Execution Time Estimation for Logic Programs via Static Analysis and Profiling

Authors: Edison Mera, Pedro Lopez-Garcia, German Puebla, Manuel Carro, Manuel Hermenegildo

Abstract: Effective static analyses have been proposed which infer bounds on the number of resolutions or reductions. These have the advantage of being independent from the platform on which the programs are executed and have been shown to be useful in a number of applications, such as granularity control in parallel execution. On the other hand, in distributed computation scenarios where platforms with d… ▽ More Effective static analyses have been proposed which infer bounds on the number of resolutions or reductions. These have the advantage of being independent from the platform on which the programs are executed and have been shown to be useful in a number of applications, such as granularity control in parallel execution. On the other hand, in distributed computation scenarios where platforms with different capabilities come into play, it is necessary to express costs in metrics that include the characteristics of the platform. In particular, it is specially interesting to be able to infer upper and lower bounds on actual execution times. With this objective in mind, we propose an approach which combines compile-time analysis for cost bounds with a one-time profiling of the platform in order to determine the values of certain parameters for a given platform. These parameters calibrate a cost model which, from then on, is able to compute statically time bound functions for procedures and to predict with a significant degree of accuracy the execution times of such procedures in the given platform. The approach has been implemented and integrated in the CiaoPP system. △ Less

Submitted 17 January, 2007; originally announced January 2007.

Comments: Paper presented at the 16th Workshop on Logic-based Methods in Programming Environments

A study of set-sharing analysis via cliques

Authors: Jorge Navas, Francisco Bueno, Manuel Hermenegildo

Abstract: We study the problem of efficient, scalable set-sharing analysis of logic programs. We use the idea of representing sharing information as a pair of abstract substitutions, one of which is a worst-case sharing representation called a clique set, which was previously proposed for the case of inferring pair-sharing. We use the clique-set representation for (1) inferring actual set-sharing informat… ▽ More We study the problem of efficient, scalable set-sharing analysis of logic programs. We use the idea of representing sharing information as a pair of abstract substitutions, one of which is a worst-case sharing representation called a clique set, which was previously proposed for the case of inferring pair-sharing. We use the clique-set representation for (1) inferring actual set-sharing information, and (2) analysis within a top-down framework. In particular, we define the abstract functions required by standard top-down analyses, both for sharing alone and also for the case of including freeness in addition to sharing. Our experimental evaluation supports the conclusion that, for inferring set-sharing, as it was the case for inferring pair-sharing, precision losses are limited, while useful efficiency gains are obtained. At the limit, the clique-set representation allowed analyzing some programs that exceeded memory capacity using classical sharing representations. △ Less

Submitted 25 August, 2005; originally announced August 2005.

Comments: 15 pages, 0 figures

A Generic Framework for the Analysis and Specialization of Logic Programs

Authors: German Puebla, Elvira Albert, Manuel Hermenegildo

Abstract: The relationship between abstract interpretation and partial deduction has received considerable attention and (partial) integrations have been proposed starting from both the partial deduction and abstract interpretation perspectives. In this work we present what we argue is the first fully described generic algorithm for efficient and precise integration of abstract interpretation and partial… ▽ More The relationship between abstract interpretation and partial deduction has received considerable attention and (partial) integrations have been proposed starting from both the partial deduction and abstract interpretation perspectives. In this work we present what we argue is the first fully described generic algorithm for efficient and precise integration of abstract interpretation and partial deduction. Taking as starting point state-of-the-art algorithms for context-sensitive, polyvariant abstract interpretation and (abstract) partial deduction, we present an algorithm which combines the best of both worlds. Key ingredients include the accurate success propagation inherent to abstract interpretation and the powerful program transformations achievable by partial deduction. In our algorithm, the calls which appear in the analysis graph are not analyzed w.r.t. the original definition of the procedure but w.r.t. specialized definitions of these procedures. Such specialized definitions are obtained by applying both unfolding and abstract executability. Our framework is parametric w.r.t. different control strategies and abstract domains. Different combinations of such parameters correspond to existing algorithms for program analysis and specialization. Simultaneously, our approach opens the door to the efficient computation of strictly more precise results than those achievable by each of the individual techniques. The algorithm is now one of the key components of the CiaoPP analysis and specialization system. △ Less

Submitted 24 August, 2005; originally announced August 2005.

Comments: In A. Serebrenik and S. Munoz-Hernandez (editors), Proceedings of the 15th Workshop on Logic-based methods in Programming Environments October 2005, Sitges. cs.PL/0508078

ACM Class: D.2.6

Distributed WWW Programming using (Ciao-)Prolog and the PiLLoW library

Authors: Daniel Cabeza, Manuel V. Hermenegildo

Abstract: We discuss from a practical point of view a number of issues involved in writing distributed Internet and WWW applications using LP/CLP systems. We describe PiLLoW, a public-domain Internet and WWW programming library for LP/CLP systems that we have designed in order to simplify the process of writing such applications. PiLLoW provides facilities for accessing documents and code on the WWW; pars… ▽ More We discuss from a practical point of view a number of issues involved in writing distributed Internet and WWW applications using LP/CLP systems. We describe PiLLoW, a public-domain Internet and WWW programming library for LP/CLP systems that we have designed in order to simplify the process of writing such applications. PiLLoW provides facilities for accessing documents and code on the WWW; parsing, manipulating and generating HTML and XML structured documents and data; producing HTML forms; writing form handlers and CGI-scripts; and processing HTML/XML templates. An important contribution of PiLLoW is to model HTML/XML code (and, thus, the content of WWW pages) as terms. The PiLLoW library has been developed in the context of the Ciao Prolog system, but it has been adapted to a number of popular LP/CLP systems, supporting most of its functionality. We also describe the use of concurrency and a high-level model of client-server interaction, Ciao Prolog's active modules, in the context of WWW programming. We propose a solution for client-side downloading and execution of Prolog code, using generic browsers. Finally, we also provide an overview of related work on the topic. △ Less

Submitted 16 December, 2003; originally announced December 2003.

Comments: 32 pages, 4 figures

ACM Class: D.1.3; D.1.6

Journal ref: Theory and Practice of Logic Programming, Vol 1(3), 2001, 251-282