Vérifier formellement des programmes concurrents est une tâche difficile. S’il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de programmes séquentiels sont utilisées avec succès depuis plusieurs années déjà, et permettent d’atteindre de hauts degrés de confiance dans nos systèmes. Cette thèse propose une alternative aux méthodes d’analyses dédiées à la vérification de programmes concurrents consistant à transformer le programme concurrent en un programme séquentiel pour le rendre analysable par des outils dédiés aux programmes séquentiels. Nous nous plaçons dans le contexte de FRAMA-C, une plate-forme d’analyse de code C spécifié avec le langage ACSL. Les différentes analyses de FRAMA-C sont des greffons à la plate-forme, ceux-ci sont à ce jour majoritairement dédiés aux programmes séquentiels. La méthode de vérification que nous proposons est appliquée manuellement à la vérification d’un code concurrent issu d’un hyperviseur. Nous automatisons la méthode à travers un nouveau greffon à FRAMA-C qui permet de produire automatiquement, depuis un programme concurrent spécifié, un programme séquentiel spécifié équivalent. Nous présentons les bases de sa formalisation, ayant pour but d’en prouver la validité. Cette validité n’est valable que pour la classe des programmes séquentiellement consistant. Nous proposons donc finalement un prototype de solveur de contraintes pour les modèles mémoire faibles, capable de déterminer si un programme appartient bien à cette classe en fonction du modèle mémoire cible. / Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware.

Studien avsåg att olika aspekter för att skapa underlag för utvecklingen med att förbättra fleranvändning. Syftet var, utöver de olika aspekterna, att på konceptuell nivå utvärdera hur fleranvändning kan utföras tekniskt samt undersöka hur användarna påverkas av denna förändring. Detta har utförts genom flertalet workshops och intervjuer. Vid två tillfällen har också författarna till rapporten utbildats i hur systemet är uppbyggt och hur det används. Utifrån detta har värdekriterier värderats mot olika tekniker. De teknikerna är Mutex, Semaphores och Oracle Tuxedo. På det sättet har olika aspekter beaktats och konceptuella modeller har målats upp. De olika teknikerna lever alla upp till de tekniska kraven som ställts, som programmeringsspråket C# och en databas från Oracle. I samverkan mellan användare och utvecklare har nivån på lösningen tagits fram, vad den ger användarna för nytta samtidigt som det inte är för komplicerat. Dessutom har det ställts krav angående prestandan, att den inte får försämras väsentligt. Användarna får ett liknande arbetssätt med minskade krav på samordning. Det medför att de kan samarbeta med de datamängder de behöver. Den lösning som passade bäst utifrån dessa kriterier var Mutex. / This paper is intended to study different aspects and take them in consideration to create a foundation for the developers to improve a multi-user environment. The purpose was to evaluate how to develop multi-user systems at a conceptual level with the technical aspects and describe how the users were affected by this. The study is based on multiple workshops and interviews. The writers have also been educated on how the system is used by the users and how the system was built, at two separate occasions. Based on this, criterias were made and these were valued against different techniques. These techniques are Mutex, Semaphores and Oracle Tuxedo. The criterias were considered and conceptual models were made to visualize the solution. The different techniques all live up to the constraints from the hardware and software of the case study, like the programming language C# and a database from Oracle. In a cooperation between the developers and users have the level of the solution been defined, where the solution ease the problems enough and still not too complex to implement. There have also been a few directions on the performance of the system. The solution should not be affecting the performance significantly. The users’working methods are not going to be particularly affected. The main part of the cooperation are not as needed as before. They can work in the same dataset concurrent in the datasets they required. On this basis the best technique to use in this case was Mutex.

