Simultaneous multithreading (SMT) processors can issue multiple instructions from distinct processes or threads in the same cycle. This technique effectively increases the overall throughput by keeping the pipeline resources more occupied at the potential expense of reducing single thread performance due to resource sharing. In the software domain, an increasing number of Dynamically Linked Libraries (DLL) are used by applications and operating systems, providing better flexibility and modularity, and enabling code sharing. It is observed that a significant amount of execution time in software today is spent in executing standard DLL instructions, that are shared among multiple threads or processes. However, for an SMT processor with a virtually-indexed based cache implementation, existing instruction fetching mechanisms can induce unnecessary false cache misses caused by the DLL-based instructions, which were intended to be shared. This problem is more conspicuous when multiple independent threads are executing concurrently in an SMT processor. This work investigates an often-neglected form of contention between running threads in the I-TLB and I-cache caused by DLLs. To address these shortcomings, we propose a system level technique involving a light-weight modification in the microarchitecture and the OS. By exploiting the nature of the DLLs in our new architecture, we are able to reinstate physical sharing of the DLLs in an SMT machine. Using Microsoft Windows based applications, our simulation results show that the optimized instruction fetching mechanism can reduce the number of DLL misses up to 5.5 times and improve the instruction cache hit rates by up to 62%, resulting in upto 30% DLL IPC improvements and upto 15% overall IPC improvements.

In this thesis, we propose new automation capabilities for the Coq proof assistant. We obtain this mechanization via an integration into Coq of decision procedures for propositional logic, equality reasoning and linear arithmetic which make up the core of the Alt-Ergo SMT solver. This integration is achieved through the reflection technique, which consists in implementing and formally proving these algorithms in Coq in order to execute them directly in the proof assistant. Because the algorithms formalized in Coq are exactly those in use in Alt-Ergo's kernel, this work significantly increases our trust in the solver. In particular, it embeds an original algorithm for combining equality modulo theory reasoning, called CC(X) and inspired by the Shostak combination algorithm, and whose justification is quite complex. Our Coq implementation is available in the form of tactics which allow one to automatically solve formulae combining propositional logic, equality and arithmetic. In order to make these tactics as efficient as may be, we have taken special care with performance in our implementation, in particular through the use of classical efficient data structures, which we provide as a separate library.

