Le travail décrit dans cette thèse s'inscrit dans le contexte du développement et de la validation des systèmes réactifs synchrones. Il vise à tirer parti de certaines formes de structuration des programmes durant le processus de développement et de validation. Nous étudions premièrement l'utilisation d'opérateurs réguliers de types "itérateurs" qui permettent d'exprimer assez facilement des programmes réguliers manipulant des tableaux. Nous montrons aussi comment, au moment de la validation, on peut tirer partie de ces structures régulières pour rendre la preuve d'une propriété plus<br />simple. Nous nous intéressons ensuite à la spécification dite "par contrat" où un couple (assume, guarantee) est associé à chaque composant pour spécifier les hypothèses sur l'environnement et les<br />propriétés satisfaites par le composant sous ces hypothèses. Nous montrons l'intérêt de tels contrats à la fois en terme de spécification et de vérification pour le cas particulier des systèmes synchrones.<br />Nous proposons une série d'algorithmes de transformations de programmes (aussi bien autour de l'utilisation des itérateurs que des contrats) utilisable comme pre-processeur d'objectifs de preuve pour les outils de validation. Nos propositions, notamment sur l'aspect langage des itérateurs, ont répondu à des besoins rencontrés dans les applications industrielles, particulièrement autour du langage Lustre, auquel nous appliquons nos résultat. Ces propositions seront bientôt incluses dans la version industrielle du langage.

Ce travail porte sur le problème de la validation des logiciels réactifs synchrones par rapport à des propriétés de sûreté. Les propriétés de sûreté permettent de spécifier les comportements sûrs d'un logiciel. D'une manière générale, notre approche aborde la validation par le test. Dans ce cadre, nous avons défini une technique qui permet de déterminer, à partir des propriétés de sûreté seulement, toutes les données de test favorisant l'observation d'une violation de ces propriétés. Cette technique permet d'anticiper une violation future. Différentes heuristiques ont été implantées pour sélectionner les données de test de façon efficace. Notre proposition a été intégrée à l'outil Lutess. Ce dernier est capable de générer automatiquement et dynamiquement des données de test en s'appuyant sur divers guides. La capacité de nos heuristiques à guider le test vers des situations où la propriété de sûreté peut être violée a été évaluée sur une étude de cas significative proposée par un consortium d'industriels du secteur des télécommunications.

Ce travail s'inscrit dans le cadre de la conception d'environnements de test fonctionnel de systèmes réactifs spécifiés formellement en Lustre. Lutess est un tel environnement. Il permet la génération automatique et dynamique de données de test. Cette génération est menée sous contraintes, de manière aléatoire, et éventuellement guidée par des propriétés. Nous avons étendu cet environnement par une méthode de test de type statistique, qui facilite la génération des données de test considérées comme significatives par l'utilisateur. Nous avons validé expérimentalement Lutess avant et après son extension, en montrant que les données générées étaient bien aléatoires et qu'elles respectaient les distributions statistiques attendues. De plus, nous avons utilisé Lutess et la méthode proposée de façon intensive pour la validation de spécifications de services téléphoniques sur deux études de cas conséquentes : une fournie par le CNET et une autre sous la forme d'un concours proposé en marge de la conférence "Feature Interaction Workshop'98". A cette occasion, Lutess a été déclaré "meilleur outil pour la détection d'interactions de services téléphoniques".

Ce travail porte sur la production de code séquentiel à partir du langage flot de données synchrone Lustre. La difficulté essentielle provient de l'aspect déclaratif du langage. En effet, il n'y a pas d'instruction de contrôle dans le langage Lustre ; toute la structure de contrôle du code objet doit donc être synthétisée par le compilateur. Cette synthèse consiste à construire un automate fini en simulant exhaustivement le comportement des variables booléennes du programme. Le code produit est particulièrement rapide ; en effet, la plupart des calculs booléens sont effectués une fois pour toute dès la compilation. En contrepartie, l'aspect exhaustif de cette démarche provoque parfois une véritable explosion de la taille du code. Ce problème peut être dû à la complexité intrinsèque du programme source ; il faut dans ce cas chercher un compromis entre rapidité et taille mémoire. Mais l'explosion peut être causée par la méthode de construction, qui produit très souvent des automates non minimaux ; nous avons donc étudié et développé un algorithme original qui construit à coup sûr des automates minimaux. Cet algorithme fait appel à de nombreuses manipulations symboliques de fonctions booléennes, que nous avons pu implémenter efficacement grâce à une représentation basée sur les graphes binaires de décision.

Orientador: Rubens Pereira dos Santos / Resumo: A proposta de tese em foco contempla análises comparativas das obras "Clarissa" (1933), de Erico Verissimo, e "O lustre" (1946), de Clarice Lispector. Escritos no início de suas carreiras literárias, os romances dialogam entre si não somente as semelhanças de enredo, personagem principal e temas, mas a presença sensível da vanguarda impressionista, materializada na tessitura literária de ambas as narrativas, seja no plano do conteúdo ou da forma romanesca. Gêneros híbridos da modernidade, nas fronteiras entre o Bildungsroman moderno e o romance lírico, neste presente estudo também se objetivou interpretá-los e confrontá-los por esta chave de leitura, mas, sobretudo, compreender como acontece, em cada um desses romances, a transcriação (conceito de Haroldo de Campos [2006, 2015]) de uma estética eminentemente plástica para as veredas da linguagem, e como o impressionismo na literatura acabou adquirindo e consolidando contornos próprios e independentes da pintura cultivada no final do século XIX e começo do XX. Norteando-se pelos pressupostos da crítica literária (resgate da recepção e fortuna crítica das obras), teoria literária, literatura comparada e estudos interartes, a hipótese levantada por esta tese repousa, portanto, em investigar e comprovar a ressonância desta estética moderna que, imbricada ao estilo único de cada autor, produziu dois romances brasileiros com fortes ecos impressionistas. Com este processo de ressignificação comparada destas obras, a pesquisa almeja ... (Resumo completo, clicar acesso eletrônico abaixo) / Abstract: The proposed thesis in focus contemplates comparative analyzes of the works "Clarissa" (1933), by Erico Verissimo, and "O lustre" (1946), by Clarice Lispector. Written at the beginning of their literary careers, the novels dialogue among themselves not only the similarities of plot, main character and themes, but the sensitive presence of the impressionist avant-garde materialized in the literary fabric of both narratives, whether in terms of content or form. romanesque. Hybrid genres of modernity, on the frontiers between the modern Bildungsroman and the lyric novel, this study also aimed to interpret and confront them by this key reading, but, above all, to understand how it happens in each of these novels. transcreation (concept by Haroldo de Campos [2006, 2015]) of an eminently plastic aesthetic for the paths of language, and how impressionism in literature eventually acquired and consolidated its own independent contours of painting cultivated in the late nineteenth and early twentieth. Guided by the assumptions of literary criticism (redemption of the reception and critical fortune of works), literary theory, comparative literature and interart studies, the hypothesis raised by this thesis rests on investigating and proving the resonance of this modern aesthetic that, imbricated In the unique style of each author, he produced two Brazilian novels with strong impressionist echoes. With this process of comparative resignification of these works, the research aims to rescu... (Complete abstract click electronic access below) / Doutor

Parallel I/O performance is crucial to sustain scientific applications on large-scale High-Performance Computing (HPC) systems. Large scale distributed storage systems, in particular the object-based storage systems, face severe challenges for managing the data efficiently. Inefficient data management leads to poor I/O and storage performance in HPC applications and scientific workflows. Some of the main challenges for efficient data management arise from poor resource allocation, load imbalance in object storage targets, and inflexible data sharing between applications in a workflow. In addition, parallel I/O makes it challenging to shoehorn new interfaces, such as taking advantage of multiple layers of storage and support for analysis in the data path. Solving these challenges to improve performance and efficiency of object-based storage systems is crucial, especially for upcoming era of exascale systems. This dissertation is focused on solving these major challenges in object-based storage systems by providing scalable data management strategies. In the first part of the dis-sertation (Chapter 3), we present a resource contention aware load balancing tool (iez) for large scale distributed object-based storage systems. In Chapter 4, we extend iez to support Progressive File Layout for object-based storage system: Lustre. In the second part (Chapter 5), we present a technique to facilitate data sharing in scientific workflows using object-based storage, with our proposed tool Workflow Data Communicator. In the last part of this dissertation, we present a solution for transparent data management in multi-layer storage hierarchy of present and next-generation HPC systems.This dissertation shows that by intelligently employing scalable data management techniques, scientific applications' and workflows' flexibility and performance in object-based storage systems can be enhanced manyfold. Our proposed data management strategies can guide next-generation HPC storage systems' software design to efficiently support data for scientific applications and workflows. / Doctor of Philosophy / Large scale object-based storage systems face severe challenges to manage the data efficiently for HPC applications and workflows. These storage systems often manage and share data inflexibly, without considering the load imbalance and resource contention in the underlying multi-layer storage hierarchy. This dissertation first studies how resource contention and inflexible data sharing mechanisms impact HPC applications' storage and I/O performance; and then presents a series of efficient techniques, tools and algorithms to provide efficient and scalable data management for current and next-generation HPC storage systems

Storage systems used for supercomputers and high performance computing (HPC) centers exhibit load imbalance and resource contention. This is mainly due to two factors: the bursty nature of the I/O of scientific applications; and the complex and distributed I/O path without centralized arbitration and control. For example, the extant Lustre parallel storage system, which forms the backend storage for many HPC centers, comprises numerous components, all connected in custom network topologies, and serve varying demands of large number of users and applications. Consequently, some storage servers can be more loaded than others, creating bottlenecks, and reducing overall application I/O performance. Existing solutions focus on per application load balancing, and thus are not effective due to the lack of a global view of the system. In this thesis, we adopt a data-driven quantitative approach to load balance the I/O servers at extreme scale. To this end, we design a global mapper on Lustre Metadata Server (MDS), which gathers runtime statistics collected from key storage components on the I/O path, and applies Markov chain modeling and a dynamic maximum flow algorithm to decide where data should be placed in a load-balanced fashion. Evaluation using a realistic system simulator shows that our approach yields better load balancing, which in turn can help yield higher end-to-end performance. / Master of Science / Critical jobs such as meteorological prediction are run at exa-scale supercomputing facilities like Oak Ridge Leadership Computing Facility (OLCF). It is necessary for these centers to provide an optimally running infrastructure to support these critical workloads. The amount of data that is being produced and processed is increasing rapidly necessitating the need for these High Performance Computing (HPC) centers to design systems to support the increasing volume of data. Lustre is a parallel filesystem that is deployed in HPC centers. Lustre being a hierarchical filesystem comprises of a distributed layer of Object Storage Servers (OSSs) that are responsible for I/O on the Object Storage Targets (OSTs). Lustre employs a traditional capacity-based Round-Robin approach for file placement on the OSTs. This results in the usage of only a small fraction of OSTs. Traditional Round-Robin approach also increases the load on the same set of OSSs which results in a decreased performance. Thus, it is imperative to have a better load balanced file placement algorithm that can evenly distribute the load across all OSSs and the OSTs in order to meet the future demands of data storage and processing. We approach the problem of load imbalance by splicing the whole system into two views: filesystem and applications. We first collect the current usage statistics of the filesystem by means of a distributed monitoring tool. We then predict the applications’ I/O request pattern by employing a Markov Chain Model. Finally, we make use of both these components to design a load balancing algorithm that eventually evens out the load on both the OSSs and OSTs. We evaluate our algorithm on a custom-built simulator that simulates the behavior of the actual filesystem.

Ce document retrace de manière synthétique mes travaux de recherche depuis septembre 1999, date à laquelle j'ai été recruté sur un poste de Maître de Conférences à l'université Joseph Fourier (Grenoble 1).<br />Ces travaux, menés au sein de l'équipe VASCO du laboratoire LIG, portent sur le test des logiciels et sont étroitement liés aux recherches effectuées de 1993 à 1997, période pendant laquelle j'ai été thésard, puis chercheur contractuel dans cette même équipe.<br />Le test logiciel est une discipline qui embrasse l'ensemble du cycle de développement.<br />En effet, dès l'analyse des besoins d'une application, apparaissent des exigences et des propriétés à tester dont la caractérisation et l'identification font partie des compétences des testeurs. Il en est de même pour la spécification du produit, la conception de son architecture technique ou la programmation. <br />Le test logiciel est également une discipline qui se veut étroitement liée et utile à la pratique professionnelle. La prise en compte des problématiques issues de cette dernière s'est faite, entre autres, au moyen de nombreuses collaborations industrielles qui ont ponctué mes travaux, en particulier dans le cadre de projets nationaux (RNRT, RNTL).

This thesis deals with an effective solution of the parallel I/O of the k-Wave tool, which is designed for time domain acoustic and ultrasound simulations. k-Wave is a supercomputer application, it runs on a Lustre file system and it requires to be implemented with MPI and stores the data in suitable data format (HDF5). I designed three methods of optimization which fits k-Wave's needs. It uses accumulation and redistribution techniques. In comparison with the native write, every optimization method led to better write speed, up to 13.6GB/s. It is possible to use these methods to optimize every data distributed application with the write speed issue.

Made available in DSpace on 2016-04-28T19:59:09Z (GMT). No. of bitstreams: 1 Joelice Barbosa dos Santos.pdf: 1243787 bytes, checksum: 2f51770054d3784d1a87df09695ca182 (MD5) Previous issue date: 2008-04-22 / Secretaria da Educação do Estado de São Paulo / The central object of this research is the analysis of the novel O Lustre, by Clarice Lispector. Some theoretical reflections about the modern novel, as well as the criticism about this book, helped us in this study. Therefore, the present work does not base itself only in the theoretical discussion, but in the critical voice too, which did not recognize this literary work of 1946 as criticism did with the others novels by this author. The observations about the Aesthetics of Reception, proposed by Hans Robert Jauss, served to draw up the way in which the horizon of expectations about this novel developed. From this approach, we can observed that the question about the convention of the genres in the Lispector s work was a key factor that bothered many critics. Actually, this book does not follow the straight rules of the traditional novel. In this novel, the character stands out in the process of construction and the relations with the space. For this, it is transforming according to the place where it is. Gaston Bachelard s concepts were the base to analyze the space in this novel. The central attention about the question of space was based in the discussions that appear in his book The Poetics of the Space. The importance of the O Lustre in Lispector s work is also noted in the quotations from the other authors which appear in this narrative, as Edgar Allan Poe. Moreover, this book presents various relations with other arts. The present research wishes to contribute with the studies about Lispector s work. Especially with a novel considered minor in the Brazilian writer s production / O objetivo principal desta pesquisa é a análise do romance O lustre, de Clarice Lispector. Diversas reflexões teóricas acerca do romance moderno, assim como a fortuna crítica sobre este livro, nos auxiliaram neste estudo. Portanto, nosso trabalho não se pauta apenas na discussão teórica, mas na voz da crítica que, de certo modo, não valorizou o volume de 1946 do mesmo modo que julgou os demais romances da escritora. As considerações sobre a recepção crítica, propostas por Hans Robert Jauss, serviram para traçarmos uma linha evolutiva do horizonte de expectativas do leitor de O lustre. A partir dessa abordagem, verificamos que a questão sobre a convenção dos gêneros na obra de Lispector foi um fator que incomodou grande parte dos críticos, uma vez que esse livro não obedece a regras rígidas. Nesse romance, a personagem ganha destaque no processo de construção e nas relações com o espaço que se mostram necessárias à medida que ela se transforma e se constrói a partir do lugar em que se encontra. As idéias de Gaston Bachelard foram relevantes na análise do espaço, pois o recorte foi baseado nas discussões presentes em seu livro A poética do espaço. A importância de O lustre dentro da obra clariceana se mostra ainda no que diz respeito às referências a outros autores presentes nessa narrativa, como Edgar Allan Poe, bem como o diálogo com outras artes, conforme observamos. Em suma, esta pesquisa quer contribuir com os estudos que abordam a obra de Clarice Lispector a partir de um romance considerado menor na produção da escritora brasileira