Verification and validation is one of the most important concerns in the area of software engineering towards more reliable software development. Hence it is important to overcome the challenges of testing concurrent programs. The extensive use of concurrent systems warrants more attention to the concurrent software testing. For testing concurrent software, automatic tools development is getting increased focus. The first part of this study presents a systematic review that aims to explore the state-of-the-art of concurrent software testing. The systematic review reports several issues like concurrent software characteristics, bugs, testing techniques and tools, test case generation techniques and tools, and benchmarks developed for the tools. The second part presents the evaluation of four commercial and open source static analysis tools detecting Java multithreaded bugs. An empirical evaluation of the tools would help the industry as well as the academia to learn more about the effectiveness of the static analysis tools for concurrency bugs.

Radio access technologies for cellular mobile networks are continuously being evolved to meet the future demands for higher data rates, and lower end‐to‐end delays. In the research and development of LTE, radio network simulations play an essential role. The evolution of parallel processing hardware makes it desirable to exploit the potential gains of parallelizing LTE radio network simulations using multithreading techniques in contrast to distributing experiments over processors as independent simulation job processes. There is a hypothesis that parallel speedup gain diminishes when running many parallel simulation jobs concurrently on the same machine due to the increased memory requirements. A proposed multithreaded prototype of the Ericsson LTE simulator has been constructed, encapsulating scheduling, execution and synchronization of asynchronous physical layer computations. In order to provide implementation transparency, an algorithm has been proposed to sort and synchronize log events enabling a sequential logging model on top of non‐deterministic execution. In order to evaluate and compare multithreading techniques to parallel simulation job distribution, a large number of experiments have been carried out for four very diverse simulation scenarios. The evaluation of the results from these experiments involved analysis of average measured execution times and comparison with ideal estimates derived from Amdahl’s law in order to analyze overhead. It has been shown that the proposed multithreaded task‐oriented framework provides a convenient way to execute LTE physical layer models asynchronously on multi‐core processors, still providing deterministic results that are equivalent to the results of a sequential simulator. However, it has been indicated that distributing parallel independent jobs over processors is currently more efficient than multithreading techniques, even though the achieved speedup is far from ideal. This conclusion is based on the observation that the overhead caused by increased memory requirements, memory access and system bus congestion is currently smaller than the thread management and synchronization overhead of the proposed multithreaded Java prototype.

La programmation concurrente à mémoire partagée est un modèle classique de concurrence qui permet notamment de tirer parti des processeurs multicoeurs aujourd'hui très répandus dans les ordinateurs personnels. Les programmes concurrents sont sujets au problème des interblocages, notoirement difficiles à prévoir et à éliminer, en particulier dans le cas de l'utilisation du mécanisme de synchronisation très populaire que sont les mutex. Dans cette thèse nous avons travaillé à rendre plus aisée la programmation avec des mutex en étudiant des méthodes d'évitement des interblocages. Nous avons d'abord étudié une méthode utilisant une analyse statique par un système de types et d'effets, puis une variante de cette méthode dans un langage à typage dynamique. La seconde méthode est celle que nous avons le plus développée. Elle combine prévention et évitement des interblocages pour fournir une fonction de verrouillage sans interblocages expressive et utilisable. Nous l'avons implémentée sous forme d'une bibliothèque Hop (dialecte de Scheme). Ce faisant, nous avons développé un algorithme sans famine pour l'acquisition simultanée d'un nombre arbitraire de mutex, et identifié le concept d'interblocage asymptotique. Nous avons également été amenés à proposer une optimisation des exceptions (blocs finally). Nos tests de performances semblent indiquer un impact négligeable de l'utilisation de notre bibliothèque sur des applications concurrentes réelles. La majeure partie de notre recherche pourrait être appliquée à d'autres langages de programmation structurée tels que Java. / Shared-memory concurrency is a classic concurrency model which, among other things, makes it possible to take advantage of multicore processors that are now widespread in personal computers. Concurrent programs are prone to deadlocks which are notoriously hard to predict and debug. Programs using mutexes, a very popular synchronization mechanism, are no exception. In this thesis we studied deadlock avoidance methods with the aim of making programming with mutexes easier. We first studied a method that uses a static analysis by means of a type and effect system, then a variation on this method in a dynamically typed language. We developed more the second method. It mixes deadlock prevention and avoidance to provide an easy-to-use and expressive deadlock-free locking function. We implemented it as a Hop (dialect of Scheme) library. This lead us to develop a starvation-free algorithm to simultaneously acquire an arbitrary number of mutexes, and to identify the concept of asymptotic deadlock. While doing so, we also developped an optimization of exceptions(finally blocks). Our performance tests seem to show that using our library has negligible impact on theperformance of real-life applications. Most of our work could be applied to other structured programming languages such as Java.