Les solveurs SMT sont des outils dédiés à la vérification d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les tableaux de bits ou les tableaux. Ajouter une nouvelle théorie à un solveur SMT nécessite en général une connaissance assez profonde du fonctionnement interne du solveur, et, de ce fait, ne peut en général être exécutée que par ses développeurs. Pour de nombreuses théories, il est également possible de fournir une axiomatisation finie en logique du premier ordre. Toutefois, si les solveurs SMT sont généralement complets et efficaces sur des problèmes sans quantificateurs, ils deviennent imprévisibles en logique du premier ordre. Par conséquent, cette approche ne peut pas être utilisée pour fournir une procédure de décision pour ces théories. Dans cette thèse, nous proposons un cadre d'application permettant de résoudre ce problème en utilisant des déclencheurs. Les déclencheurs sont des annotations permettant de spécifier la forme des termes avec lesquels un quantificateur doit être instancié pour obtenir des instances utiles pour la preuve. Ces annotations sont utilisées par la majorité des solveurs SMT supportant les quantificateurs et font partie du format SMT-LIB v2. Dans notre cadre d'application, l'utilisateur fournit une axiomatisation en logique du premier ordre de sa théorie, ainsi qu'une démonstration de sa correction, de sa complétude et de sa terminaison, et obtient en retour un solveur correct, complet et qui termine pour sa théorie. Dans cette thèse, nous décrivons comment un solveur SMT peut être étendu à notre cadre nous basant sur l'algorithme DPLL modulo théories, utilisé traditionnellement pour modéliser ls solveurs SMT. Nous prouvons également que notre extension a bien les propriétés attendues. L'effort à fournir pour implémenter cette extension dans un solveur SMT existant ne doit être effectué qu'une fois et le mécanisme peut ensuite être utilisé sur de multiples théories axiomatisées. De plus, nous pensons que, en général, cette implémentation n'est pas plus compliquée que l'ajout d'une unique théorie au solveur. Nous avons fait ce travail pour le solveur SMT Alt-Ergo, nous en présentons certains détails dans la thèse. Pour valider l'utilisabilité de notre cadre d'application, nous avons prouvé la complétude et la terminaison de plusieurs axiomatizations, dont une pour les listes impératives doublement chaînée, une pour les ensembles applicatifs et une pour les vecteurs de Ada. Nous avons ensuite utilisé notre implémentation dans Alt-Ergo pour discuter de l'efficacité de notre système dans différents cas.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:31Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:47Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:48:08Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Made available in DSpace on 2017-02-07T17:48:08Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) Previous issue date: 2016-09-13 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The software development for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification mechanisms, in order to create robust systems and reduce product recall rates. In addition, further development-time reduction and system robustness can be achieved through cross-platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present work proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), name as the efficient SMT-based bounded model checker (ESBMC++), for verifying actual Qt-based applications, and presents a success rate of 89%, for the developed benchmark suite. We also evaluate our simplified version of the Qt framework using other state-of-the-art verifiers for C++ programs and an evaluation about their level of compliance. It is worth mentioning that the proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code. / O desenvolvimento de software para sistemas embarcados tem crescido rapidamente, o que na maioria das vezes acarreta em um aumento da complexidade associada a esse tipo de projeto. Como consequência, as empresas de eletrônica de consumo costumam investir recursos em mecanismos de verificação rápida e automática, com o intuito de desenvolver sistemas robustos e assim reduzir as taxas de recall de produtos. Além disso, a redução no tempo de desenvolvimento e na robustez dos sistemas desenvolvidos podem ser alcançados através de frameworks multi-plataformas, tais como Qt, que oferece um conjunto de bibliotecas (gráficas) confiáveis para vários dispositivos embarcados. Desta forma, este trabalho propõe uma versão simplificada do framework Qt que integrado a um verificador baseado nas teorias do módulo da satisfatibilidade, denominado Efficient SMT-Based Bounded Model Checker (ESBMC++), verifica aplicações reais que ultilizam o Qt, apresentando uma taxa de sucesso de 89%, para os benchmarks desenvolvidos. Com a versão simplificada do framework Qt proposto, também foi feita uma avaliação ultilizando outros verificadores que se encontram no estado da arte para verificação de programas em C++ e uma avalição a cerca de seu nível de conformidade. Dessa maneira, a metodologia proposta se afirma como a primeira a verificar formalmente aplicações baseadas no framework Qt, além de possuir um potencial para desenvolver novas frentes para a verificação de código portátil.

