Modern software is built by teams of developers that work in a collaborative environment. The goal of this kind of development is that multiple developers can work in parallel. They can alter a set of shared artifacts and inspect and integrate the source code changes of other developers. For example, bug fixes, enhancements, new features or adaptations due to changing environment might be integrated into the system release. At a technical level, a collaborative development process is supported by version control systems. Since these version control systems allow developers to work in their own branch, merging and integration have become an integral part of the development process. These systems use automatic and advanced merging techniques to help developers to merge their modifications in the development repositories. However, these techniques do not guarantee to have a functional system. While the use of branching in the development process offers numerous advantages, the activity of merging and integrating changes is hampered by the lack of comprehensive support to assist developers in these activities. For example, the integration of changes can have an unexpected impact on the design or behavior of the system, leading to the introduction of subtle bugs. Furthermore, developers are not supported when integrating changes across branches (cherry picking), when dealing with branches that have diverged, when finding the dependencies between changes, or when assessing the potential impact of changes. In this dissertation we present an approach that aims at alleviating these problems by providing developers and, more precisely, integrators with semi-automated support for assisted integration within a branch and across branches. We focus on helping integrators with their information needs when understanding and integrating changes by means of characterizations of changes and streams of changes (i.e., sequence of successive changes within a branch) together with their dependencies. These characterizations rely on the first-class representation of systems' histories and changes based on program entities and their relationships rather than on files and text. For this, we provide a family of meta-models (Ring, RingH, RingS and RingC) that offer us the representation of program entities, systems' histories, changes and their dependencies, along with analyses for version comparison, and change and dependency identification. Instances of these meta-models are then used by our proposed tool support to enable integrators to analyze the characterizations and changes. Torch, a visual tool, and JET, a set of tools, actually provide the information needs to assist integration within a branch and across branches by means of the characterization of changes and streams of changes respectively.

Ce mémoire présente une implantation de la création paresseuse de tâches desti- née à des systèmes multiprocesseurs à mémoire distribuée. Elle offre un sous-ensemble des fonctionnalités du Message-Passing Interface et permet de paralléliser certains problèmes qui se partitionnent difficilement de manière statique grâce à un système de partitionnement dynamique et de balancement de charge. Pour ce faire, il se base sur le langage Multilisp, un dialecte de Scheme orienté vers le traitement parallèle, et implante sur ce dernier une interface semblable à MPI permettant le calcul distribué multipro- cessus. Ce système offre un langage beaucoup plus riche et expressif que le C et réduit considérablement le travail nécessaire au programmeur pour pouvoir développer des programmes équivalents à ceux en MPI. Enfin, le partitionnement dynamique permet de concevoir des programmes qui seraient très complexes à réaliser sur MPI. Des tests ont été effectués sur un système local à 16 processeurs et une grappe à 16 processeurs et il offre de bonnes accélérations en comparaison à des programmes séquentiels équiva- lents ainsi que des performances acceptables par rapport à MPI. Ce mémoire démontre que l’usage des futures comme technique de partitionnement dynamique est faisable sur des multiprocesseurs à mémoire distribuée. / This master’s thesis presents an implementation of lazy task creation for distributed memory multiprocessors. It offers a subset of Message-Passing Interface’s functionality and allows parallelization of some problems that are hard to statically partition thanks to its dynamic partitionning and load balancing system. It is based on Multilisp, a Scheme dialect for parallel computing, and implements an MPI like interface on top of it. It offers a richer and more expressive language than C and simplify the work needed to developp programs similar to those in MPI. Finally, dynamic partitioning allows some programs that would be very hard to develop in MPI. Tests were made on a 16 cpus computer and on a 16 cpus cluster. The system gets good accelerations when compared to equivalent sequential programs and acceptable performances when compared to MPI. It shows that it is possible to use futures as a dynamic partitioning method on distributed memory multiprocessors.

Face à l'augmentation de la taille et de la complexité des systèmes logiciels, il convient de les décrire à un plus haut niveau d'abstraction (\ie au-delà du code) avant de concrètement les implémenter. Toutefois, l'utilisation de ces descriptions de haut niveau dans les processus de construction et de vérification des systèmes reste très rudimentaire, ne permettant pas de véritablement guider et faciliter le développement logiciel. Cette thèse propose une nouvelle approche pour rendre plus simple et plus sûr le développement de systèmes logiciels. Cette approche repose sur l'utilisation de langages dédiés et sur un couplage fort entre une couche de spécification et d'architecture et une couche d'implémentation. Elle consiste tout d'abord à décrire à un haut niveau d'abstraction différents aspects, à la fois fonctionnels et non fonctionnels, d'un système dans la couche de spécification et d'architecture. Ces descriptions sont ensuite analysées et utilisées pour personnaliser la couche d'implémentation, afin de faciliter la construction et la vérification du système logiciel. Nous illustrons notre approche dans le domaine de l'informatique ubiquitaire. À la suite d'une analyse complète du domaine, nous avons conçu deux langages dédiés à l'orchestration d'objets communicants, Pantaxou et Pantagruel.

