Network processors are new types of multithreaded multicore processors geared towards achieving both fast processing speed and flexibility of programming. The architecture of network processors considers many special properties for packet processing, including multiple threads, multiple processor cores on the same chip, special functional units, simplified ISA and simplified pipeline, etc. The architectural peculiarities of network processors raise new challenges for compiler design and optimization. Due to very high clocking speeds, the CPU memory gap on such processors is huge, making registers extremely precious. Moreover, the register file is split into two banks, and for any ALU instruction, the two source operands must come from different banks. We present and compare three different approaches to do register allocation and bank assignment. We also address the problem of sharing registers across threads in order to maximize the utilization of hardware resources. The context switches on the IXP network processor only happen when long latency operations are encountered. As a result, context switches are highly frequent. Therefore, the designer of the IXP network processor decided to make context switches extremely lightweight, i.e. only the program counter(PC) is stored together with the context. Since registers are not saved and restored during context switches, it becomes difficult to share registers across threads. For a conventional processor, each thread can assume that it can use the entire register file, because registers are always part of the context. However, with lightweight context switch, each thread must take a separate piece of the register file, making register usage inefficient. Programs executing on network processors typically have runtime constraints. Scheduling of multiple programs sharing a CPU must be orchestrated by the OS and the hardware using certain sharing policies. Real time applications demand a real time aware OS kernel to meet their specified deadlines. However, due to stringent performance requirements on network processors, neither OS nor hardware mechanisms is typically feasible. In this work, we demonstrate that a compiler approach could achieve some of the OS scheduling and real time scheduling functionalities without introducing a hefty overhead.

Recent years have witnessed the emergence of microprocessors that are embedded within a plethora of devices used in everyday life. Embedded architectures are customized through a meticulous and time consuming design process to satisfy stringent constraints with respect to performance, area, power, and cost. In embedded systems, the cost of the memory hierarchy limits its ability to play as central a role. This is due to stringent constraints that fundamentally limit the physical size and complexity of the memory system. Ultimately, application developers and system engineers are charged with the heavy burden of reducing the memory requirements of an application. This thesis offers the intriguing possibility that compilers can play a significant role in the automatic design space exploration and optimization of embedded memory systems. This insight is founded upon a new analytical model and novel compiler optimizations that are specifically designed to increase the synergy between the processor and the memory system. The analytical models serve to characterize intrinsic program properties, quantify the impact of compiler optimizations on the memory systems, and provide deep insight into the trade-offs that affect memory system design.

Thesis (M.S.E.C.E.)--Baylor University, 2008. / Includes bibliographical references (p. 77-79).

Thesis (Ph. D.)--University of Alabama at Birmingham, 2007. / Additional advisors: Jeff Gray, Marjan Mernik, Alan Sprague, Murat Tanik. Description based on contents viewed June 25, 2007; title from title screen. Includes bibliographical references (p. 132-138).

As software and hardware systems grow more complex and we begin to rely more on their correctness and reliability, it becomes exceedingly important to formally verify certain properties of these systems. If done naïvely, verifying a system can easily require exponentially more work than running it, in order to account for all possible executions. However, there are often symmetries or other properties of a system that can be exploited to reduce the amount of necessary work. In this thesis, we present a number of approaches that do this in the context of the CSP model checker FDR. CSP is named for Communicating Sequential Processes, or parallel combinations of state machines with synchronised communications. In the FDR model, the component processes are typically converted to explicit state machines while their parallel combination is evaluated lazily during model checking. Our contributions are motivated by this model but applicable to other models as well. We first address the scalability of the component machines by proposing a lazy compiler for a subset of CSP_M selected to model parameterised state machines. This is a typical case where the state space explosion can make model checking impractical, since the size of the state space is exponential in the number and size of the parameters. A lazy approach to evaluating these systems allows only the reachable subset of the state space to be explored. As an example, in studying security protocols, it is common to model an intruder parameterised by knowledge of each of a list of facts; even a relatively small 100 facts results in an intractable 2¹⁰⁰ states, but the rest of the system can ensure that only a small number of these states are reachable. Next, we address the scalability of the overall combination by presenting novel algorithms for bisimulation reduction with respect to strong bisimulation, divergence- respecting delay bisimulation, and divergence-respecting weak bisimulation. Since a parallel composition is related to the Cartesian product of its components, performing a relatively time-consuming bisimulation reduction on the components can reduce its size significantly; an efficient bisimulation algorithm is therefore very desirable. This thesis is motivated by practical implementations, and we discuss an implementation of each of the proposed algorithms in FDR. We thoroughly evaluate their performance and demonstrate their effectiveness.