Submitted by Haroudo Xavier Filho (haroudo.xavierfo@ufpe.br) on 2016-04-08T18:59:56Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação_PatriciaTenório_BC.pdf: 884166 bytes, checksum: 0a78095c224981af6d91420fd610f878 (MD5) / Made available in DSpace on 2016-04-08T18:59:56Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação_PatriciaTenório_BC.pdf: 884166 bytes, checksum: 0a78095c224981af6d91420fd610f878 (MD5) Previous issue date: 2015-09-17 / Dissertação resultado da pesquisa de Mestrado em Letras, área de concentração Teoria da Literatura, linha de pesquisa Intersemiose, no Programa de Pós-Graduação em Letras da Universidade Federal de Pernambuco, tendo como objetivo relacionar o romance O retrato de Dorian Gray, de Oscar Wilde, com três pilares teóricos: o índice fotográfico de Charles Sanders Peirce, o tempo de Agostinho de Hipona e a prefiguração no conceito de figura de Erich Auerbach. A cada capítulo, outros teóricos são convidados a dialogar, tais como John R. Searle, Susan Sontag, Philippe Dubois, Roland Barthes, Albert Einstein, Henri Bergson, Georges Didi-Huberman e Gaston Bachelard. / Dissertation result of Master’s research in Literature, area of concentration Literary Theory, line of research Intersemiosis, in the Postgraduate Program in Literature from the Federal University of Pernambuco, having as objective order to relate the novel The Picture of Dorian Gray, by Oscar Wilde, with three theoretical pillars: the photographic index of Charles Sanders Peirce, the time of Augustine from Hippona and the foreshadowing in the concept of figure from Erich Auerbach. Each chapter, other theorists are invited to dialogue, such as John R. Searle, Susan Sontag, Philippe Dubois, Roland Barthes, Albert Einstein, Henri Bergson, Georges Didi-Huberman and Gaston Bachelard.

La thèse porte sur les réseaux de Kahn, un modèle de concurrence simple et expressif proposé par Gilles Kahn dans les années 70, et leur implémentation sur des architectures multi-coeurs modernes, à mémoire partagée. Dans un réseau de Kahn, le programmeur décrit un programme parallèle comme un ensemble de processus et de canaux communicants, reliant chacun exactement un processus producteur à un consommateur. Nous nous concentrons ici sur les aspects algorithmiques et les choix de conception liés à l'implémentation, avec deux points clefs : les garanties non bloquantes et la mémoire relâchée. Le développement d'algorithmes non bloquants efficaces s'inscrit dans une optique de gestion des ressources et de garantie de performance sur les plateformes à ordonnancement irrégulier, telles que les machines virtuelles ou les GPU. Un travail complémentaire sur les modèles de mémoire relâchée vient compléter cette approche théorique par un prolongement plus pratique dans le monde des architectures à mémoire partagée contemporaines. Nous présentons un nouvel algorithme non bloquant pour l'interprétation de réseaux de Kahn. Celui-ci est parallèle sur les accès disjoints : il permet à plusieurs processeursde travailler simultanément sur un même réseau de Kahn partagé, tout en exploitant le parallélisme entre processus indépendants. Il offre dans le même temps des garanties de progrès non bloquant : en mémoire bornée et en présence de retards sur les processeurs. L'ensemble forme, à notre connaissance, le premier système complètement non bloquant de cette envergure : techniques classiques de programmation non bloquante et contributions spécifiques aux réseaux de Kahn. Nous discutons également d'une variante bloquante destinée au calcul haute performance, avec des résultats expérimentaux encourageants. / In this thesis, we are interested in Kahn process networks, a simple yet expressive model of concurrency, and its parallel implementation on modern shared-memory architectures. Kahn process networks expose concurrency to the programmer through an arrangement of sequential processes and single-producer single-consumer channels. The focus is on the implementation aspects. Of particular importance to our study are two parameters: lock freedom and relaxed memory. The development of fast andefficient lock-free algorithms ties into concerns of controlled resource consumption and reliable performance on current and future platforms with unfair or skewed scheduling such as virtual machines and GPUs. Our work with relaxed memory models complements this more theoretical approach by offering a window into realistic sharedmemory architectures. We present a new lock-free algorithm for a Kahn process network interpreter. It is disjoint-access parallel: we allow multiple threads to work on the same shared Kahn process network, fully utilizing the parallelism exhibited by independent processes. It is nonblockingin that it guarantees global progress in bounded memory, even in the presence of (possibly infinite) delays affecting the executing threads. To our knowledge, it is the first lock-free system of this size, and integrates various well-known non-blocking techniques and concepts (e.g., safe memory reclamation, multi-word updates, assistance) with ideas and optimizations specific to the Kahn network setting. We also discuss a variant of the algorithm, which is blocking and targeted at high-performance computing, with encouraging experimental results.

