Дисертації з теми "Compiler theory"

The Planguages project is the birthplace of the Planguage programmingapproach, which is designed to alleviate the task of writing parallelprograms and harness massively parallel computers and networks of workstations. Planguage has two existing translators, Parallel C (PC) and Pfortran,which is used for their base languages, C and Fortran77. The translatorswork with MPI (Message Passing Interface) for communications. SOS(ipStreams, Overlapping and Shortcutting), a function library that supportsthe three named functionalities, can be used to further optimize parallel algorithms. This project is the next step in the continuing project of updatingthe PC Compiler. The goal is to test the viability of using “shortcutting”functions. Parallel programs with the ability to shortcut can be generatedby the updated version of the PC Compiler. In addition, this project introducesthe ability of the PC Compiler to translate a race condition intoa non-deterministic solution. This document explores different phases of the project in detail. Thefollowing phases are included: software design, algorithm design, analysis,and results. The deliverables, source code, and diagrams are included asAppendices.

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Un compilateur de protocoles est un outil qui genere a partir d'une specification formelle d'un protocole une implementation. Les compilateurs de protocoles produisent generalement du code de qualite mediocre en terme de vitesse d'execution et de taille du code et sont, pour cette raison, peu utilises. Dans cette these, nous montrons qu'en utilisant une approche synchrone et en optimisant le code genere, il est possible de compiler des specifications formelles en des implementations tres performantes. Nous avons developpe un compilateur de protocoles qui utilise ces deux techniques. Ce compilateur prend en entree une specification modulaire du protocole ecrite dans le langage synchrone esterel. La specification est compilee en un automate sequentiel par le compilateur esterel dans un format intermediaire (le format oc). L'automate est alors optimise et transforme en une implementation c par notre optimisateur de protocoles, appele hippco. Hippco ameliore les performances du code et reduit sa taille en optimisant simultanement la vitesse d'execution du chemin commun et la taille du chemin rare. Nous evaluons les performances des implementations de notre compilateur en specifiant le protocole tcp et en comparant les performances de l'implementation automatiquement generee avec celle d'une version manuelle derivee de l'implementation standard bsd. Les resultats sont tres encourageants. Le code genere par hippco execute moins d'instructions et utilise le cache d'instructions et le pipelining plus efficacement que le code bsd tout en ayant une taille de code raisonnable

Dynamically Typed Assembly Language (D-TAL) is not only a lightweight and effective solution to the gap generated by the drop in security produced by the translation of high-level language instructions to low-level language instructions, but it considerably eases up the burden generated by the level of complexity required to implement typed assembly languages statically. Although there are tradeoffs between the static and dynamic approaches, focusing on a dynamic approach leads to simpler, easier to reason about, and more feasible ways to understand deployment of types over monomorphically-typed or untyped intermediate languages. On this occasion, DISM, a simple but powerful and mature untyped assembly language, is extended by the addition of type annotations (on memory and registers) to produce an instance of D-TAL. Strong-DISM, the resulting language, statically, lends itself to simpler analysis about type access and security as the correlation between datatypes and instructions with their respective memory and registers becomes simpler to observe; while dynamically, it disallows operations and further eliminates conditions that from high level languages could be used to violate/circumvent security.

Mobile devices connected to cloud based services are becoming a mainstream method of delivery up-to-date and context aware information to users. Connecting mobile applications to cloud service require significant developer effort. Yet this communication code usually follows certain patterns, varying accordingly to the specific type of data sent and received from the server. By analyzing the causes of theses variations, we can create a system that can automate the code creation for communication from a mobile device to a cloud server. To automate code creation, a general pattern must extracted. This general solution can then be applied to any database configuration. Automating this process frees up valuable development time, allowing developers to make other parts of the application and/or backend service a better experience for the end user.

Static analysis tools can aid programmers by reporting potential programming mistakes prior to the execution of a program. Funqual is a static analysis tool that reads C++17 code ``in the wild'' and checks that the function call graph follows a set of rules which can be defined by the user. This sort of analysis can help the programmer to avoid errors such as accidentally calling blocking functions in time-sensitive contexts or accidentally allocating memory in heap-sensitive environments. To accomplish this, we create a type system whereby functions can be given user-defined type qualifiers and where users can define their own restrictions on the call graph based on these type qualifiers. We demonstrate that this tool, when used with hand-crafted rules, can catch certain types of errors which commonly occur in the wild. We claim that this tool can be used in a production setting to catch certain kinds of errors in code before that code is even run.