Os compiladores têm por função traduzir um programa em uma linguagem fonte para uma linguagem alvo, geralmente uma linguagem de máquina. Nessa tradução, encontrar a melhor correspondência entre as linguagens é um problema complexo, pelo tamanho do espaço de busca. Por tal complexidade, uma etapa de transformação de código é necessária, na qual algoritmos de transformação modificam o código tentando melhorá-lo sem alterar seu significado. O Problema de Seleção de Transformações (PST) consiste na busca das melhores transformações para um código de entrada, tal que o código final obtenha um bom desempenho. O estado-da-arte não possui estratégias que possibilitem soluções para o PST aplicáveis a usuários finais, pois o tempo de resposta é alto para tal aplicação. O objetivo deste trabalho é formular técnicas para encontrar efetivas sequências de transformações a serem aplicadas a um código de entrada, de forma a aumentar seu desempenho reduzindo o tempo de execução. Além disso, objetiva-se reduzir o tempo de resposta de forma que a solução para o PST se aproxime da utilização por usuários finais. Inicialmente, se explora a Variable Neighborhood Search (VNS) para solucionar o PST, compilando iterativamente cada código de entrada. A aplicação da VNS alcançou resultados até 15,72% melhores do que outra estratégia iterativa, conseguindo melhoria em todos os programas avaliados em relação ao melhor nível de transformação. Contudo, a compilação iterativa possui alto tempo de resposta. Assim, é necessário explorar técnicas de aprendizagem de máquina, que podem prover bons resultados baseadas em experiências anteriores do compilador. Dessa forma, esta dissertação explora diferentes caracterizações de programas para representar o conhecimento acumulado na aplicação de transformações, para então aplicar a um sistema de geração de código com Raciocínio Baseado em Casos (RBC), que escolhe determinada sequência para um programa de entrada. A representação do conhecimento é capaz de atingir 81% de proximidade do melhor resultado possível para os programas avaliados, enquanto o sistema RBC gera resultados 13,74% melhores do que o nível -O3, em um tempo de resposta 99% inferior ao de estratégias de compilação iterativa. A melhoria nas formas de recuperação de experiências anteriores conseguiu superar em 20,23% o desempenho obtido por outra estratégia comparada com um número de avaliações próximo. / Compilers aims to translate a source language program to a target language, usually a machine language. Find the best correspondence between programming languages is a complex problem, due to the size of search space. Because of this complexity, a code transformation step is needed, where transformation algorithms modify the code, trying to improve it without semantic alterations. Despite, the result of the application of these algorithms depends on code particularities. The Transformations Selection Problem (TSP) consists of the search for the best transformations to an input code, such that target code achieves a good performance. The state-of-art does not have strategies that allow the application of TSP solutions to final users, because the response time is very high to this. This work aims to formulate techniques to find effective transformations sequences to be applied to an input code, in a way to increase programs performance reducing its execution time. Furthermore, another objective is to reduce the compiler response time, to approximate a TSP solution to final users application. Initially, the metaheuristic Variable Neighborhood Search (VNS) is explored to solve TSP, compiling iteratively each input code. VNS achieved results up to 15.72% better than another iterative strategy, reaching improvement for all evaluated programs compared to the best compiler transformation level. However, the iterative compilation demands a high response time. Therefore, it is necessary to explore machine learning techniques, which can provide good results based on compiler previous experiences, with a cost of an initial training phase. Thus, this work explores different program characterizations to represent the cumulated knowledge on transformations application, to formulate a code generation system with Case-Based Reasoning (CBR), which chooses certain sequence to an input program. The knowledge representation is capable to reach 81% of proximity of the best possible result to evaluated programs, while the CBR system generates results 13.74% better than -O3 level, on a response time 99% lower than iterative compilation techniques. The improvement of previous experiences recovering method obtained performances over 20.23% compared to another strategy with a close evaluations number.

Os compiladores têm por função traduzir um programa em uma linguagem fonte para uma linguagem alvo, geralmente uma linguagem de máquina. Nessa tradução, encontrar a melhor correspondência entre as linguagens é um problema complexo, pelo tamanho do espaço de busca. Por tal complexidade, uma etapa de transformação de código é necessária, na qual algoritmos de transformação modificam o código tentando melhorá-lo sem alterar seu significado. O Problema de Seleção de Transformações (PST) consiste na busca das melhores transformações para um código de entrada, tal que o código final obtenha um bom desempenho. O estado-da-arte não possui estratégias que possibilitem soluções para o PST aplicáveis a usuários finais, pois o tempo de resposta é alto para tal aplicação. O objetivo deste trabalho é formular técnicas para encontrar efetivas sequências de transformações a serem aplicadas a um código de entrada, de forma a aumentar seu desempenho reduzindo o tempo de execução. Além disso, objetiva-se reduzir o tempo de resposta de forma que a solução para o PST se aproxime da utilização por usuários finais. Inicialmente, se explora a Variable Neighborhood Search (VNS) para solucionar o PST, compilando iterativamente cada código de entrada. A aplicação da VNS alcançou resultados até 15,72% melhores do que outra estratégia iterativa, conseguindo melhoria em todos os programas avaliados em relação ao melhor nível de transformação. Contudo, a compilação iterativa possui alto tempo de resposta. Assim, é necessário explorar técnicas de aprendizagem de máquina, que podem prover bons resultados baseadas em experiências anteriores do compilador. Dessa forma, esta dissertação explora diferentes caracterizações de programas para representar o conhecimento acumulado na aplicação de transformações, para então aplicar a um sistema de geração de código com Raciocínio Baseado em Casos (RBC), que escolhe determinada sequência para um programa de entrada. A representação do conhecimento é capaz de atingir 81% de proximidade do melhor resultado possível para os programas avaliados, enquanto o sistema RBC gera resultados 13,74% melhores do que o nível -O3, em um tempo de resposta 99% inferior ao de estratégias de compilação iterativa. A melhoria nas formas de recuperação de experiências anteriores conseguiu superar em 20,23% o desempenho obtido por outra estratégia comparada com um número de avaliações próximo. / Compilers aims to translate a source language program to a target language, usually a machine language. Find the best correspondence between programming languages is a complex problem, due to the size of search space. Because of this complexity, a code transformation step is needed, where transformation algorithms modify the code, trying to improve it without semantic alterations. Despite, the result of the application of these algorithms depends on code particularities. The Transformations Selection Problem (TSP) consists of the search for the best transformations to an input code, such that target code achieves a good performance. The state-of-art does not have strategies that allow the application of TSP solutions to final users, because the response time is very high to this. This work aims to formulate techniques to find effective transformations sequences to be applied to an input code, in a way to increase programs performance reducing its execution time. Furthermore, another objective is to reduce the compiler response time, to approximate a TSP solution to final users application. Initially, the metaheuristic Variable Neighborhood Search (VNS) is explored to solve TSP, compiling iteratively each input code. VNS achieved results up to 15.72% better than another iterative strategy, reaching improvement for all evaluated programs compared to the best compiler transformation level. However, the iterative compilation demands a high response time. Therefore, it is necessary to explore machine learning techniques, which can provide good results based on compiler previous experiences, with a cost of an initial training phase. Thus, this work explores different program characterizations to represent the cumulated knowledge on transformations application, to formulate a code generation system with Case-Based Reasoning (CBR), which chooses certain sequence to an input program. The knowledge representation is capable to reach 81% of proximity of the best possible result to evaluated programs, while the CBR system generates results 13.74% better than -O3 level, on a response time 99% lower than iterative compilation techniques. The improvement of previous experiences recovering method obtained performances over 20.23% compared to another strategy with a close evaluations number.