C++ est un des langages de programmation les plus utilisés en pratique, y compris pour le logiciel embarqué critique. C'est pourquoi la vérication de programmes écrits en C++ devient intéressante, en particulier via l'utilisation de méthodes formelles. Pour cela, il est nécessaire de se fonder sur une sémantique formelle de C++. De plus, une telle sémantique formelle peut être validée en la prenant comme base pour la spécication et la preuve d'un compilateur C++ réaliste, afin d'établir la confiance dans les techniques usuelles des compilateurs C++. Dans cette thèse, nous nous focalisons sur le modèle objet de C++. Nous proposons une sémantique formelle de l'héritage multiple en C++ comprenant les structures imbriquées à la C, sur laquelle s'appuie notre étude de la représentation concrète des objets avec optimisations des bases vides, à travers des conditions suffisantes que nous prouvons correctes vis-à-vis des accès aux champs et des opérations polymorphes. Puis nous spécifions un algorithme de représentation en mémoire fondé sur l'ABI pour Itanium, et une extension de cet algorithme avec optimisations des champs vides, et nous prouvons qu'ils satisfont nos conditions. Nous obtenons alors un compilateur vérifié et réaliste d'un sous-ensemble de C++ vers un langage à trois adresses et accès mémoire de bas niveau. Rajoutant à notre sémantique la construction et la destruction d'objets, nous étudions leurs interactions avec l'héritage multiple. Cela nous permet de formaliser la gestion de ressources, notamment le principe RAII (resource acquisition is initialization) via l'ordre de construction et destruction des sous-objets. Nous étudions aussi les effets sur les opérations polymorphes telles que la sélection de fonction virtuelle pendant la construction et la destruction, en généralisant la notion de type dynamique. Nous obtenons alors un compilateur vérifié pour notre sémantique étendue, notamment en prouvant la correction de l'implémentation des changements de types dynamiques. Toutes nos spécifications et preuves sont formalisées en Coq.

Cette thèse propose une nouvelle approche du parallélisme et de la concurrence, posant les bases d'un langage de programmation à la fois sûr et "secure" (garantissant la sécurité des données), fondé sur une sémantique formelle claire et simple, tout en étant adapté aux architectures multi-cores. Nous avons adopté le paradigme synchrone, dans sa variante réactive, qui fournit une alternative simple à la programmation concurrente standard en limitant l'impact des erreurs dépendant du temps ("data-races"). Dans un premier temps, nous avons considéré un langage réactif d'orchestration, DSL, dans lequel on fait abstraction de la mémoire (Partie 1). Dans le but de pouvoir traiter la mémoire et la sécurité, nous avons ensuite étudié (Partie 2) un noyau réactif, CRL, qui utilise un opérateur de parallélisme déterministe. Nous avons prouvé la réactivité bornée des programmes de CRL. Nous avons ensuite équipé CRL de mécanismes pour contrôler le flux d'information (Partie 3). Pour cela, nous avons d'abord étendu CRL avec des niveaux de sécurité pour les variables et les évènement, puis nous avons défini dans le langage étendu, SSL, un système de types permettant d'éviter les fuites d'information. Parallèlement (Partie 4), nous avons ajouté la mémoire à CRL, en proposant le modèle DSLM. En utilisant une notion d'agent, nous avons structuré la mémoire de telle sorte qu'il ne puisse y avoir de "data-races". Nous avons également étudié l'implémentation de DSLM sur les architectures multi-cores, fondée sur la notion de site et de migration d'un agent entre les sites. L'unification de SSL et de DSLM est une piste pour un travail futur.

