Búsqueda avanzada

Resultados de búsqueda para abstract interpretation

Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP

CiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming. In this adaptation, the tabling engine drives the fixpoint computation, while the constraint solver handles the LUB of the abstract substitutions of different clauses. That simplifies the code and improves performance, since termination, dependencies, and some crucial operations (e.g., branch switching and resumption) are directly handled by the tabling engine. Determining whether the fixpoint has been reached uses semantic equivalence, which can decide that two syntactically different abstract substitutions represent the same element in the abstract domain. Therefore, the tabling analyzer can reuse answers in more cases than an analyzer using syntactical equality. This helps achieve better performance, even taking into account the additional cost associated to these checks. Our implementation is based on the TCLP framework available in Ciao Prolog and is one-third the size of the initial fixpoint implementation in CiaoPP. Its performance has been evaluated by analyzing several programs using different abstract domains.

The full paper has been presented at the 35th International Conference on Logic Programming (ICLP 2019), Las Cruces, USA, September 20-25, 2019 [1].

Autores: Joaquín Arias / Manuel Carro / 
Palabras Clave: abstract interpretation - CiaoPP - constraints - PLAI - Prolog - Tabling

Static Performance Guarantees for Programs with Run-time Checks

Instrumenting programs for performing runtime checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. This is especially true in dynamic languages such as Prolog. However, such runtime checks inevitably introduce runtime overhead (in execution time, memory, energy, etc.). Several approaches have been proposed for reducing this 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 may still introduce an unacceptable level of overhead. It is thus important for programmers to be able to determine the additional cost due to the runtime checks and compare it to some notion of admissible cost. The common practice used for estimating runtime 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.

Autores: Maximiliano Klemen / Nataliia Stulova / Pedro Lopez-Garcia / Manuel V. Hermenegildo / José Morales / 
Palabras Clave: abstract interpretation - Assertions - Constraint Logic Programming - Program analysis - Resource Usage Analysis - Run-time Checks

Abstract Diagnosis for Timed Concurrent Constraint programs Abstract

This short paper is a summary of the published paper [CTV11] where a general framework for the debugging of tccp programs is defined. To this end, a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems was presented. In order to effectively implement the technique, we also provided an abstract semantics.

Autores: M. Comini / L. Titolo / A. Villanueva / 
Palabras Clave: abstract diagnosis - abstract interpretation - concurrent constraint paradigm - denotational semantics

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada