Refactorings are structured changes to existing software that leave its externally observable behaviour unchanged. The intent is to improve readability, performance or other non-behavioural properties of a program. Agile software engineering processes stress the importance of refactoring to keep program code extensible and maintainable. Despite their apparent benefits, manual refactorings are time-consuming and prone to introducing unintended side effects. Research efforts seek to support and automate refactoring tasks to overcome these limitations. Current research in automatic refactoring, as well as state-of-the-art automated refactoring tools, frequently rely on syntax-driven approaches. They focus on transformations which can be safely performed using only syntactic information about a program or act overly conservative when knowledge about program semantics is required. In this thesis we explore semantics-driven refactoring, which enables much more sophisticated refactoring schemata. Our semantics-driven refactorings rely on formal verification algorithms to reason over a program's behaviour, and we conjecture they are more precise and can handle more complex code scenarios than syntax-driven ones. For this purpose, we present and implement a program synthesis algorithm based on the CEGIS paradigm and demonstrate that it can be applied to a diverse set of applications. Our synthesiser relies on the bounded model checker CBMC as an oracle and is based on an earlier research prototype called Kalashnikov. We further define our Java Stream Theory (JST) which allows us to reason over a set of interesting semantic refactorings. Both solutions are combined into an automated semantic refactoring decision procedure, reasoning over program behaviours, and searching the space of possible refactorings using program synthesis. We provide experimental evidence to support our conjecture that semanticsdriven refactorings exceed syntax-driven approaches in precision and scope.

Model-based design based on the Simulink modeling formalism and the associated toolchain has gained its popularity in the development of complex embedded control systems. However,the current research on software synthesis for Simulink models has a critical gap for providing a deterministic, semantics-preserving implementation on multicore architectures with partitioned fixed-priority scheduling. In this thesis, we propose to judiciously assign task offset, task priority, and task communication mechanism, to avoid simultaneous access to shared memory by tasks on different cores, to preserve the model semantics, and to optimize the control performance. We develop two approaches to solve the problem: (a) a mixed integer linear programming (MILP) formulation; and (b) a problem specific exact algorithm that may run several magnitudes faster than MILP. / Master of Science / To save development time and money, automotive industries have been developing models using software, before implementing them directly on hardware. For reliability, the model generated from the software tool should behave in a well defined manner, coherent to the ideal design of the model. While the current tools are able to generate this reliable model for a single processor system, they are not able to do so for a system with multiple processors. When two or more processors contend to access the same resource at the same time, the existing tools are unable to provide a well defined execution order in their model. Since modern embedded systems need multiple processors to meet their increasing performance demands, it is imperative that the software tools scale up to multiple processors as well. In this work, we seek to bridge this gap by presenting two solutions that generate a deterministic software implementation of a system with multiple processors. In our solutions, we generate a model with well defined execution order by ensuring that at any given time, only one processor accesses a given resource. Furthermore, apart from ensuring determinism, we also improve upon the performance of the generated model by ensuring that there is minimal end-to-end latency in the system.

Technological advances are providing us with the capability to integrate more and more functionality into a single chip. This is leading to a new design paradigm, System On a Chip (SOC). In SOC designs all the functionality of a system is put inside a single chip, leading to increased performance, reduced power consumption, lower costs, and reduced size. SOC design brings with it new challenges and difficulties, however. The designs are now large, complicated and involve both software and hardware components. The designs have to be modeled at a high level of abstraction before partitioning into hardware and software components for final implementation. SystemC is a system level modeling language useful for System On a Chip design. It provides various features to perform system level modeling and simulation, which are missing in the generic HDL's such as VHDL and Verilog. The hardware portion of the SystemC models can be synthesized into hardware using commercial tools . The software portion can be rewritten as embedded software for the target processor. The aim of this thesis is to explore the SOC design process and to define methods for software synthesis of SystemC models. Software synthesis involves translation of SystemC models into code that is suitable for execution on an embedded processor. A simple scheduler that replaces the SystemC simulation kernel is proposed. This scheduler allows SystemC models to be executed directly as embedded software without the need for extensive modification or translation. Application of this process to the development of a GSM speech processing system, including the translation of part of the SystemC model into software that will execute on an embedded processor, is shown and the results are presented. / Master of Science

Made available in DSpace on 2014-06-11T19:22:35Z (GMT). No. of bitstreams: 0 Previous issue date: 2006-05-19Bitstream added on 2014-06-13T20:29:09Z : No. of bitstreams: 1 dezani_h_me_ilha.pdf: 383103 bytes, checksum: 4d2db649fe811e74784845f2d0b245b4 (MD5) / Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / Neste trabalho descreve-se um programa de geração automática de código para o microcontrolador 8051 da Intel, a partir de uma rede de Petri, com o objetivo de minimizar o tempo gasto na codificação do programa e automatizar completamente este processo de transformação. Definiu-se o uso da rede de Petri Lugar/Transição como modelo de entrada pois, mesmo tendo um modelo mais compacto, a rede de Petri Colorida, quando transformada em código Assembly é consideravelmente maior que o código Assembly gerado para a rede de Petri Lugar/Transição. Conclui-se que o código gerado pelo programa corresponde, exatamente, ao modelo da rede e pode ser executado pela arquitetura-alvo sem a necessidade de alterações no código. / This dissertation describes a program for the automatic generation of microcontroller code. The program takes a Petri net as input and outputs the corresponding assembly code for the Intel's 8051. The goal of this work is to speed up the coding process as well as to completely automate such a transformation. We use place/transition nets because even colored Petri nets resulting in quite compact models the assembly codes produced from them are much larger than those produced from place/transition nets. Also the code generated by the program described here exactly matches the net model, and can be directly executed on the target architecture without the need for further tuning.

Orientador: Norian Marranghello / Banca: Rogéria Cristiane Gratão de Souza / Banca: Carlos Magnus Carlson Filho / Resumo: Neste trabalho descreve-se um programa de geração automática de código para o microcontrolador 8051 da Intel, a partir de uma rede de Petri, com o objetivo de minimizar o tempo gasto na codificação do programa e automatizar completamente este processo de transformação. Definiu-se o uso da rede de Petri Lugar/Transição como modelo de entrada pois, mesmo tendo um modelo mais compacto, a rede de Petri Colorida, quando transformada em código Assembly é consideravelmente maior que o código Assembly gerado para a rede de Petri Lugar/Transição. Conclui-se que o código gerado pelo programa corresponde, exatamente, ao modelo da rede e pode ser executado pela arquitetura-alvo sem a necessidade de alterações no código. / Abstract: This dissertation describes a program for the automatic generation of microcontroller code. The program takes a Petri net as input and outputs the corresponding assembly code for the Intel's 8051. The goal of this work is to speed up the coding process as well as to completely automate such a transformation. We use place/transition nets because even colored Petri nets resulting in quite compact models the assembly codes produced from them are much larger than those produced from place/transition nets. Also the code generated by the program described here exactly matches the net model, and can be directly executed on the target architecture without the need for further tuning. / Mestre

Resource management is a critical part in high-performance computing software. While management of processing resources to increase performance is the most critical, efficient management of memory resources plays an important role in solving large problems. This thesis research seeks to create an effective dynamic memory management scheme for a declarative data-parallel programming system. In such systems, some sort of automatic resource management is a requirement. Using the Loci framework, this thesis research focuses on exploring such opportunities. We believe there exists an automatic memory management scheme for such declarative data-parallel systems that provides good compromise between memory utilization and performance. In addition to basic memory management, this thesis research also seeks to develop methods that take advantages of the cache memory subsystem and explore balances between memory utilization and parallel communication costs in such declarative data-parallel frameworks.

Made available in DSpace on 2014-06-12T15:49:47Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / A grande expansão do mercado de dispositivos digitais tem forçado empresas desenvolvedoras de sistemas embarcados em lidar com diversos desafios para prover sistemas complexos nesse nicho de mercado. Um dos desafios prominentes está relacionado ao consumo de energia, principalmente, devido aos seguintes fatores: (i) mobilidade; (ii) problemas ambientais; e (iii) o custo da energia. Como consequência, consideráveis esforços de pesquisa têm sido dedicados para a criação de técnicas voltadas para aumentar a economia de energia. Na última década, diversas técnicas foram desenvolvidas para reduzir o consumo de energia em sistemas embarcados. Muitos métodos lidam com gerenciamento dinâmico de energia (DPM), como, por exemplo, dynamic voltage scaling (DVS), cooperativamente com sistemas operacionais especializados, a fim de controlar o consumo de energia durante a execução do sistema. Entretanto, apesar da disponibilidade de muitos métodos de redução de consumo de energia, diversas questões estão em aberto, principalmente, no contexto de sistemas de tempo real crítico. Este trabalho propõe um método de síntese de software, o qual leva em consideração relação entre tarefas, overheads, restrições temporais e de energia. O método é composto por diversas atividades, as quais incluem: (i) medição; (ii) especificação; (iii) modelagem formal; (vi) escalonamento; e (v) geração de código. O método também é centrado no formalismo redes de Petri, o qual define uma base para geração precisa de escalas em tempo de projeto, adotando DVS para reduzir o consumo de energia. A partir de uma escala viável, um código customizado é gerado satisfazendo as restrições especificadas, e, dessa forma, garantindo previsibilidade em tempo de execução. Para lidar com a natureza estática das escalas geradas em tempo de projeto, um escalonador simples em tempo de execução é também proposto para melhorar o consumo de energia durante a execução do sistema. Diversos experimentos foram conduzidos, os quais demonstram a viabilidade da abordagem proposta para satisfazer restrições críticas de tempo e energia. Adicionalmente, um conjunto integrado de ferramentas foram desenvolvidas para automatizar algumas atividades do método de síntese de software proposto

