Combining static analysis and profiling for estimating execution times

Effective static analyses have been proposed which infer bounds on the number of resolutions. 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 a given platform in order to determine the valúes of certain parameters for that 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 that concrete platform. The approach has been implemented and integrated in the CiaoPP system.

User-definable resource bounds analysis for logic programs

We present a static analysis that infers both upper and lower bounds on the usage that a logic program makes of a set of user-definable resources. The inferred bounds will in general be functions of input data sizes. A resource in our approach is a quite general, user-defined notion which associates a basic cost function with elementary operations. The analysis then derives the related (upper- and lower-bound) resource usage functions for all predicates in the program. We also present an assertion language which is used to define both such resources and resourcerelated properties that the system can then check based on the results of the analysis. We have performed some preliminary experiments with some concrete resources such as execution steps, bytes sent or received by an application, number of files left open, number of accesses to a datábase, number of calis to a procedure, number of asserts/retracts, etc. Applications of our analysis include resource consumption verification and debugging (including for mobile code), resource control in parallel/distributed computing, and resource-oriented specialization.

Towards execution time estimation for logic programs via static analysis and profiling

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 valúes of certain parameters for a given platform. These parameters calíbrate 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.

Resource bounds analysis.

We present a generic analysis that infers both upper and lower bounds on the usage that a program makes of a set of user-definable resources. The inferred bounds will in general be functions of input data sizes. A resource in our approach is a quite general, user-defined notion which associates a basic cost function with elementary operations. The analysis then derives the related (upper- and lower- bound) cost functions for all procedures in the program. We also present an assertion language which is used to define both such resources and resource-related properties that the system can then check based on the results of the analysis. We have performed some experiments with some concrete resource-related properties such as execution steps, bits sent or received by an application, number of arithmetic operations performed, number of calls to a procedure, number of transactions, etc. presenting the resource usage functions inferred and the times taken to perform the analysis. Applications of our analysis include resource consumption verification and debugging (including for mobile code), resource control in parallel/distributed computing, and resource-oriented specialization.

Combining static analysis and profiling for estimating execution times in logic programs

Effective static analyses have been proposed which allow inferring functions which bound the number of resolutions or reductions. These have the advantage of being independent from the platform on which the programs are executed and such bounds have been shown useful in a number of applications, such as granularity control in parallel execution. On the other hand, in certain distributed computation scenarios where different platforms come into play, with each platform having different capabilities, it is more interesting 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 time. With this objective in mind, we propose a method which allows inferring upper and lower bounds on the execution times of procedures of a program in a given execution platform. The approach combines compile-time cost bounds analysis with a one-time profiling of the platform in order to determine the values of certain constants for that platform. These constants 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.

Termination and cost analysis: Complexity and precision issues

The research in this thesis is related to static cost and termination analysis. Cost analysis aims at estimating the amount of resources that a given program consumes during the execution, and termination analysis aims at proving that the execution of a given program will eventually terminate. These analyses are strongly related, indeed cost analysis techniques heavily rely on techniques developed for termination analysis. Precision, scalability, and applicability are essential in static analysis in general. Precision is related to the quality of the inferred results, scalability to the size of programs that can be analyzed, and applicability to the class of programs that can be handled by the analysis (independently from precision and scalability issues). This thesis addresses these aspects in the context of cost and termination analysis, from both practical and theoretical perspectives. For cost analysis, we concentrate on the problem of solving cost relations (a form of recurrence relations) into closed-form upper and lower bounds, which is the heart of most modern cost analyzers, and also where most of the precision and applicability limitations can be found. We develop tools, and their underlying theoretical foundations, for solving cost relations that overcome the limitations of existing approaches, and demonstrate superiority in both precision and applicability. A unique feature of our techniques is the ability to smoothly handle both lower and upper bounds, by reversing the corresponding notions in the underlying theory. For termination analysis, we study the hardness of the problem of deciding termination for a speci�c form of simple loops that arise in the context of cost analysis. This study gives a better understanding of the (theoretical) limits of scalability and applicability for both termination and cost analysis.

Towards execution time estimation in abstract machine-based languages

Abstract machines provide a certain separation between platformdependent and platform-independent concerns in compilation. Many of the differences between architectures are encapsulated in the speciflc abstract machine implementation and the bytecode is left largely architecture independent. Taking advantage of this fact, we present a framework for estimating upper and lower bounds on the execution times of logic programs running on a bytecode-based abstract machine. Our approach includes a one-time, programindependent proflling stage which calculates constants or functions bounding the execution time of each abstract machine instruction. Then, a compile-time cost estimation phase, using the instruction timing information, infers expressions giving platform-dependent upper and lower bounds on actual execution time as functions of input data sizes for each program. Working at the abstract machine level makes it possible to take into account low-level issues in new architectures and platforms by just reexecuting the calibration stage instead of having to tailor the analysis for each architecture and platform. Applications of such predicted execution times include debugging/veriflcation of time properties, certiflcation of time properties in mobile code, granularity control in parallel/distributed computing, and resource-oriented specialization.

Towards data-aware resource analysis for service orchestrations

Compile-time program analysis techniques can be applied to Web service orchestrations to prove or check various properties. In particular, service orchestrations can be subjected to resource analysis, in which safe approximations of upper and lower resource usage bounds are deduced. A uniform analysis can be simultaneously performed for different generalized resources that can be directiy correlated with cost- and performance-related quality attributes, such as invocations of partners, network traffic, number of activities, iterations, and data accesses. The resulting safe upper and lower bounds do not depend on probabilistic assumptions, and are expressed as functions of size or length of data components from an initiating message, using a finegrained structured data model that corresponds to the XML-style of information structuring. The analysis is performed by transforming a BPEL-like representation of an orchestration into an equivalent program in another programming language for which the appropriate analysis tools already exist.

Interval-based resource usage verification: Formalization and prototype

In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program which are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach in this paper we provide a number of novel contributions: we present a full formalization, and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.

Novel system for bite-force sensing and monitoring based on magnetic eear field communication

Intraoral devices for bite-force sensing have several applications in odontology and maxillofacial surgery, as bite-force measurements provide additional information to help understand the characteristics of bruxism disorders and can also be of help for the evaluation of post-surgical evolution and for comparison of alternative treatments. A new system for measuring human bite forces is proposed in this work. This system has future applications for the monitoring of bruxism events and as a complement for its conventional diagnosis. Bruxism is a pathology consisting of grinding or tight clenching of the upper and lower teeth, which leads to several problems such as lesions to the teeth, headaches, orofacial pain and important disorders of the temporomandibular joint. The prototype uses a magnetic field communication scheme similar to low-frequency radio frequency identification (RFID) technology (NFC). The reader generates a low-frequency magnetic field that is used as the information carrier and powers the sensor. The system is notable because it uses an intra-mouth passive sensor and an external interrogator, which remotely records and processes information regarding a patient?s dental activity. This permits a quantitative assessment of bite-force, without requiring intra-mouth batteries, and can provide supplementary information to polysomnographic recordings, current most adequate early diagnostic method, so as to initiate corrective actions before irreversible dental wear appears. In addition to describing the system?s operational principles and the manufacture of personalized prototypes, this report will also demonstrate the feasibility of the system and results from the first in vitro and in vivo trials.

Analysis of service-oriented computing systems