The factors determining the quality of surface mount technology (SMT) solder joints are numerous, and complex. The exploration of these factors, and how they may affect the reliability and quality of the joints can only be achieved through continuous research. In this project, essential areas of SMT joints were selected for study and analysis, with the intention of providing additional design and process guidelines for the production of quality SMT joints. In the infrared reflow process, one of the common defect phenomena is the occurrence of tombstoning; that is after soldering only one end of the component is soldered while the other is lifted up, assuming a position like a tombstone. The initiation of tombstoning during reflow was analysed based on the forces acting on the component. A model was developed to predict the initiation of this phenomenon. The model shows that, under vibration-free conditions, the surface tension of the molten solder is the source of the force causing the initiation of tombstoning. The contact angle, which varies with the length of the printed circuit board solder land, has a significant effect on the value of the surface tension acting as a force pulling upward on the component. The model further shows that tombstoning initiation is due to the combined effects of the surface tension; the weight of the component; the dimensions of the component; the length of the solder underneath the component; and the length of the solder protruding from the end of the component. Selected components were used as examples for predicting the conditions of initiation, and these conditions were further substantiated by a series of experiments. Another area of study was a method which directly pulled the components off printed circuit boards and this was used as a means for testing the bond quality of surface mount technology leadless chip solder joints. Components D7243, CC1206, RC1206, RC121O, and CC1 812 were selected for this study. It was found that the ultimate tensile force which breaks a component off the printed circuit board has the potential to be used as a parameter for measuring the quality of the solder joint. The effect of solder thickness on the strength of a joint has also been investigated. The shape of joints soldered by two methods, wave soldering and infrared reflow, were compared. Joints at the two ends of a component produced by infrared reflow were found more uniform than the ones produced by wave soldering. A recommendation is made here for the wave soldering approach in achieving uniform solder joints. The effects of solder shape on the joint strength were further investigated by finite element analysis. A convex joint was found marginally more robust than a concave joint. Two aspects of the internal structure of SMT solder joints were investigated, void content and copper/tin intermetallic compounds. The voiding conditions of wave-soldered and infrared reflow joints were compared. No voids were found in all specimens that were produced by wave soldering. However, there were always voids inside joints produced by infrared reflow. Microhardness tests indicated that the hardness of compounds at the copper/solder interface of infrared reflowed joints is lower than that in the wave-soldered joints. It is considered that the lower hardness of the interfacial region of the infrared reflowed joints is due to the presence of voids. Scanning electron microscopy was used to study the formation of copper/tin intermetallic compounds for joints produced by infrared reflow. The results show that Cu 6 Sn5 was the only compound with a detectable thickness. Other compounds such as Cu3 Sn, were virtually not found at all. Aging of the joints at 100°C, shows that both the Cu 6Sn5 and the overall interfacial thickness grew with time. One of the important areas which had been overlooked previously and was studied in some details was the effects of solder paste exposure on the quality of solder paste. The characteristic changes of solder paste due to exposure were investigated in three areas, weight loss, tackiness, and rheology. The evaporation of low boiling point solvents was considered as the main contribution to the loss in the weight of the solder paste. The weight loss against exposure time was found to follow an exponential behaviour. A method was designed to evaluate the tackiness changes of solder paste due to exposure. It was found that the decay of tackiness against exposure time can be expressed by a power law. It is recommended that solder paste manufacturers should provide the necessary characteristic constants so as to enable the characteristics to be calculated after a specific exposure. The rheological changes of the solder paste as a result of exposure were also investigated. The implication on the printability of the solder paste due to these changes was studied and discussed.

Simultanous Multithreading (SMT) är ett koncept för att möjligöra effektivare utnyttjande av processorer genom att exekvera flera trådar samtidigt på en enda processorkärna, vilket leder till att systemet kan nyttjas till större grad. Om flera trådar använder samma funktonsenheter i procesorkärnan kommer effektiviteten att minska eftersom detta är ett scenario när SMT inte kan omvandla thread-level parallelism (TLP) till instruction-level parallelism (ILP). I tidigare arbete av de Blanche och Lundqvist föreslår de en simpel schemaläggningsprincip genom att anta att flera instanser av samma program använder samma resurser, bör dessa inte tillåtas att samköras. I detta arbete tillämpar vi deras princip på processorer med stöd för SMT, med motiveringen att flera identiska trådar använder samma funktionsenheter inom processorkärnan. Vi påvisar detta genom att förhindra program från att exekveras simultant med identiska program härleder till att SMT kan omvandla TLP till ILP oftare, när jobb inte kan utnyttja ILP självständigt. Intuitivt visar vi även att genom sakta ned ILP genom att göra det motsatta kan vi lindra belastningen på minnessystemet. / Simultaneous Multithreading (SMT) allows for more efficient processor utilization through co-executing multiple threads on a single processing core, increasing system efficiency and throughput. Multiple co-executing threads share the functional units of a processing core and if the threads use the same functional units, efficiency decreases as this is a scenario where SMT cannot convert thread-level parallelism (TLP) to instruction-level parallelism (ILP). In previous work by de Blanche and Lundqvist, they propose a simple co-scheduling principle co-scheduling multiple instances of the same job should be considered a bad co-schedule as they are more likely to use the same resources. In this thesis, we apply their principle on SMT processors with the rationale that identical threads should use the same functional units within a processing core. We demonstrate that by disallowing jobs to coexecute with itself we enable SMT to convert TLP to ILP more often and that this is true if jobs cannot exploit ILP by themselves. Intuitively, we also show that slowing down ILP by doing the opposite can alleviate the stress on the memory system.