Today, a plethora of parallel execution platforms are available. One platform in particular is the GPGPU – a massively parallel architecture designed for exploiting data parallelism. However, GPGPUS are notoriously difficult to program due to the way data is accessed and processed, and many interconnected factors affect the performance. This makes it an exceptionally challengingtask to write correct and high-performing applications for GPGPUS. This thesis project aims to address this problem by investigating how ForSyDe models – a software engineering methodology where applications are modeled at a very high level of abstraction – can be synthesized into CUDA C code for execution on NVIDIA CUDA-enabled graphics cards. The report proposes a software synthesis process which discovers one type of potential data parallelism in a model and generates either pure C or CUDA C code. A prototype of the software synthesis component has also been implemented and tested on models derived from two applications – a Mandelbrot generator and an industrial-scale image processor. The synthesized CUDA code produced in the tests was shown to be both correct and efficient, provided there was enough computation complexity in the processes to amortize the overhead cost of using the GPGPU.

Formally-based design and implementation techniques for complex safety-critical embedded systems are required not only to handle the complexity, but also to provide correctness guarantees. Traditional design approaches struggle to cope with complexity, and they generally require extensive testing to guarantee correctness. As the designs get larger and more complex, traditional approaches face many limitations. An alternate design approach is to adopt a "correct-by-construction" paradigm and synthesize the desired hardware and software from the high-level descriptions expressed using one of the many formal modeling languages. Since these languages are equipped with formal semantics, formally-based tools can be employed for various analysis. In this dissertation, we adopt one such formal modeling language - MRICDF (Multi-Rate Instantaneous Channel-connected Data Flow). MRICDF is a graphical, declarative, polychronous modeling language, with a formalism that allows the modeler to easily describe multi-clocked systems without the necessity of global clock. Unnecessary synchronizations among concurrent computation entities can be avoided using a polychronous language such as MRICDF. We have explored a Boolean theory-based techniques for synthesizing multi-threaded/concurrent code and extended the technique to improve the performance of synthesized multi-threaded code. We also explored synthesizing ASIPs (Application Specific Instruction Set Processors) from MRICDF models. Further, we have developed formal techniques to identify constructive causality in polychronous models. We have also developed SMT (Satisfiablity Modulo Theory)-based techniques to identify dimensional inconsistencies and to perform value-range analysis of polychronous models. / Ph. D.

Due to the ever increasing complexity of safety-critical applications, handwritten code is being replaced by automatically generated code derived from a high level specification. Code generation from high level specification requires a model of computation with an underlying formalism and correctness-preserving refinement steps to generate the lower level application code. Such software synthesis techniques are said to be 'correct-by-construction'. Synchronous programming languages such as Esterel, LUSTRE, which are based on a synchronous model of computation are used for sequential code generation. They work on a synchrony assumption (zero time intraprocess computation and zero time inter process communication) at the specification level. Early versions of synchronous languages followed an execution pattern where an iteration of software was mapped to an interval between ticks of an external reference clock. Since this external reference tick was unrelated to variables (or signals) within the software, redundant operations such as reading of ports, computation of guards were performed for each tick. In this dissertation, we highlight some of these performance issues and missed optimization opportunities. Also we show how a multi-clock (or polychronous) formalism, where each variable has an independent rate of execution associated with it, can avoid these problems. An existing polychronous language named SIGNAL, creates a hierarchy of clocks based on the rate of execution of individual variables, to form a root clock which acts a reference tick. We seek to replace the clock analysis with a technique to form a unique order of events without a reference time line. For this purpose, we present a new polychronous formalism termed Multi-rate Instantaneous Channel connected Data Flow (MRICDF). Our new synthesis technique inspects the specification to identify a master trigger at a Boolean equation level to act as the reference tick. Furthermore, we attempt to make polychronous specification based software synthesis more accessible to practicing engineers, by constructing a software tool EmCodeSyn, with a visual environment for specification and a more intuitive analysis technique. Our Boolean approach to sequential synthesis of embedded software has multiple implementations, each of which utilizes existing academic software tools. Optimizations are proposed to minimize synthesis time by simplifying the input to these external tools. Weaknesses in causal loop analysis techniques applied by existing synthesis tools are highlighted and solutions for performing time efficient loop analysis are integrated into EmCodeSyn. We have also determined that a part of the non-synthesizable polychronous specifications can be used to generate correct multi-threaded code. Additionally, we investigate composition of polychronous modules and propose properties that are necessary to guarantee agreement on shared signals. / Ph. D.