<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>

Submitted by Milena Rubi (milenarubi@ufscar.br) on 2016-10-18T13:50:17Z No. of bitstreams: 1 FERREIRA_Maria_2015.pdf: 44702801 bytes, checksum: d58773cbbac5f088372d16f186805b06 (MD5) / Approved for entry into archive by Milena Rubi (milenarubi@ufscar.br) on 2016-10-18T13:50:31Z (GMT) No. of bitstreams: 1 FERREIRA_Maria_2015.pdf: 44702801 bytes, checksum: d58773cbbac5f088372d16f186805b06 (MD5) / Approved for entry into archive by Milena Rubi (milenarubi@ufscar.br) on 2016-10-18T13:50:43Z (GMT) No. of bitstreams: 1 FERREIRA_Maria_2015.pdf: 44702801 bytes, checksum: d58773cbbac5f088372d16f186805b06 (MD5) / Made available in DSpace on 2016-10-18T13:51:11Z (GMT). No. of bitstreams: 1 FERREIRA_Maria_2015.pdf: 44702801 bytes, checksum: d58773cbbac5f088372d16f186805b06 (MD5) Previous issue date: 2015-12-18 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / Compiler error messages should allow programmers to understand and solve quickly problems found during the compilation process. However, compilers usually issue short contextless messages with little information and with terms that are difficult to understand. This work introduces the plug-in Error Message System (EMS) that allows the presentation of easy-to-understand and more meaningful error messages. EMS is a plug-in to the Eclipse IDE. It is highly configurable through Domain Specific Languages (DSLs). The DSLs allow that regular users build their own error messages and share them. Beginner programmers can use a set of error messages adapted to them thus reducing the time of understanding and correction of compilation errors. / As mensagens de erro dos compiladores devem permitir que os programadores compreendam e solucionem os problemas encontrados durante o processo de compilação rapidamente. Entretanto, os compiladores usualmente emitem mensagens curtas, sem contexto, pouco informativas e com termos de difícil compreensão. Este trabalho apresenta o plug-in Error Message System (EMS) que permite a apresentação das mensagens de erro mais fáceis de entender e mais informativas. EMS é um plugin para a IDE Eclipe e é altamente configurável através de linguagens específicas de domínio(LED). As LEDs permitem que usuários comuns façam suas próprias mensagens de erro e as compartilhem. Programadores iniciantes podem utilizar um conjunto de mensagens adaptadas a eles, reduzindo o tempo de compreensão e correção dos erros de compilação.