This thesis explores modalities in two hagiographical collections from the late Middle Ages; the Legenda Aurea and the Gilte Legende by drawing inspiration from post-colonial hybridity theories.. It conducts a close textual analysis by studying the use of pronouns in five saints’ legends where female saints transcend traditional gender identities and become men, and focuses on how they transcend, live as men, and die. The study concludes that the use of pronouns is fluid in the Latin Legenda Aurea, while the Middle English Gilte Legende has more female pronouns and additions to the texts where the female identity of the saints is emphasised. This is interpreted as a sign of the feminisation of religious language in Europe during the late Middle Ages, and viewed parallel with the increase of holy women at that time. By doing this, it underlines the importance of new words and concepts when describing and understanding medieval views on gender.

O ChipCflow é o projeto de uma ferramenta para execução de algoritmos utilizando o modelo a fluxo de dados dinâmico em hardware reconfigurável. Tem como principal objetivo utilizar o modelo de arquitetura a fluxo de dados, associado ao conceito de arquiteturas reconfiguráveis, para acelerar programas de aplicação escritos em C. Essa aceleração vai acontecer nas partes mais intensas de processamento (exemplo: loops), através da execução direta em hardware, aproveitando ao máximo o paralelismo considerado natural do modelo a fluxo de dados. O módulo de conversão C em grafo a fluxo de dados, desenvolvido neste trabalho de doutoramento, é parte fundamental no desenvolvimento do projeto ChipCflow e se trata de um pré-compilador C que gera código VHDL para os operadores a fluxo de dados a partir de módulos do programa de aplicação escrito originalmente em C. É possível considerar como principal resultado dessa tese, a implementação de algoritmos a partir de uma linguagem C em grafo a fluxo de dados no modelo proposto no projeto ChipCflow, onde os operadores a fluxo de dados são os já tradicionalmente conhecidos, e até mesmo a forma de interconexão também, entretanto a forma de abordar essa implementação, em VHDL, e na forma de fluxo de dados dinâmico, torna o modelo proposto, tanto para o hardware como para o compilador, uma característica única existente até o momento.
ChipCflow is a tool for algorithms execution using a data dynamic flow in reconfigurable hardware. The main purpose of the work is to use the data flow architecture model, associated to the concept of reconfigurable architectures, to speed up C written applications. The program acceleration happens in the most intensive processing parts (example: loops), through direct hardware execution, using to advantage of the natural parallelism of the data flow model. The C conversion module in data flow graph is the basic part in the development of the ChipCflow project and the specific objective of the developed work. In this work we present detais of the C precompiler that generates VHDL code for the data flow operators modules of the written program of the original application in C. It is possible to consider as the main result of this thesis, the implementation of algorithms from a C language in the data flow graph model proposed in the project ChipCflow, where the operators to the data stream are typically already known, and even the way interconnection too, but how to approach the implementation in VHDL, and as a dynamic data flow, makes the proposed model for both the hardware and the compiler, a feature only available so far.

This thesis presents the ideas underlying a computer program that takes as input a schematic of a mechanical or hydraulic power transmission system, plus specifications and a utility function, and returns catalog numbers from predefined catalogs for the optimal selection of components implementing the design. Unlike programs for designing single components or systems, the program provides the designer with a high level "language" in which to compose new designs. It then performs some of the detailed design process. The process of "compilation" is based on a formalization of quantitative inferences about hierarchically organized sets of artifacts and operating conditions. This allows the design compilation without the exhaustive enumeration of alternatives.

Data-flow analysis is an integral part of any aggressive optimizing compiler. We propose a framework for improving the precision of data-flow analysis in the presence of complex control-flow. We initially perform data-flow analysis to determine those control-flow merges which cause the loss in data-flow analysis precision. The control-flow graph of the program is then restructured such that performing data-flow analysis on the resulting restructured graph gives more precise results. The proposed framework is both simple, involving the familiar notion of product automata, and also general, since it is applicable to any forward or backward data-flow analysis. Apart from proving that our restructuring process is correct, we also show that restructuring is effective in that it necessarily leads to more optimization opportunities. Furthermore, the framework handles the trade-off between the increase in data-flow precision and the code size increase inherent in the restructuring. We show that determining an optimal restructuring is NP-hard, and propose and evaluate a greedy heuristic. The framework has been implemented in the Scale research compiler, and instantiated for the specific problems of Constant Propagation and Liveness analysis. On the SPECINT 2000 benchmark suite we observe an average speedup of 4% in the running times over Wegman-Zadeck conditional constant propagation algorithm and 2% over a purely path profile guided approach for Constant Propagation. For the problem of Liveness analysis, we see an average speedup of 0.8% in the running times over the baseline implementation.

