Búsqueda avanzada

El autor Manuel Carro ha publicado 13 artículo(s):

1 - A Haskell Implementation of a Rule-Based Program Transformation for C Programs

Obtaining good performance when programming heterogeneous computing platforms poses significant challenges for the programmer. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code is transformed into a functionally equivalent one better suited for a given platform. The transformation rules are formalized in a domain-specific language (STML) that takes care of the syntactic and semantic conditions required to apply a given transformation. STML rules are compiled into Haskell function definitions that operate at AST level. Program properties, to be matched with rule conditions, can be automatically inferred or, alternatively, stated as annotations in the source code. Early experimental results are described.

Autores: Salvador Tamarit / Guillermo Vigueras / Manuel Carro / Julio Mariño / 
Palabras Clave:

2 - Lightweight compilation of (C)LP to JavaScript

We present and evaluate a compiler from Prolog (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 extension mechanism. 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.

Autores: Jose F. Morales / Rémy Haemmerlé / Manuel Carro / Manuel V. Hermenegildo / 
Palabras Clave: Ciao - Implementation of Prolog - JavaScript - Logic Programming System - Modules - Prolog - Web

3 - A General Implementation Framework for Tabled CLP

This is a summary of [PCHS12], where a framework to combine tabling evaluation [TS86, War92] and constraint logic programming [JM94] is described (TCLP). This combination has been studied previously from a theoretical point of view [Tom97, Cod95], where it is shown that the constraint domain needs to offer projection and entailment checking operations in order to ensure completeness w.r.t. the declarative semantics. However, existing TCLP frameworks and implementations lack a complete treatment of constraint projection and / or entailment. The novelty of our proposal is that we present a complete implementation framework for TCLP, independent from the constraint solver, which can use either precise or approximate projection and entailment, possibly with optimizations.

Autores: Pablo Chico de Guzmán / Manuel Carro / Manuel V. Hermenegildo / Peter Stuckey / 
Palabras Clave: Constraint Logic Programming - Implementation - Performance - Tabling

4 - Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations (extended abstract)

Quality of Service (QoS) attributes, such as execution time, availability, or cost, are critical for the usability of Web services. This in particular applies to service compositions, which are commonly used for implementing more complex, higher level, and/or cross-organizational tasks by assembling loosely-coupled individual service components (often provided and controlled by third parties). The QoS attributes of service compositions depend on the QoS attributes of the service components, as well as on environmental factors and the actual data being handled, and are usually regulated by means of Service-Level Agreements (SLAs), which define the permissible boundaries for the values of the related properties. Predicting whether an SLA will be violated for a given executing instance of a service composition is therefore very important. Such a prediction can be used for preventing or mitigating the consequences of SLA violations ahead of time.
We propose a method whereby constraints that model SLA conformance and violation are derived at any given point of the execution of a service composition. These constraints are generated using the structure of the composition and properties of the component services, which can be either known or measured empirically. Violation of these constraints means that the corresponding scenario is unfeasible, while satisfaction gives values for the constrained variables (start / end times for activities, or number of loop iterations) which make the scenario possible. These results can be used to perform optimized service matching or trigger preventive adaptation or healing.

Autores: Dragan Ivanovic / Manuel Carro / Manuel Hermenegildo / 
Palabras Clave:

5 - Towards a Semantics-Aware Code Transformation Toolchain for Heterogeneous Systems

Obtaining good performance when programming heterogeneous computing platforms poses significant challenges. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code with semantic annotations is transformed into functionally equivalent code better suited for a given platform. The transformation steps are represented as rules which can be fired when certain syntactic and semantic conditions are fulfilled. These rules are not hard-wired into the rewriting engine: they are written in a C-like language and are automatically processed and incorporated by the rewriting engine. That makes it possible for end-users to add their own rules or to provide sets of rules which are adapted to certain specific domains or purposes.

Autores: Salvador Tamarit  /  Julio Mariño / Guillermo Vigueras  / Manuel Carro / 
Palabras Clave:

6 - Description and Evaluation of a Generic Design to Integrate CLP and Tabled Execution (Trabajo de alto nivel)

Logic programming systems with tabling and constraints (TCLP, tabled constraint logic
programming) have been shown to be more expressive and in some cases more efficient
than those featuring only either tabling or constraints. Previous implementations of TCLP
systems which use entailment to determine call / answer subsumption did not provide a
simple, uniform, and well-documented interface to facilitate the integration of additional
constraint solvers in existing tabling systems, which would increase the application range of
TCLP. We present the design and an experimental evaluation of Mod TCLP, a framework
which eases this integration. Mod TCLP views the constraints solver as a client of the tabling
system. The tabling system is generic w.r.t. the constraint solver and only requires a clear,
small interface from the latter. We validate our design by integrating four constraint solvers:
a re-engineered version of a previously existing constraint solver for difference constraints,
written in C; the standard versions of Holzbauer’s CLP(Q) and CLP(R), written in Prolog;
and a new constraint solver for equations over finite lattices. We evaluate the performance
of our framework in several benchmarks using the aforementioned constraint solvers. All
the development work and evaluation was done in Ciao Prolog.

Autores: Joaquín Arias / Manuel Carro / 
Palabras Clave: constraints - Implementation - Interface - Prolog - Tabling

7 - Constraint Answer Set Programming without Grounding (Trabajo ya publicado)

Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward as the grounding phase, present in most ASP systems, removes variables and the links among them, and also causes a combinatorial explosion in the size of the program. This has led CASP systems to devise several methods to overcome this issue: restricting the constraint domains (e.g., discrete instead of dense), where constraints can appear, or the type (or number) of models that can be returned. In this paper we propose to incorporate constraints into s(ASP), a goal-directed, top-down execution model which implements ASP while retaining logical variables both during execution and in the answer sets. The resulting model, s(CASP), can constrain variables that (as in CLP) are kept during the execution and in the answer sets. s(CASP) inherits and generalizes the execution model of s(ASP) while parameterizing the constraint solver. We describe this novel execution model and show, through several examples, the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other ASP systems with constraints. We also report improved performance w.r.t. other very mature, highly optimized ASP systems in some benchmarks.

Autores: Joaquín Arias / Manuel Carro / Kyle Marple / Elmer Salazar / Gopal Gupta / 
Palabras Clave: constraints - goal-directed evaluation - predicate - stable model

8 - Modeling Systems and Proving their Correctness with Event-B and Rodin (Tutorial)

Event-B is a formal development method. It can be used to model and verify correctness of sequential, concurrent, and reactive systems. It uses (infinite) discrete transition systems to capture how the model evolves and first-order logic and typed set theory to express the desirable properties of the system. The proofs that these properties hold are performed using sequent calculus. There are deduction rules specific for useful theories. Event-B is however is not restricted to classical set-theoretical notations and the sequent calculus: it includes notations for defining transitions over states of the model which resembles a programming language, and a rich mathematical toolkit (including operations and relations on sets and functions) to build complex models easily.

Autores: Manuel Carro / 
Palabras Clave: Correctness by Construction - Formal proofs - Rigorous software development

9 -

10 -

12 - Modeling and Reasoning in Event Calculus Using Constraint Answer Set Programming

Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of continuous change in dense domains (e.g., time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query driven, top-down execution model for predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be modeled in s(CASP) and how its expressiveness makes it pos- sible to perform deductive and abductive reasoning tasks in domains featuring, for example, constraints involving dense time and fluents.

Autores: Joaquín Arias / Manuel Carro / 
Palabras Clave: Answer Set Programming - constraints - Event Calculus - Top-down execution

13 - 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