Atuais paradigmas correntes de programação de software, mais precisamente o Paradigma Imperativo (PI) e o Paradigma Declarativo (PD), apresentam deficiências que afetam o desempenho das aplicações e a obtenção de “desacoplamento” (ou acoplamento mínimo) entre elementos de software. Com o objetivo de amenizar essas deficiências, foi desenvolvido o Paradigma Orientado a Notificações (PON). O PON se inspira nos conceitos do PI (e.g. objetos) e do PD (e.g. base de fatos e regras), mas altera a essência da execução ou inferência lógica-causal. Basicamente, o PON usa objetos para tratar de fatos e regras na forma de composições de outros objetos menores que, entretanto, apresentam características comportamentais de certa autonomia, independência, reatividade e colaboração por meio de notificações pontuais para fins de inferência. Isto dito, salienta-se que a materialização dos conceitos do PON se deu por meio de um arquétipo ou Framework elaborado em linguagem de programação C++. Tal materialização do PON vem sendo utilizada como uma alternativa para o desenvolvimento de aplicações sob o domínio desse paradigma e possibilitou, de fato, a criação de aplicações para ambientes computacionais usuais baseados na chamada arquitetura Von Neumann. Apesar destas contribuições para com a sua materialização, o desenvolvimento de aplicações no PON ainda não apresentava resultados satisfatórios em termos de desempenho tal qual deveria a luz do seu cálculo assintótico, nem a facilidade de programação que seria uma das suas características principais. Nesse âmbito, o presente trabalho propõe como evolução para o estado da técnica do PON a criação de uma linguagem e compilador para o paradigma. Sendo assim, este trabalho apresenta a definição da linguagem criada com a utilização de exemplos práticos guiados pelo desenvolvimento de aplicações. Subsequentemente são apresentados detalhes do compilador bem como sua estrutura. Para demonstrar a evolução do estado da técnica do paradigma, no tocante a desempenho (e.g. tempo de processamento) e facilidade de programação foram realizados estudos comparativos com a utilização da linguagem e compilador. Os estudos comparativos foram guiados com a elaboração de dois softwares denominados aplicação Mira ao Alvo e aplicação de Vendas. Essas aplicações foram desenvolvidas com base na linguagem PON e foram realizados experimentos simulando sequências de execução com o intuito de avaliar o tempo de processamento para o resultado gerado pelo compilador PON. Ainda, tais experimentos possibilitaram a avaliação de maneira subjetiva da linguagem de programação PON no tocante a facilidade de programação. Deste modo, foi possível observar com tais estudos comparativos que os resultados apresentados pelo compilador PON foram satisfatórios quando comparados aos resultados obtidos pelo Framework e por aplicações equivalentes desenvolvidas baseadas no Paradigma Orientado a Objetos (POO). / The current software development paradigms, specifically the Imperative Paradigm (IP) and the Declarative Paradigm (DP), have weaknesses that affect the applications performance and decoupling (or minimal coupling) between the software modules. In order to provide a solution regarding these weaknesses, the Notification Oriented Paradigm (NOP) was developed. NOP is inspired by the concepts of the IP (e.g. objects) and DP (e.g. base of facts and Rules). Basically, NOP uses objects to deal with facts and Rules as compositions of other, smaller, objects. These objects have the following behavioral characteristics: autonomy, independence, responsiveness and collaboration through notifications. Thus, it’s highlighted that the realization of these concepts was firstly instantiated through a Framework developed in C++. Such NOP materialization has been used as an alternative for Application development in the domain of this paradigm and made possible, in fact, the creation of applications for typical computing environments based on Von Neumann architecture. The development of the C++ materialization of NOP has not presented satisfactory results in terms of performance as it should when taking into account its asymptotic calculation and programming facility. In this context, this work presents an evolution of NOP by creating a specific programming language, and its respective compiler, for this paradigm. Therefore, this work presents the language definition and the details of the development of its compiler. To evaluate the evolution regarding to performance (e.g. processing time) and programming facility, some comparative studies using the NOP language and compiler are presented. These comparative studies were performed by developing two software applications called Target and Sales Application. These applications have been developed based on NOP language, and the experiments were performed simulating sequences of execution in order to evaluate the processing time for the generated results by NOP compiler. Still, these experiments allowed the evaluation of NOP programming language, in a subjective way, regarding to ease programming. Thus, with such comparative studies, it was possible to observe that the results presented by the compiler NOP were satisfactory when compared to the results achieved via Framework and for equivalent applications developed based on the Oriented Object Paradigm (OOP).