Zhang, Qirun.
Thesis (Ph.D.)--Chinese University of Hong Kong, 2013.
Includes bibliographical references (leaves 170-186).
Electronic reproduction. Hong Kong : Chinese University of Hong Kong, [2012] System requirements: Adobe Acrobat Reader. Available via World Wide Web.
Abstracts also in Chinese.

Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.
Dentro de las teorías fundacionales de la matemática se encuentran la Teoría de Conjuntos y la Teoría de Tipos. La primera es bien conocida en la comunidad matemática; la teoría de tipos además de ser una posible fundación, es una base para lenguajes de programación lo suficientemente expresivos para enunciar teoremas, escribir sus pruebas y que su corrección sea verificada automáticamente. Esta tesis resume tres trabajos independientes pero relacionados entre sí. El primero consiste en el desarrollo de una metodología para definir compiladores correctos por construcción mediante el uso de tipos dependientes. Gracias a la expresividad de estos sistemas de tipos refinamos los lenguajes fuente y destino con su semántica; el tipo de la función de compilación es exactamente la preservación de la semántica. Matemáticamente podemos concebir los lenguajes como álgebras de términos de una signatura y al compilador como el homomorfismo inducido por la interpretación de una signatura en la otra. Esto nos llevó a formalizar en Agda una librería para Álgebra Universal Heterogénea, incluyendo las principales definiciones y resultados básicos, un sistema deductivo para un cálculo ecuacional y las nociones de morfismos entre signaturas y álgebras reducto. El último aporte de la tesis surge del estudio de uno de los problemas más famosos en la teoría de conjuntos: la independencia de la hipótesis del continuo (CH) respecto a la teoría ZFC. Gödel y Cohen demostraron, respectivamente, que no puede refutarse ni probarse CH en ZFC. Cohen desarrolló para ello la técnica de Forcing, que es la única manera conocida para extender modelos de ZFC. Si bien este desarrollo constituye uno de los avances más grandes en teoría de conjuntos, no existe hasta el momento ninguna formalización de Forcing en asistentes de prueba. Como parte de este doctorado hemos comenzado la formalización en el asistente Isabelle/ZF de la técnica de Forcing, llegando a probar que la extensión genérica satisface varios axiomas de ZF.
Set Theory and Type Theory are known as Foundations of Mathematics. The first one is well known by mathematicians; Type Theory, besides being a foundation, is the basis for programming languages expressive enough to state theorems, write their proofs and verify their correctness automatically. This thesis summarizes three works. The first one consists of the development of a methodology to define correct-by-construction compilers, using dependent types. Thanks to the expressiveness of these type systems, we refine the syntax of source and target languages by adding information of semantics at type level; then, the type of the compiler function expresses the property of correctness. We can conceive the languages as term algebras of a signature, and the compiler as the homomorphism induced by the interpretation of a signature in other. Hence we formalized in the Agda proof assistant a library of Heterogeneous Universal Algebra, including main definitions and basic results, a deductive system for equational calculus and notions of morphisms between signatures and reduct algebras. The last contribution of this thesis is motivated by the study of one of the most famous problems in set theory: the independence of the continuum hypothesis (CH) with respect to the ZFC theory. Gödel and Cohen showed that CH cannot be refuted or proven. In his work, Cohen developed the technique of forcing, the only known way to extend models of ZFC. Despite the importance of forcing in set theory, there was no mechanization in proof assistants. Our last work consists of the first steps of a complete formalization of forcing in the Isabelle proof assistant.
Gunther, Emmanuel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina.

The determinants of health care use among rural, low-income mothers and their children were assessed using a multi-state, longitudinal data set, Rural Families Speak. The results indicate that rural mothers’ decisions regarding health care utilization for themselves and for their child can be best modeled using a simultaneous systems approach to negative binomial regression. Mothers’ visits to a health care provider increased with higher self-assessed depression scores, increased number of child’s doctor visits, greater numbers of total children in the household, greater numbers of chronic conditions, need for prenatal or post-partum care, development of a new medical condition, and having health insurance (Medicaid/equivalent and HMO/private). Child’s visits to a health care provider, on the other hand, increased with greater numbers of chronic conditions, development of a new medical condition, and increased mothers’ visits to a doctor. Child’s utilization of pediatric health care services decreased with higher levels of maternal depression, greater numbers of total children in the household, if the mother had HMO/private health care coverage, if the mother was pregnant, and if the mother was Latina/African American. Mother’s use of health care services decreased with her age, increased number of child’s chronic conditions, income as a percent of the federal poverty line, and if child had HMO/private health care insurance. The study expands the econometric techniques available for assessing maternal and pediatric health care use and the results contribute to an understanding of how rural, low-income mothers choose the level of health care services use for themselves and for their child. Additionally, the results would assist in formulating policies to reorient the type of health care services provided to this vulnerable population.