Global flow analysis as a practical compilation tool

This paper addresses the issue of the practicality of global flow analysis in logic program compilation, in terms of speed of the analysis, precisión, and usefulness of the information obtained. To this end, design and implementation aspects are discussed for two practical abstract interpretation-based flow analysis systems: MA , the MCC And-parallel Analyzer and Annotator; and Ms, an experimental mode inference system developed for SB-Prolog. The paper also provides performance data obtained (rom these implementations and, as an example of an application, a study of the usefulness of the mode information obtained in reducing run-time checks in independent and-parallelism.Based on the results obtained, it is concluded that the overhead of global flow analysis is not prohibitive, while the results of analysis can be quite precise and useful.

On the practicality of global flow analysis of logic programs

This paper addresses the issue of the practicality of global flow analysis in logic program compilation, in terms of both speed and precision of analysis. It discusses design and implementation aspects of two practical abstract interpretation-based flow analysis systems: MA3, the MOO Andparallel Analyzer and Annotator; and Ms, an experimental mode inference system developed for SB-Prolog. The paper also provides performance data obtained from these implementations. Based on these results, it is concluded that the overhead of global flow analysis is not prohibitive, while the results of analysis can be quite precise and useful.

Data-Flow analysis of prolog programs with extra-logical features

Abstract interpretation-based data-flow analysis of logic programs is at this point relatively well understood from the point of view of general frameworks and abstract domains. On the other hand, comparatively little attention has been given to the problems which arise when analysis of a full, practical dialect of the Prolog language is attempted, and only few solutions to these problems have been proposed to date. Such problems relate to dealing correctly with all builtins, including meta-logical and extra-logical predicates, with dynamic predicates (where the program is modified during execution), and with the absence of certain program text during compilation. Existing proposals for dealing with such issues generally restrict in one way or another the classes of programs which can be analyzed if the information from analysis is to be used for program optimization. This paper attempts to fill this gap by considering a full dialect of Prolog, essentially following the recently proposed ISO standard, pointing out the problems that may arise in the analysis of such a dialect, and proposing a combination of known and novel solutions that together allow the correct analysis of arbitrary programs using the full power of the language.

Global analysis of standard prolog programs

Abstract interpretation-based data-flow analysis of logic programs is, at this point, relatively well understood from the point of view of general frameworks and abstract domains. On the other hand, comparatively little attention has been given to the problems which arise when analysis of a full, practical dialect of the Prolog language is attempted, and only few solutions to these problems have been proposed to date. Existing proposals generally restrict in one way or another the classes of programs which can be analyzed. This paper attempts to fill this gap by considering a full dialect of Prolog, essentially the recent ISO standard, pointing out the problems that may arise in the analysis of such a dialect, and proposing a combination of known and novel solutions that together allow the correct analysis of arbitrary programs which use the full power of the language.

Programming with global analysis

Global data-flow analysis of (constraint) logic programs, which is generally based on abstract interpretation [7], is reaching a comparatively high level of maturity. A natural question is whether it is time for its routine incorporation in standard compilers, something which, beyond a few experimental systems, has not happened to date. Such incorporation arguably makes good sense only if: • the range of applications of global analysis is large enough to justify the additional complication in the compiler, and • global analysis technology can deal with all the features of "practical" languages (e.g., the ISO-Prolog built-ins) and "scales up" for large programs. We present a tutorial overview of a number of concepts and techniques directly related to the issues above, with special emphasis on the first one. In particular, we concéntrate on novel uses of global analysis during program development and debugging, rather than on the more traditional application área of program optimization. The idea of using abstract interpretation for validation and diagnosis has been studied in the context of imperative programming [2] and also of logic programming. The latter work includes issues such as using approximations to reduce the burden posed on programmers by declarative debuggers [6, 3] and automatically generating and checking assertions [4, 5] (which includes the more traditional type checking of strongly typed languages, such as Gódel or Mercury [1, 8, 9]) We also review some solutions for scalability including modular analysis, incremental analysis, and widening. Finally, we discuss solutions for dealing with meta-predicates, side-effects, delay declarations, constraints, dynamic predicates, and other such features which may appear in practical languages. In the discussion we will draw both from the literature and from our experience and that of others in the development and use of the CIAO system analyzer. In order to emphasize the practical aspects of the solutions discussed, the presentation of several concepts will be illustrated by examples run on the CIAO system, which makes extensive use of global analysis and assertions.

Effectiveness of abstract interpretation in automatic parallelization: a case study in logic programming

We report on a detailed study of the application and effectiveness of program analysis based on abstract interpretation to automatic program parallelization. We study the case of parallelizing logic programs using the notion of strict independence. We first propose and prove correct a methodology for the application in the parallelization task of the information inferred by abstract interpretation, using a parametric domain. The methodology is generic in the sense of allowing the use of different analysis domains. A number of well-known approximation domains are then studied and the transformation into the parametric domain defined. The transformation directly illustrates the relevance and applicability of each abstract domain for the application. Both local and global analyzers are then built using these domains and embedded in a complete parallelizing compiler. Then, the performance of the domains in this context is assessed through a number of experiments. A comparatively wide range of aspects is studied, from the resources needed by the analyzers in terms of time and memory to the actual benefits obtained from the information inferred. Such benefits are evaluated both in terms of the characteristics of the parallelized code and of the actual speedups obtained from it. The results show that data flow analysis plays an important role in achieving efficient parallelizations, and that the cost of such analysis can be reasonable even for quite sophisticated abstract domains. Furthermore, the results also offer significant insight into the characteristics of the domains, the demands of the application, and the trade-offs involved.

Approximate Relational Reasoning for Probabilistic Programs

La seguridad verificada es una metodología para demostrar propiedades de seguridad de los sistemas informáticos que se destaca por las altas garantías de corrección que provee. Los sistemas informáticos se modelan como programas probabilísticos y para probar que verifican una determinada propiedad de seguridad se utilizan técnicas rigurosas basadas en modelos matemáticos de los programas. En particular, la seguridad verificada promueve el uso de demostradores de teoremas interactivos o automáticos para construir demostraciones completamente formales cuya corrección es certificada mecánicamente (por ordenador). La seguridad verificada demostró ser una técnica muy efectiva para razonar sobre diversas nociones de seguridad en el área de criptografía. Sin embargo, no ha podido cubrir un importante conjunto de nociones de seguridad “aproximada”. La característica distintiva de estas nociones de seguridad es que se expresan como una condición de “similitud” entre las distribuciones de salida de dos programas probabilísticos y esta similitud se cuantifica usando alguna noción de distancia entre distribuciones de probabilidad. Este conjunto incluye destacadas nociones de seguridad de diversas áreas como la minería de datos privados, el análisis de flujo de información y la criptografía. Ejemplos representativos de estas nociones de seguridad son la indiferenciabilidad, que permite reemplazar un componente idealizado de un sistema por una implementación concreta (sin alterar significativamente sus propiedades de seguridad), o la privacidad diferencial, una noción de privacidad que ha recibido mucha atención en los últimos años y tiene como objetivo evitar la publicación datos confidenciales en la minería de datos. La falta de técnicas rigurosas que permitan verificar formalmente este tipo de propiedades constituye un notable problema abierto que tiene que ser abordado. En esta tesis introducimos varias lógicas de programa quantitativas para razonar sobre esta clase de propiedades de seguridad. Nuestra principal contribución teórica es una versión quantitativa de una lógica de Hoare relacional para programas probabilísticos. Las pruebas de correción de estas lógicas son completamente formalizadas en el asistente de pruebas Coq. Desarrollamos, además, una herramienta para razonar sobre propiedades de programas a través de estas lógicas extendiendo CertiCrypt, un framework para verificar pruebas de criptografía en Coq. Confirmamos la efectividad y aplicabilidad de nuestra metodología construyendo pruebas certificadas por ordendor de varios sistemas cuyo análisis estaba fuera del alcance de la seguridad verificada. Esto incluye, entre otros, una meta-construcción para diseñar funciones de hash “seguras” sobre curvas elípticas y algoritmos diferencialmente privados para varios problemas de optimización combinatoria de la literatura reciente. ABSTRACT The verified security methodology is an emerging approach to build high assurance proofs about security properties of computer systems. Computer systems are modeled as probabilistic programs and one relies on rigorous program semantics techniques to prove that they comply with a given security goal. In particular, it advocates the use of interactive theorem provers or automated provers to build fully formal machine-checked versions of these security proofs. The verified security methodology has proved successful in modeling and reasoning about several standard security notions in the area of cryptography. However, it has fallen short of covering an important class of approximate, quantitative security notions. The distinguishing characteristic of this class of security notions is that they are stated as a “similarity” condition between the output distributions of two probabilistic programs, and this similarity is quantified using some notion of distance between probability distributions. This class comprises prominent security notions from multiple areas such as private data analysis, information flow analysis and cryptography. These include, for instance, indifferentiability, which enables securely replacing an idealized component of system with a concrete implementation, and differential privacy, a notion of privacy-preserving data mining that has received a great deal of attention in the last few years. The lack of rigorous techniques for verifying these properties is thus an important problem that needs to be addressed. In this dissertation we introduce several quantitative program logics to reason about this class of security notions. Our main theoretical contribution is, in particular, a quantitative variant of a full-fledged relational Hoare logic for probabilistic programs. The soundness of these logics is fully formalized in the Coq proof-assistant and tool support is also available through an extension of CertiCrypt, a framework to verify cryptographic proofs in Coq. We validate the applicability of our approach by building fully machine-checked proofs for several systems that were out of the reach of the verified security methodology. These comprise, among others, a construction to build “safe” hash functions into elliptic curves and differentially private algorithms for several combinatorial optimization problems from the recent literature.

Urban wind energy: empirical optimization of high-rise building roof shape for the wind energy exploitation

El programa Europeo HORIZON2020 en Futuras Ciudades Inteligentes establece como objetivo que el 20% de la energía eléctrica sea generada a partir de fuentes renovables. Este objetivo implica la necesidad de potenciar la generación de energía eólica en todos los ámbitos. La energía eólica reduce drásticamente las emisiones de gases de efecto invernadero y evita los riesgos geo-políticos asociados al suministro e infraestructuras energéticas, así como la dependencia energética de otras regiones. Además, la generación de energía distribuida (generación en el punto de consumo) presenta significativas ventajas en términos de elevada eficiencia energética y estimulación de la economía. El sector de la edificación representa el 40% del consumo energético total de la Unión Europea. La reducción del consumo energético en este área es, por tanto, una prioridad de acuerdo con los objetivos "20-20-20" en eficiencia energética. La Directiva 2010/31/EU del Parlamento Europeo y del Consejo de 19 de mayo de 2010 sobre el comportamiento energético de edificaciones contempla la instalación de sistemas de suministro energético a partir de fuentes renovables en las edificaciones de nuevo diseño. Actualmente existe una escasez de conocimiento científico y tecnológico acerca de la geometría óptima de las edificaciones para la explotación de la energía eólica en entornos urbanos. El campo tecnológico de estudio de la presente Tesis Doctoral es la generación de energía eólica en entornos urbanos. Específicamente, la optimization de la geometría de las cubiertas de edificaciones desde el punto de vista de la explotación del recurso energético eólico. Debido a que el flujo del viento alrededor de las edificaciones es exhaustivamente investigado en esta Tesis empleando herramientas de simulación numérica, la mecánica de fluidos computacional (CFD en inglés) y la aerodinámica de edificaciones son los campos científicos de estudio. El objetivo central de esta Tesis Doctoral es obtener una geometría de altas prestaciones (u óptima) para la explotación de la energía eólica en cubiertas de edificaciones de gran altura. Este objetivo es alcanzado mediante un análisis exhaustivo de la influencia de la forma de la cubierta del edificio en el flujo del viento desde el punto de vista de la explotación energética del recurso eólico empleando herramientas de simulación numérica (CFD). Adicionalmente, la geometría de la edificación convencional (edificio prismático) es estudiada, y el posicionamiento adecuado para los diferentes tipos de aerogeneradores es propuesto. La compatibilidad entre el aprovechamiento de las energías solar fotovoltaica y eólica también es analizado en este tipo de edificaciones. La investigación prosigue con la optimización de la geometría de la cubierta. La metodología con la que se obtiene la geometría óptima consta de las siguientes etapas: - Verificación de los resultados de las geometrías previamente estudiadas en la literatura. Las geometrías básicas que se someten a examen son: cubierta plana, a dos aguas, inclinada, abovedada y esférica. - Análisis de la influencia de la forma de las aristas de la cubierta sobre el flujo del viento. Esta tarea se lleva a cabo mediante la comparación de los resultados obtenidos para la arista convencional (esquina sencilla) con un parapeto, un voladizo y una esquina curva. - Análisis del acoplamiento entre la cubierta y los cerramientos verticales (paredes) mediante la comparación entre diferentes variaciones de una cubierta esférica en una edificación de gran altura: cubierta esférica estudiada en la literatura, cubierta esférica integrada geométricamente con las paredes (planta cuadrada en el suelo) y una cubierta esférica acoplada a una pared cilindrica. El comportamiento del flujo sobre la cubierta es estudiado también considerando la posibilidad de la variación en la dirección del viento incidente. - Análisis del efecto de las proporciones geométricas del edificio sobre el flujo en la cubierta. - Análisis del efecto de la presencia de edificaciones circundantes sobre el flujo del viento en la cubierta del edificio objetivo. Las contribuciones de la presente Tesis Doctoral pueden resumirse en: - Se demuestra que los modelos de turbulencia RANS obtienen mejores resultados para la simulación del viento alrededor de edificaciones empleando los coeficientes propuestos por Crespo y los propuestos por Bechmann y Sórensen que empleando los coeficientes estándar. - Se demuestra que la estimación de la energía cinética turbulenta del flujo empleando modelos de turbulencia RANS puede ser validada manteniendo el enfoque en la cubierta de la edificación. - Se presenta una nueva modificación del modelo de turbulencia Durbin k — e que reproduce mejor la distancia de recirculación del flujo de acuerdo con los resultados experimentales. - Se demuestra una relación lineal entre la distancia de recirculación en una cubierta plana y el factor constante involucrado en el cálculo de la escala de tiempo de la velocidad turbulenta. Este resultado puede ser empleado por la comunidad científica para la mejora del modelado de la turbulencia en diversas herramientas computacionales (OpenFOAM, Fluent, CFX, etc.). - La compatibilidad entre las energías solar fotovoltaica y eólica en cubiertas de edificaciones es analizada. Se demuestra que la presencia de los módulos solares provoca un descenso en la intensidad de turbulencia. - Se demuestran conflictos en el cambio de escala entre simulaciones de edificaciones a escala real y simulaciones de modelos a escala reducida (túnel de viento). Se demuestra que para respetar las limitaciones de similitud (número de Reynolds) son necesarias mediciones en edificaciones a escala real o experimentos en túneles de viento empleando agua como fluido, especialmente cuando se trata con geometrías complejas, como es el caso de los módulos solares. - Se determina el posicionamiento más adecuado para los diferentes tipos de aerogeneradores tomando en consideración la velocidad e intensidad de turbulencia del flujo. El posicionamiento de aerogeneradores es investigado en las geometrías de cubierta más habituales (plana, a dos aguas, inclinada, abovedada y esférica). - Las formas de aristas más habituales (esquina, parapeto, voladizo y curva) son analizadas, así como su efecto sobre el flujo del viento en la cubierta de un edificio de gran altura desde el punto de vista del aprovechamiento eólico. - Se propone una geometría óptima (o de altas prestaciones) para el aprovechamiento de la energía eólica urbana. Esta optimización incluye: verificación de las geometrías estudiadas en el estado del arte, análisis de la influencia de las aristas de la cubierta en el flujo del viento, estudio del acoplamiento entre la cubierta y las paredes, análisis de sensibilidad del grosor de la cubierta, exploración de la influencia de las proporciones geométricas de la cubierta y el edificio, e investigación del efecto de las edificaciones circundantes (considerando diferentes alturas de los alrededores) sobre el flujo del viento en la cubierta del edificio objetivo. Las investigaciones comprenden el análisis de la velocidad, la energía cinética turbulenta y la intensidad de turbulencia en todos los casos. ABSTRACT The HORIZON2020 European program in Future Smart Cities aims to have 20% of electricity produced by renewable sources. This goal implies the necessity to enhance the wind energy generation, both with large and small wind turbines. Wind energy drastically reduces carbon emissions and avoids geo-political risks associated with supply and infrastructure constraints, as well as energy dependence from other regions. Additionally, distributed energy generation (generation at the consumption site) offers significant benefits in terms of high energy efficiency and stimulation of the economy. The buildings sector represents 40% of the European Union total energy consumption. Reducing energy consumption in this area is therefore a priority under the "20-20-20" objectives on energy efficiency. The Directive 2010/31/EU of the European Parliament and of the Council of 19 May 2010 on the energy performance of buildings aims to consider the installation of renewable energy supply systems in new designed buildings. Nowadays, there is a lack of knowledge about the optimum building shape for urban wind energy exploitation. The technological field of study of the present Thesis is the wind energy generation in urban environments. Specifically, the improvement of the building-roof shape with a focus on the wind energy resource exploitation. Since the wind flow around buildings is exhaustively investigated in this Thesis using numerical simulation tools, both computational fluid dynamics (CFD) and building aerodynamics are the scientific fields of study. The main objective of this Thesis is to obtain an improved (or optimum) shape of a high-rise building for the wind energy exploitation on the roof. To achieve this objective, an analysis of the influence of the building shape on the behaviour of the wind flow on the roof from the point of view of the wind energy exploitation is carried out using numerical simulation tools (CFD). Additionally, the conventional building shape (prismatic) is analysed, and the adequate positions for different kinds of wind turbines are proposed. The compatibility of both photovoltaic-solar and wind energies is also analysed for this kind of buildings. The investigation continues with the buildingroof optimization. The methodology for obtaining the optimum high-rise building roof shape involves the following stages: - Verification of the results of previous building-roof shapes studied in the literature. The basic shapes that are compared are: flat, pitched, shed, vaulted and spheric. - Analysis of the influence of the roof-edge shape on the wind flow. This task is carried out by comparing the results obtained for the conventional edge shape (simple corner) with a railing, a cantilever and a curved edge. - Analysis of the roof-wall coupling by testing different variations of a spherical roof on a high-rise building: spherical roof studied in the litera ture, spherical roof geometrically integrated with the walls (squared-plant) and spherical roof with a cylindrical wall. The flow behaviour on the roof according to the variation of the incident wind direction is commented. - Analysis of the effect of the building aspect ratio on the flow. - Analysis of the surrounding buildings effect on the wind flow on the target building roof. The contributions of the present Thesis can be summarized as follows: - It is demonstrated that RANS turbulence models obtain better results for the wind flow around buildings using the coefficients proposed by Crespo and those proposed by Bechmann and S0rensen than by using the standard ones. - It is demonstrated that RANS turbulence models can be validated for turbulent kinetic energy focusing on building roofs. - A new modification of the Durbin k — e turbulence model is proposed in order to obtain a better agreement of the recirculation distance between CFD simulations and experimental results. - A linear relationship between the recirculation distance on a flat roof and the constant factor involved in the calculation of the turbulence velocity time scale is demonstrated. This discovery can be used by the research community in order to improve the turbulence modeling in different solvers (OpenFOAM, Fluent, CFX, etc.). - The compatibility of both photovoltaic-solar and wind energies on building roofs is demonstrated. A decrease of turbulence intensity due to the presence of the solar panels is demonstrated. - Scaling issues are demonstrated between full-scale buildings and windtunnel reduced-scale models. The necessity of respecting the similitude constraints is demonstrated. Either full-scale measurements or wind-tunnel experiments using water as a medium are needed in order to accurately reproduce the wind flow around buildings, specially when dealing with complex shapes (as solar panels, etc.). - The most adequate position (most adequate roof region) for the different kinds of wind turbines is highlighted attending to both velocity and turbulence intensity. The wind turbine positioning was investigated for the most habitual kind of building-roof shapes (flat, pitched, shed, vaulted and spherical). - The most habitual roof-edge shapes (simple edge, railing, cantilever and curved) were investigated, and their effect on the wind flow on a highrise building roof were analysed from the point of view of the wind energy exploitation. - An optimum building-roof shape is proposed for the urban wind energy exploitation. Such optimization includes: state-of-the-art roof shapes test, analysis of the influence of the roof-edge shape on the wind flow, study of the roof-wall coupling, sensitivity analysis of the roof width, exploration of the aspect ratio of the building-roof shape and investigation of the effect of the neighbouring buildings (considering different surrounding heights) on the wind now on the target building roof. The investigations comprise analysis of velocity, turbulent kinetic energy and turbulence intensity for all the cases.