Safety-critical systems, especially those found in avionics and automotive industries, rely on machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic exhibits subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. Failure of safety-critical systems is unacceptable, due to high-stakes involving human lives or huge amounts of money, time and effort. By formally proving properties of systems, we can be assured that they meet safety requirements. However, to prove such properties it is necessary to reason about machine arithmetic. SMT techniques for machine arithmetic are lacking scalability. This thesis presents approaches that augment or complement existing SMT techniques for machine arithmetic. In this thesis, we explore approximations as a means of augmenting existing decision procedures. A general approximation refinement framework is presented, along with its implementation called UppSAT. The framework solves a sequence of approximations. Initially very crude, these approximations are fairly easy to solve. Results of solving approximate constraints are used to either reconstruct a solution of original constraints, obtain a proof of unsatisfiability or to refine the approximation. The framework preserves soundness, completeness, and termination of the underlying decision procedure, guaranteeing that eventually, either a solution is found or a proof that solution does not exist. We evaluate the impact of approximations implemented in the UppSAT framework on the state-of-the-art in SMT for floating-point arithmetic. A novel method to reason about the theory of fixed-width bit-vectors called mcBV is presented. It is an instantiation of the model constructing satisfiability calculus, mcSAT, and uses a new lazy representation of bit-vectors that allows both bit- and word-level reasoning. It uses a greedy explanation generalization mechanism capable of more general learning compared to traditional approaches. Evaluation of mcBV shows that it can outperform bit-blasting on several classes of problems.

Advances in integrated circuit technology continue to provide more and more transistors on a chip. Computer architects are faced with the challenge of finding the best way to translate these resources into high performance. The challenge in the design of next generation CPU (central processing unit) lies not on trying to use up the silicon area, but on finding smart ways to make use of the wealth of transistors now available. In addition, the next generation architecture should offer high throughout performance, scalability, modularity, and low energy consumption, instead of an architecture that is suitable for only one class of applications or users, or only emphasize faster clock rate. A program exhibits different types of parallelism: instruction level parallelism (ILP), thread level parallelism (TLP), or data level parallelism (DLP). Likewise, architectures can be designed to exploit one or more of these types of parallelism. It is generally not possible to design architectures that can take advantage of all three types of parallelism without using very complex hardware structures and complex compiler optimizations. We present the state-of-art architecture SDF (scheduled data flowed) which explores the TLP parallelism as much as that is supplied by that application. We implement a SDF single-chip multiprocessor constructed from simpler processors and execute the automatically parallelizing application on the single-chip multiprocessor. SDF has many desirable features such as high throughput, scalability, and low power consumption, which meet the requirements of the next generation of CPU design. Compared with superscalar, VLIW (very long instruction word), and SMT (simultaneous multithreading), the experiment results show that for application with very little parallelism SDF is comparable to other architectures, for applications with large amounts of parallelism SDF outperforms other architectures.

This thesis focuses on design and implementation of a tool for automated generation of test inputs for a specified program trace. The aim of the thesis is to make development of testing suites (complying a given advanced coverage criteria) easier and more effective. These kinds of test suites are used in critical applications with code base written in low-level languages like C/C++ with strict restrictions applied. The tool investigates a program model and what conditions must be met to execute program in a way following provided trace. The tool uses advanced SMT-solver tool (software tool specialized for solving satisfiability problem) for generating fitting values. LLVM compiler framework libraries are used for modelling a program. Z3 library is used as a SMT-solver backend. This thesis brings results in architectural and implementation design of a tool capable of test inputs generation based on program analysis and provided program trace to cover.

Prioritization of software requirements is an important part of the requirements engineering process within the industry of software development. There are many different methods for achieving the most optimal order of software requirements, a list that shows in what order the requirements should be implemented. This degree project utilizes the SMT-based solver Z3 for an interactive prioritization algorithm. Previous studies have shown good results with another SMT-based solver called Yices. With the newer Z3 from Microsoft, the results have been improved further, and the tool is based on Python, and the framework for Z3 is called Z3PY. Experiments have been conducted on a set of different software requirements derived from a project in the healthcare industry and show that the Z3 solution is, in general, improving the requirements prioritization compared to other mentioned solutions in the study that has been tested on the same set of requirements. Results show that the Z3 solution outperformed the other SMT-based solution Yices by 2-4% regarding disagreement and by 3% regarding average distance. The results are significantly improved based on an ANOVA test with a p-value <= 0.05.