La computación basada en servicios (Service-Oriented Computing, SOC) se estableció como un paradigma ampliamente aceptado para el desarollo de sistemas de software flexibles, distribuidos y adaptables, donde las composiciones de los servicios realizan las tareas más complejas o de nivel más alto, frecuentemente tareas inter-organizativas usando los servicios atómicos u otras composiciones de servicios. En tales sistemas, las propriedades de la calidad de servicio (Quality of Service, QoS), como la rapídez de procesamiento, coste, disponibilidad o seguridad, son críticas para la usabilidad de los servicios o sus composiciones en cualquier aplicación concreta. El análisis de estas propriedades se puede realizarse de una forma más precisa y rica en información si se utilizan las técnicas de análisis de programas, como el análisis de complejidad o de compartición de datos, que son capables de analizar simultáneamente tanto las estructuras de control como las de datos, dependencias y operaciones en una composición. El análisis de coste computacional para la composicion de servicios puede ayudar a una monitorización predictiva así como a una adaptación proactiva a través de una inferencia automática de coste computacional, usando los limites altos y bajos como funciones del valor o del tamaño de los mensajes de entrada. Tales funciones de coste se pueden usar para adaptación en la forma de selección de los candidatos entre los servicios que minimizan el coste total de la composición, basado en los datos reales que se pasan al servicio. Las funciones de coste también pueden ser combinadas con los parámetros extraídos empíricamente desde la infraestructura, para producir las funciones de los límites de QoS sobre los datos de entrada, cuales se pueden usar para previsar, en el momento de invocación, las violaciones de los compromisos al nivel de servicios (Service Level Agreements, SLA) potenciales or inminentes. En las composiciones críticas, una previsión continua de QoS bastante eficaz y precisa se puede basar en el modelado con restricciones de QoS desde la estructura de la composition, datos empiricos en tiempo de ejecución y (cuando estén disponibles) los resultados del análisis de complejidad. Este enfoque se puede aplicar a las orquestaciones de servicios con un control centralizado del flujo, así como a las coreografías con participantes multiples, siguiendo unas interacciones complejas que modifican su estado. El análisis del compartición de datos puede servir de apoyo para acciones de adaptación, como la paralelización, fragmentación y selección de los componentes, las cuales son basadas en dependencias funcionales y en el contenido de información en los mensajes, datos internos y las actividades de la composición, cuando se usan construcciones de control complejas, como bucles, bifurcaciones y flujos anidados. Tanto las dependencias funcionales como el contenido de información (descrito a través de algunos atributos definidos por el usuario) se pueden expresar usando una representación basada en la lógica de primer orden (claúsulas de Horn), y los resultados del análisis se pueden interpretar como modelos conceptuales basados en retículos. ABSTRACT Service-Oriented Computing (SOC) is a widely accepted paradigm for development of flexible, distributed and adaptable software systems, in which service compositions perform more complex, higher-level, often cross-organizational tasks using atomic services or other service compositions. In such systems, Quality of Service (QoS) properties, such as the performance, cost, availability or security, are critical for the usability of services and their compositions in concrete applications. Analysis of these properties can become more precise and richer in information, if it employs program analysis techniques, such as the complexity and sharing analyses, which are able to simultaneously take into account both the control and the data structures, dependencies, and operations in a composition. Computation cost analysis for service composition can support predictive monitoring and proactive adaptation by automatically inferring computation cost using the upper and lower bound functions of value or size of input messages. These cost functions can be used for adaptation by selecting service candidates that minimize total cost of the composition, based on the actual data that is passed to them. The cost functions can also be combined with the empirically collected infrastructural parameters to produce QoS bounds functions of input data that can be used to predict potential or imminent Service Level Agreement (SLA) violations at the moment of invocation. In mission-critical applications, an effective and accurate continuous QoS prediction, based on continuations, can be achieved by constraint modeling of composition QoS based on its structure, known data at runtime, and (when available) the results of complexity analysis. This approach can be applied to service orchestrations with centralized flow control, and choreographies with multiple participants with complex stateful interactions. Sharing analysis can support adaptation actions, such as parallelization, fragmentation, and component selection, which are based on functional dependencies and information content of the composition messages, internal data, and activities, in presence of complex control constructs, such as loops, branches, and sub-workflows. Both the functional dependencies and the information content (described using user-defined attributes) can be expressed using a first-order logic (Horn clause) representation, and the analysis results can be interpreted as a lattice-based conceptual models.

Dynamic gamma frequency feedback coupling between higher and lower order visual cortices underlies perceptual completion in humans

To perceive a coherent environment, incomplete or overlapping visual forms must be integrated into meaningful coherent percepts, a process referred to as ?Gestalt? formation or perceptual completion. Increasing evidence suggests that this process engages oscillatory neuronal activity in a distributed neuronal assembly. A separate line of evidence suggests that Gestalt formation requires top-down feedback from higher order brain regions to early visual cortex. Here we combine magnetoencephalography (MEG) and effective connectivity analysis in the frequency domain to specifically address the effective coupling between sources of oscillatory brain activity during Gestalt formation. We demonstrate that perceptual completion of two-tone ?Mooney? faces induces increased gamma frequency band power (55?71 Hz) in human early visual, fusiform and parietal cortices. Within this distributed neuronal assembly fusiform and parietal gamma oscillators are coupled by forward and backward connectivity during Mooney face perception, indicating reciprocal influences of gamma activity between these higher order visual brain regions. Critically, gamma band oscillations in early visual cortex are modulated by top-down feedback connectivity from both fusiform and parietal cortices. Thus, we provide a mechanistic account of Gestalt perception in which gamma oscillations in feature sensitive and spatial attention-relevant brain regions reciprocally drive one another and convey global stimulus aspects to local processing units at low levels of the sensory hierarchy by top-down feedback. Our data therefore support the notion of inverse hierarchical processing within the visual system underlying awareness of coherent percepts.

An elicitor isolated from smut teliospores (Sporisorium scitamineum) enhances lignin deposition on the cell wall on both sclerenchyma and xylem in sugarcane leaves

Sugarcane leaf shows the classical arrangement of cells which defines a C4 species. Vascular bundles consist of xylem, phloem and fibres, surrounded by an outer layer of sclereids and an inner ring of stone cells associated with the phloem. Some sclereids located below and above the vascular bundles act as docking cells and connect the vascular bundle to the internal surfaces of upper and lower layers of the epidermis. A compact mass of sclereids occupies the total internal volume of the leaf edge. Neither docking cells nor the internal mass of sclereids in the edge were markedly coloured by acriflavin or phloroglucinol, indicating the absence of lignin in their cell walls. However, such staining indicated that fibres of the vascular bundle and the external layer of sclereids were strongly lignified. Incubation of leaf discs with an elicitor produced by the pathogen Sporisorium scitamineum increased the thickness of the lignified cell walls of sclereids as well as the mid and small xylem vessels, as a possible mechanical defense response to the potential entry of the pathogen.