No description available.

Contracts for concurrency describe required atomicity of method sequences in concurrent programs. This work proposes a dynamic analyzer to verify programs written in Java against contracts for concurrency. The analyzer was designed to detect violations of parametric contracts with spoilers. The proposed analyzer was implemented as an extension to the RoadRunner framework. Support for accessing the method arguments and return values was added to RoadRunner as a part of the solution. The analyzer was fully implemented and verified on a set of testing programs.

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau, comme les pointeurs et les interactions avec le matériel spécifique. De plus, le fait que ces systèmes soient concurrents conduit à une augmentation exponentielle du nombre de comportements possibles, ce qui rend plus difficile leur vérification. Dans cette thèse, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous avons proposé un modèle de mémoire et d'exécution d'un programme C séquentiel en TLA+. En se basant sur ce modèle, nous avons proposé un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous avons montré comment ce modèle peut s'étendre pour modéliser les programmes C concurrents et gérer la synchronisation entre plusieurs processus ainsi que leur ordonnancement. Pour réduire la complexité du model-checking, nous avons proposé une technique permettant de réduire significativement la complexité de la vérification. Cette réduction consiste pour un code C à agglomérer une suite d'instructions lors de la génération du code TLA+, sous réserve d'un ensemble de conditions.Nous avons appliqué la méthodologie proposée dans cette thèse sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel,sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.Les résultats ont permis d'étudier le comportement du système, de vérifier certaines propriétés et de trouver des bugs indétectables par des simples tests. / Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems. But, the application of formal methods to software systems, implemented in C, is challenging due to the presence of pointers, pointer arithmetic andinteraction with hardware. Moreover, software systems are often concurrent, making the verification process infeasible. This work provides a methodology to specify and verify C software systems usingmodel-checking technique. The proposed methodology is based on translating the semantics of Cinto TLA+, a formal specification language for reasoning about concurrent and reactive systems. We define a memory and execution model for a sequential program and a set of translation rules from C to TLA+ that we developed in a tool called C2TLA+. Based on this model, we show that it can be extended to support concurrency, synchronization primitives and process scheduling. Although model-checking is an efficient and automatic technique, it faces the state explosion problem when the system becomes large. To overcome this problem, we propose a state-space reduction technique. The latter is based on agglomerating a set of C instructions during the generation phase of the TLA+ specification. This methodology has been applied to a concrete case study, a microkernel of an industrial real-time operating system, on which a set of functional properties has been verified. The application of the agglomeration technique to the case study shows the usefulness of the proposed technique in reducing the complexity of verification. The obtained results allow us to study the behavior of the system and to find errors undetectable using traditional testing techniques.