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

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: **

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

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

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: **

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: **

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

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

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

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.

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.