Occupational allergic multiorgan disease induced by wheat flour

Bakers are repeatedly exposed to wheat flour (WF) and may develop sensitization and occupational rhinoconjunctivitis and/or asthma to WF allergens.1 Several wheat proteins have been identified as causative allergens of occupational respiratory allergy in bakery workers.1 Testing of IgE reactivity in patients with different clinical profiles of wheat allergy (food allergy, wheat-dependent exercise-induced anaphylaxis, and baker's asthma) to salt-soluble and salt-insoluble protein fractions from WF revealed a high degree of heterogeneity in the recognized allergens. However, mainly salt-soluble proteins (albumins, globulins) seem to be associated with baker's asthma, and prolamins (gliadins, glutenins) with wheat-dependent exercise-induced anaphylaxis, whereas both protein fractions reacted to IgE from food-allergic patients.1 Notwithstanding, gliadins have also been incriminated as causative allergens in baker's asthma.2 We report on a 31-year-old woman who had been exposed to WF practically since birth because her family owned a bakery housed in the same home where they lived. She moved from this house when she was 25 years, but she continued working every day in the family bakery. In the last 8 years she had suffered from work-related nasal and ocular symptoms such as itching, watery eyes, sneezing, nasal stuffiness, and rhinorrhea. These symptoms markedly improved when away from work and worsened at work. In the last 5 years, she had also experienced dysphagia with frequent choking, especially when ingesting meats or cephalopods, which had partially improved with omeprazole therapy. Two years before referral to our clinic, she began to have dry cough and breathlessness, which she also attributed to her work environment. Upper and lower respiratory tract symptoms increased when sifting the WF and making the dough. The patient did not experience gastrointestinal symptoms with ingestion of cereal products. Skin prick test results were positive to grass (mean wheal, 6 mm), cypress (5 mm) and Russian thistle pollen (4 mm), WF (4 mm), and peach lipid transfer protein (6 mm) and were negative to rice flour, corn flour, profilin, mites, molds, and animal dander. Skin prick test with a homemade WF extract (10% wt/vol) was strongly positive (15 mm). Serologic tests yielded the following results: eosinophil cationic protein, 47 ?g/L; total serum IgE, 74 kU/L; specific IgE (ImmunoCAP; ThermoFisher, Uppsala, Sweden) to WF, 7.4 kU/L; barley flour, 1.24 kU/L; and corn, gluten, alpha-amylase, peach, and apple, less than 0.35 kU/L. Specific IgE binding to microarrayed purified WF allergens (WDAI-0.19, WDAI-0.53, WTAI-CM1, WTAI-CM2, WTAI-CM3, WTAI-CM16, WTAI-CM17, Tri a 14, profilin, ?-5-gliadin, Tri a Bd 36 and Tri a TLP, and gliadin and glutamine fractions) was assessed as described elsewhere.3 The patient's serum specifically recognized ?-5-gliadin and the gliadin fraction, and no IgE reactivity was observed to other wheat allergens. Spirometry revealed a forced vital capacity of 3.88 L (88%), an FEV1 of 3.04 L (87%), and FEV1/forced vital capacity of 83%. A methacholine inhalation test was performed following an abbreviated protocol,4 and the results were expressed as PD20 in cumulative dose (mg) of methacholine. Methacholine inhalation challenge test result was positive (0.24 mg cumulative dose) when she was working, and after a 3-month period away from work and with no visits to the bakery house, it gave a negative result. A chest x-ray was normal. Specific inhalation challenge test was carried out in the hospital laboratory by tipping WF from one tray to another for 15 minutes. Spirometry was performed at baseline and at 2, 5, 10, 15, 20, 30, 45, and 60 minutes after the challenge with WF. Peak expiratory flow was measured at baseline and then hourly over 24 hours (respecting sleeping time). A 12% fall in FEV1 was observed at 20 minutes and a 26% drop in peak expiratory flow at 9 hours after exposure to WF,

Using combined static analysis and profiling for logic program execution time estimation

Predicting statically the running time of programs has many applications ranging from task scheduling in parallel execution to proving the ability of a program to meet strict time constraints. A starting point in order to attack this problem is to infer the computational complexity of such programs (or fragments thereof). This is one of the reasons why the development of static analysis techniques for inferring cost-related properties of programs (usually upper and/or lower bounds of actual costs) has received considerable attention.