En C, une stratégie classique pour implémenter les codes de gestion d'erreur est de faire suivre chaque opération qui peut générer une erreur d'une structure conditionnelle qui teste si l'opération a renvoyé une erreur. Ce stratégie basique, cependant, est sujette à erreurs, et il est courant d'oublier des opérations de nettoyage requises, ainsi que d'oublier de mettre à jour des codes de gestion d'erreur existants lorsque la fonction est étendue avec de nouvelles opérations. De plus, une partie importante du code doit souvent être dupliquée. Un style de programmation, <EM> stratégie goto </EM>, qui peut réduire en partie certaines de ces difficultés. Pour améliorer la structure des codes de gestion d'erreur dans les logiciels système, nous définissions un algorithme qui permet de transformer les codes de gestion d'erreur implémentés suivant la stratégie basique en codes de gestion d'erreur qui utilisent la <EM> stratégie goto</EM>. Même lorsque les codes de gestion d'erreurs sont structurés, la gestion et la libération des ressources allouées restent un problème lorsqu'il s'agit d'assurer la robustesse du code système. Dans cette thèse, nous proposons un algorithme <EM> microscopique </EM> de détection d'omission de libération de ressource, basé sur une analyse principalement intra-procédurale, qui prend en compte les flux et les chemins du code et qui cible et exploite les propriétés des codes de gestion d'erreur. Notre algorithme est résistant aux faux positifs dans l'ensemble des acquisitions de ressources et des opérations de libération, ce qui produit un faible taux de faux positifs dans les rapports renvoyés par l'outil tout en passant à l'échelle.

Thesis (Ph. D.)--Harvard University, 1985. / Includes bibliographical references (p).

Made available in DSpace on 2014-12-17T14:08:34Z (GMT). No. of bitstreams: 1 FelipeCAC.pdf: 1359871 bytes, checksum: 241fcfb66da39be9d48445bc9f6d11de (MD5) Previous issue date: 2009-06-30 / This work proposes an environment for programming programmable logic controllers applied to oil wells with BCP type method of artificially lifting. The environment will have an editor based in the diagram of sequential functions for programming of PLCs. This language was chosen due to the fact of being high-level and accepted by the international standard IEC 61131-3. The use of these control programs in real PLC will be possible with the use of an intermediate level of language based on XML specification PLCopen T6 XML. For the testing and validation of the control programs, an area should be available for viewing variables obtained through communication with a real PLC. Thus, the main contribution of this work is to develop a computational environment that allows: modeling, testing and validating the controls represented in SFC and applied in oil wells with BCP type method of artificially lifting / Este trabalho prop?e um ambiente computacional para programa??o de controladores l?gicos program?veis aplicados aos po?os de petr?leo com m?todo de eleva??o artificial do tipo BCP. O ambiente ter? um editor para programa??o de PLCs baseado principalmente no diagrama de fun??es sequenciais (SFC). Esta linguagem foi escolhida por ser considerada de alto n?vel e por ser aceita pelo padr?o internacional IEC 61131-3. O uso destes programas de controle em PLCs reais ser? poss?vel com a utiliza??o de uma linguagem de n?vel intermedi?rio baseada na especifica??o TC6 XML pela organiza??o PLCopen. Para os testes e a valida??o dos programas de controle, dever? ser disponibilizada uma ?rea para visualiza??o das vari?veis obtidas atrav?s da comunica??o com um PLC real. Desta forma, a principal contribui??o deste trabalho ? desenvolver um ambiente computacional que permita: modelar, testar e validar os controles representados em SFC e aplicados nos po?os petrol?feros com m?todo de eleva??o artificial do tipo BCP

This thesis is about techniques for proving the functional correctness of Abstract Data Type (ADT) implementations. We provide a framework for proving the functional correctness of imperative language implementations of ADTs, using a theory of refinement. We develop a theory of refinement to reason about both declarative and imperative language implementations of ADTs. Our theory facilitates compositional reasoning about complex implementations that may use several layers of sub-ADTs. Based on our theory of refinement, we propose a methodology for proving the functional correctness of an existing imperative language implementation of an ADT. We propose a mechanizable translation from an abstract model in the Z language to an abstract implementation in VCC’s ghost language. Then we present a technique to carry out the refinement checks completely within the VCC tool. We apply our proposed methodology to prove the functional correctness of the scheduling-related functionality of FreeRTOS, a popular open-source real-time operating system. We focused on the scheduler-related functionality, found major deviations from the intended behavior, and did a machine-checked proof of the correctness of the fixed code. We also present an efficient way to phrase the refinement conditions in VCC, which considerably improves VCC’s performance. We evaluated this technique on a simplified version of FreeRTOS which we constructed for this verification exercise. Using our efficient approach, VCC always terminates and leads to a reduction of over 90% in the total time taken by a naive check, when evaluated on this case-study.

CAPES / Os paradigmas de programação tradicionais carecem de técnicas para concepção de softwares de forma produtiva e de qualidade para uso eficiente das tecnologias de execução paralela, fornecidas pelos hardwares dos sistemas computacionais modernos. O Paradigma Orientado a Notificações (PON) apresenta uma nova abordagem no tocante ao processamento lógico-causal, primeiramente para o desenvolvimento de software, a qual se baseia em pequenas entidades colaborativas e pontualmente notificantes. Essa abordagem é mais eficiente e desacoplada quando comparado com os paradigmas de programação tradicionais, como o Paradigma Declarativo (PD) e o Paradigma Imperativo (PI). Ela permite a exploração de processamento, inclusive do paralelo e/ou distribuído, de maneira mais simples e eficiente do que em PI/PD. O PON inicialmente teve sua origem como uma solução de software, destacando a recente linguagem e compilador LingPON. No entanto outras pesquisas também o exploraram como uma solução de hardware em lógica reconfigurável, o qual apresenta um modelo de execução mais próximo ao modelo do PON. De fato, no tocante ao processamento paralelo, a execução de aplicações PON nem sempre pode ser feita da forma mais eficiente pelas arquiteturas de computadores tradicionais,baseados em conjunto de núcleos com modelos de execução sequencial. Neste âmbito, foi proposta uma nova arquitetura de computador orientada a notificações chamada NOCA (Notification Oriented Computer Architecture), a qual fornece uma dinâmica de execução segundo o modelo do PON, sendo composta por múltiplas unidades de processamento, a fim de permitir explorar de maneira mais adequada o paralelismo. Os experimentos realizados sobre um protótipo desta arquitetura demonstraram que a NOCA apresenta ganhos em avaliações comparativas de desempenho, dadas determinadas condições. No entanto, alguns aspectos foram desvantajosos ao protótipo da NOCA, em particular a baixa escala de paralelização obtida em função de limitação de palco de experimentação. Neste sentido, esta dissertação de mestrado apresenta o desenvolvimento de um simulador para a arquitetura NOCA, o qual é denominado de NOCASim. A implementação da NOCA na forma de software tem como objetivo simular o funcionamento dela com a quantidade de processadores simulados na mesma proporção do que o número de elementos PON que compõem uma aplicação. Isto permitiria obter dados de desempenho para validação do seu modelo funcional. Como estratégia de desenvolvimento, primeiramente este trabalho adaptou a LingPON para gerar assembly da NOCA facilitando o desenvolvimento de aplicações. Subsequentmente e principalmente, fez-se uso dos artefatos de projeto próprios da NOCA sendo que seu funcionamento consiste em simular em software a atualização dos estados internos da NOCA de forma semelhante a cada mudança do ciclo de clock. Experimentos realizados por meio do NOCASim com diferentes configurações demostraram que a NOCA apresenta melhora de desempenho a medida que o número de unidades de processamento aumenta. Além disso, verificaram-se possibilidades de melhorias conceituais a NOCA, que tendem a fortalecê-la como uma alternativa de execução paralela. / Traditional programming paradigms lack techniques for the productive and quality software’s design that makes efficient use of the parallel execution capabilities provided by the modern computing systems hardware. The Notification Oriented Paradigm (NOP) presents a new approach to develop more efficient and decoupled software when compared to the traditional programming paradigms, such as the Imperative Paradigm and the Declarative Paradigm. The NOP allows the exploitation of parallelization and/or distribution in a simpler and more efficient way than more commonly used programming paradigms. Initially, the NOP was conceived as an alternative software paradigm, highlighting the recent NOP language and compiler. However, other research was focused on hardware development using reconfigurable logic, which enables an execution model closer to the NOP model. Indeed, in parallel processing, the NOP applications cannot always be executed efficiently by the traditional computer architectures hardware based on set of cores with sequential execution model. Aiming at more efficient execution of NOP applications, a new Notification Oriented Computer Architecture (NOCA) has been developed. NOCA is based on multiple processing units, where each unit corresponds to specific elements of the NOP model. This way, parallelism is adequately exploited. Experiments were performed on a prototype of this architecture. When compared with Imperative Paradigm, execution time was improved under certain conditions, in particular, the low scale of parallelization obtained as a function of stage limitation of experimentation. In this sense, this Master of Science dissertation presents the development of a simulator for the NOCA architecture, which is called NOCASim. The NOCA implementation over software approach aims to simulate NOCA behavior with amount of simulated processors in the same proportions as the amount of NOP elements of an application. This allows obtain data for validation of NOCA functional model. As a development strategy, firstly this work adapted a NOP language to generate NOCA assembly facilitating the development of applications for this architecture. In the sequence, the own NOCA's design artifacts were used for the NOCASim development. The NOCASim operation consists of simulating in software to update the NOCA internal states in a similar way to each change in the clock cycle. The experiments results using NOCASim with different configurations have demonstrated that the NOCA performance improve when the number of processing units increases. In addition, were observed new possibilities for conceptual improvements to NOCA, which tend to strengthen it as a parallel execution alternative.