Les comportements des processus concurrents peuvent être exprimés en utilisant des calculs de processus, des langages formels simples qui permettent de démontrer des résultats mathématiques précis sur les interactions entre processus. Un exemple très simple est CCS, un autre exemple est le pi-calcul, plus expressif grâce à un mécanisme de communication de canaux. Dans ce dernier, on peut instaurer un système de types (pour raffiner l'analyse aux environnements plus contraints) et encoder le lambda-calcul (qui représente les calculs séquentiels).Certains de ces calculs, comme CCS ou des variantes du pi-calcul comme les calculs de fusions, ont une certaine propriété de symétrie. On utilise dans un premier temps cette symétrie comme un outil, pour prouver que deux encodages du lambda-calcul dans le pi-calcul sont en fait équivalents.Cette preuve nécessitant un système de types et une forme de symétrie, on se pose la question de l'existence d'un système de types pour les autres calculs symétriques, notamment les calculs de fusion, à laquelle on répond par la négative avec un théorème d'impossibilité.En analysant ce théorème, on découvre un contrainte fondamentale de ces calculs qui empêche l'utilisation des types, à savoir la présence d'une notion de relation d'équivalence entre les canaux de communication. Le relâchement de cette contrainte pour obtenir une relation de pré-ordre engendre un calcul intéressant qui recouvre des notions importantes du pi-calcul, absentes dans les calculs de fusion : les types et les noms privés. La première partie de la thèse se concentre sur l'étude de ce calcul.La deuxième partie de la thèse se concentre sur la bisimulation, une méthode pour établir l'équivalence de deux agents dans des langages d'ordre supérieur, par exemple le pi-calcul ou le lambda-calcul. Une amélioration de cette méthode est la théorie des techniques modulo, très puissante, mais qui malheureusement s'applique uniquement aux systèmes de premier ordre, comme les automates ou CCS.Cette thèse s'applique alors à décrire les langages d'ordre supérieur en tant que systèmes du premier ordre. On récupère ainsi la théorie générale des techniques modulo pour ces langages, en prouvant correctes la correspondance induite et les techniques spécifiques à chaque langage. On détaille les tenants et aboutissants de cette approche, pour fournir les outils nécessaires à son utilisation pour d'autres langages d'ordre supérieur. / The behaviours of concurrent processes can be expressed using process calculi, which are simple formal languages that let us establish precise mathematical results on the behaviours and interactions between processes. A very simple example is CCS, another one is the pi-calculus, which is more expressive thanks to a name-passing mechanism. The pi-calculus supports the addition of type systems (to refine the analysis to more subtle environments) and the encoding of the lambda-calculus (which represents sequential computations).Some of these calculi, like CCS or variants of the pi-calculus such as fusion calculi, enjoy a property of symmetry. First, we use this symmetry as a tool to prove that two encodings of the lambda-calculus in the pi-calculus are in fact equivalent.This proof using a type system and a form of symmetry, we wonder if other existing symmetric calculi can support the addition of type systems. We answer negatively to this question with an impossibility theorem.Investigating this theorem leads us to a fundamental constraint of these calculi that forbids types: they induce an equivalence relation on names. Relaxing this constraint to make it a preorder relation yields another calculus that recovers important notions of the pi-calculus, that fusion calculi do not satisfy: the notions of types and of privacy of names. The first part of this thesis focuses on the study of this calculus, a pi-calculus with preorders on names.The second part of this thesis focuses on bisimulation, a proof method for equivalence of agents in higher-order languages, like the pi- or the lambda-calculi. An enhancement of this method is the powerful theory of bisimulations up to, which unfortunately only applies for first-order systems, like automata or CCS.We then proceed to describe higher-order languages as first-order systems. This way, we inherit the general theory of up-to techniques for these languages, by proving correct the translations and up-to techniques that are specific to each language. We give details on the approach, to provide the necessary tools for future applications of this method to other higher-order languages.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-07-12T12:30:10Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) DISSERTAÇÃO (2015-08-17) - RAFAEL BRANDAO LOBO.pdf: 1015468 bytes, checksum: d543b6f16adc4ce4d3aa4d59c8d546ff (MD5) / Made available in DSpace on 2016-07-12T12:30:10Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) DISSERTAÇÃO (2015-08-17) - RAFAEL BRANDAO LOBO.pdf: 1015468 bytes, checksum: d543b6f16adc4ce4d3aa4d59c8d546ff (MD5) Previous issue date: 2015-07-17 / CAPEs / Deadlocks are a common type of concurrency bug. When a deadlock occurs, it is difficult to clearly determine whether there is an actual deadlock or if the application is slow or hanging due to a different reason. It is also difficult to establish the cause of the deadlock. In general, developers deal with deadlocks by using analysis tools, introducing application-specific deadlock detection mechanisms, or simply by using techniques to avoid the occurrence of deadlocks by construction. In this paper we propose a different approach. We believe that if deadlocks manifest at runtime, as exceptions, programmers will be able to identify these deadlocks in an accurate and timely manner. We leverage two insights to make this practical: (i) most deadlocks occurring in real systems involve only two threads acquiring two locks (TTTL deadlocks); and (ii) it’s possible to detect TTTL deadlocks efficiently enough for most practical systems. We conducted a study on bug reports and found that more than 90% of identified deadlocks were indeed TTTL.We extended Java’s ReentrantLock class to detect TTTL deadlocks and measured the performance overhead of this approach with a conservative benchmark. For applications whose execution time is not dominated by locking, the overhead is estimated as below 6%. Empirical usability evaluation in two experiments showed that students finished tasks 16.87% to 30.7% faster on the average using our approach with the lock being the most significant factor behind it, and, in one of the experiments they were able to identify the defects more accurately with a signficant 81.25% increase in the number of correct answers when deadlock exceptions where present. / Deadlocks são um tipo comum de bug de concorrência. Quando um deadlock acontece, é difícil determinar claramente se houve um deadlock de verdade ou se a aplicação está lenta ou travada por qualquer outro motivo. Também é difícil estabelecer a causa do deadlock. Em geral, desenvolvedores lidam com deadlocks de várias maneiras: utilizando ferramentas analíticas; utilizando mecanismos especificos da aplicação para detectar deadlocks; ou simplesmente usando técnicas para evitar a ocorrência de deadlocks no momento da construção do código. Neste trabalho, propomos uma abordagem diferente. Acreditamos que se deadlocks se manifestarem durante a execução na forma de exceções, programadores serão capazes de identificar esses deadlocks de forma mais precisa e mais rápida. Levamos em consideração alguns aspectos para tornar esta abordagem prática: (i) a maioria dos deadlocks que ocorrem em sistemas reais envolvem apenas duas threads adquirindo dois locks ou two-thread, two-lock (TTTL) deadlock; e (ii) é possível detectar TTTL deadlocks de forma suficientemente eficiente para uso prático na maioria dos sistemas. Conduzimos um estudo com bugs reportados em sistemas de software de larga escala e descobrimos que mais de 90% dos bugs identificados como deadlocks eram de fato TTTL. Extendemos a classe ReentrantLock de Java para detectar TTTL deadlocks e medimos seu overhead na performance com um benchmark bastante conservador onde medimos o overhead das operações de trava quando deadlocks não são possíveis. Para aplicações cujo tempo de execução não é dominado por travas, o impacto médio no tempo de execução é na ordem de 6%. Realizamos uma avaliação empírica para testar usabilidade através de dois experimentos. Nesta avaliação, mostramos que, em média, estudantes terminam tarefas de 16.87% a 30.7% mais rapidamente usando nossa abordagem, sendo o tipo de abordagem o fator de maior significância e, em um dos experimentos, estudantes foram capazes de identificar mais corretamente a causa dos bugs, mostrando que o número de respostas corretas aumentou significativamente em 81.25% quando as exceções propostas estavam presentes.

The advent of multicore processors has put the performance of traditional parallel programming techniques in question. The traditional lock-based parallel programming techniques are error prone and suffer from various problems such as deadlocks, live-locks, priority inversion etc. In the last one and half decade, a considerable amount of the research has been carried out to achieve the synchronization among the parallel applications without using locking. One of most promising technique which has come out as a result of this research work is Transactional Memory (TM). Transactional Memory system commits the data in atomic code sequences called the transaction. Research has shown that Transactional Memory has the potential to out perform traditional locking mechanisms. In order to understand the design and implementation trade-offs of different implementations of the Software Transactional Memory, a comprehensive comparative study is required. Although some comparative studies have been carried out in the past, they were very focused in their scope and covered only few STM implementations. In this master thesis, a qualitative literature survey is conducted and the state of the art in Software Transactional Memory is presented, covering prominent approaches to date while discussing their design and implementation trade offs. / Cell. Number: 0046762600489 Address: c/o Muhammad Naveed Ahmed, G-Infartsvagen 3B, Appartment No. 683, 371 41 Karlkrona, Sweden

The aim of this work is to investigate whether threaded Android-applications written in C or C++ are more time-efficient than threaded Android-applications written in Java. The first part of the work was to perform a literature analysis in order to find out which types of algorithms were used in previous studies comparing the performance between non-threaded Android-applications written in Java and C/C++. Another literature analysis was performed where the outcome was to find suitable threaded versions of algorithms that could be used to compare the difference in time-consumption between algorithms implemented in Java and C/C++. Results have shown that for simple arithmetic operations and sorting functions, it is still possible to gain performance in terms of time-efficiency by implementing applications in C/C++. However, there are clear indications that these gains are smaller than they are in the non-threaded case. In algorithms dealing with string operations, the Java-version was significantly more time-efficient than the C++-version

Doctor of Philosophy / Department of Computing and Information Science / John M. Hatcliff / With the advent of multi-core processors and rich language support for concurrency, the paradigm of concurrent programming has arrived; however, the cost of developing and maintaining concurrent programs is still high. Simultaneously, the increase in social ubiquity of computing is reducing the "time-to-market" factor while demanding stronger correctness requirements. These effects are amplified with ever-growing size of software systems. Consequently, there is (will be) a rise in the demand for scalable and accurate techniques to enable faster development and maintenance of correct large scale concurrent software. This dissertation presents a collection of scalable and accurate approaches to tackle the above situation. Primarily, the approaches are focused on discovering dependences (relations) between various parts of the software/program and leveraging the dependences to improve maintenance and development tasks via program slicing (comprehension) and verification. Briefly, the proposed approaches are embodied in the following specific contributions: 1. New trace-based foundation for control dependences. 2. An equivalence class based analysis to efficiently and accurately calculate escape information and intra- and inter-thread dependences. 3. A new parametric data flow style slicing algorithm with various extensions to uniformly and easily realize and reason about most existing forms of static sequential and concurrent slicing. 4. A new generic notion of property/trace sensitivity to represent and reason about richer forms of context sensitivity. 5. Program dependence based partial order reduction techniques to enable efficient and accurate state space exploration in both static and dynamic mode. In an attempt to simplify the approaches, they have been based on the basic concepts/ideas of the affected techniques (e.g. program slicing is a rooted transitive closure of dependence relation). As trace-based reasoning is well suited for concurrent systems, an attempt has been made to explore trace-based reasoning wherever possible. While providing a rigorous theoretical presentation of these techniques, this effort also validates the techniques by implementing them in a robust tool framework called Indus (available from http://indus.projects.cis.ksu.edu) and then providing experimental results that demonstrate the effectiveness of the techniques on various concurrent applications. Given the current trend towards concurrent programming and social ubiquity of computing, the approaches proposed in this dissertation provide a foundation for collectively attacking scalability, accuracy, and soundness challenges in current and emerging systems.

This master thesis is a programmer's guide book of a concurrent programming on the Java 8 platform. Concurrency brings additional issues that cannot occur in single-threaded ap-plications. One of the thesis' objectives is to analyze these issues and introduce several principles that, in case they are properly followed, help to create flawless and well-behaving concurrent applications. Another goal of this thesis is to describe the Java con-currency programming from the theoretical point of view. Firstly, the thesis is focused on basic thread development and synchronization issues. Later, it introduces the features and instruments that are provided by Java 5 and higher versions. The theoretical passages are enriched by practical examples that perform discussed features and help to clarify some specific issues. The thesis is written in Czech language and covers large set of concurrency topics from the very basics through the utility libraries to modern instruments present in Java 8.

This thesis is an analysis of frameworks which support multithreading application devel-opment on platform Java. In particular this thesis analyses the overview of libraries which supports multithreading development in this language. Provided features are shown and described by the code examples. The thesis describes the principles of concurrent pro-gramming. Although multithreaded applications undoubtedly have many advantages, one of the goals of the thesis is to highlight the possible risks associated with their use. By the analysis of Java platform, I used method of description, analysis, synthesis and comparison. This thesis is composed of theoretical part, which defines the basic concepts and principles of concurrent applications. Theoretical parts also contain recherché of works, which deal with the topic of concurrent programming. In the analytical part are described and evaluated changes at various versions of Java language. Benefit of this work is clear documentation and evaluation of Java language concurrent utilities, from the oldest version of Java 1 to latest Java 8. So this work can help those, who need to learn how to develop concurrent applications in Java.

Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. Third, partial order models are automatically extracted from some instrumented concurrent program execution, and potential atomicity violation bugs are automatically verified based on the partial order models using model checking. Our formal specification and verification of Mondex have contributed to the world wide effort in developing a verified software repository. Our method to mine Petri net models automatically from provenance offers a new approach to build scientific workflows. Our dynamic prediction tool, named McPatom, can predict several known bugs in real world systems including one that evades several other existing tools. McPatom is efficient and scalable as it takes advantage of the nature of atomicity violations and considers only a pair of threads and accesses to a single shared variable at one time. However, predictive tools need to consider the tradeoffs between precision and coverage. Based on McPatom, this dissertation presents two methods for improving the coverage and precision of atomicity violation predictions: 1) a post-prediction analysis method to increase coverage while ensuring precision; 2) a follow-up replaying method to further increase coverage. Both methods are implemented in a completely automatic tool.

Muitos dos sistemas de computação existentes atualmente são concorrentes, ou seja, neles constam diversas entidades que, ao mesmo tempo, operam sobre um conjunto de recursos compartilhados. Nesse contexto, devemos controlar a concorrência das diversas operações realizadas, ou então a interferência entre elas poderia causar inconsistências nos recursos compartilhados ou nas próprias operações realizadas. Nesse texto, vamos tratar especificamente de estruturas de dados concorrentes, ou seja, estruturas de dados cujas operações associadas -- consideramos inserção, remoção e busca -- sejam passíveis de execução simultânea por diversas entidades. Tendo em vista o controle da concorrência, vamos adotar uma abordagem baseada no emprego de locks, uma primitiva de sincronização muito usual na literatura. Nossa discussão será apresentada em termos de certas estruturas de dados chamadas skip graphs, que têm propriedades interessantes para outros contextos, como o contexto de sistemas distribuídos. / Many existing computer systems are concurrent, or, in other words, they are composed of many entities that, at the same time, operate over some set of shared resources. In this context, we must control the concurrency of the operations, otherwise the interference between them could cause inconsistencies in the shared resources or in the operations themselves. In this text, we specifically discuss concurrent data structures, or, in other words, data structures over which the associated operations -- we consider insertion, removal and search -- could be executed simultaneously by various entities. In order to control the concurrency, we will employ an aproach based on the use of locks, a widely known synchronization primitive in the literature. Our discussion will be presented in terms of data structures called skip graphs, which have interesting properties in other contexts, as the context of distributed systems.

Los lenguajes concurrentes est an cada d a m as presentes en nuestra sociedad, tanto en las nuevas tecnolog as como en los sistemas utilizados de manera cotidiana. M as a un, dada la actual distribuci on de los sistemas y su arquitectura interna, cabe esperar que este hecho siga siendo una realidad en los pr oximos a~nos. En este contexto, el desarrollo de herramientas de apoyo al desarrollo de programas concurrentes se vuelve esencial. Adem as, el comportamiento de los sistemas concurrentes es especialmente dif cil de analizar, por lo que cualquier herramienta que ayude en esta tarea, a un cuando sea limitada, ser a de gran utilidad. Por ejemplo, podemos encontrar herramientas para la depuraci on, an alisis, comprobaci on, optimizaci on, o simpli caci on de programas. Muchas de ellas son ampliamente utilizadas por los programadores hoy en d a. El prop osito de esta tesis es introducir, a trav es de diferentes lenguajes de programaci on concurrentes, t ecnicas de an alisis que puedan ayudar a mejorar la experiencia del desarrollo y publicaci on de software para modelos concurrentes. En esta tesis se introducen tanto an alisis est aticos (aproximando todas las posibles ejecuciones) como din amicos (considerando una ejecuci on en concreto). Los trabajos aqu propuestos di eren lo su ciente entre s para constituir ideas totalmente independientes, pero manteniendo un nexo com un: el hecho de ser un an alisis para un lenguaje concurrente. Todos los an alisis presentados han sido de nidos formalmente y se ha probado su correcci on, asegurando que los resultados obtenidos tendr an el grado de abilidad necesario en sistemas que lo requieran, como por ejemplo, en sistemas cr ticos. Adem as, se incluye la descripci on de las herramientas software que implementan las diferentes ideas propuestas. Esto le da al trabajo una utilidad m as all a del marco te orico, permitiendo poner en pr actica y probar con ejemplos reales los diferentes an alisis. Todas las ideas aqu presentadas constituyen, por s mismas, propuestas aplicables en multitud de contextos y problemas actuales. Adem as, individualmente sirven de punto de partida para otros an alisis derivados, as como para la adaptaci on a otros lenguajes de la misma familia. Esto le da un valor a~nadido a este trabajo, como bien atestiguan algunos trabajos posteriores que ya se est an bene ciando de los resultados obtenidos en esta tesis. / Concurrent languages are increasingly present in our society, both in new technologies and in the systems used on a daily basis. Moreover, given the current systems distribution and their internal architecture, one can expect that this remains so in the coming years. In this context, the development of tools to support the implementation of concurrent programs becomes essential. Futhermore, the behavior of concurrent systems is particularly difficult to analyse, so that any tool that helps in this task, even if in a limited way, will be very useful. For example, one can find tools for debugging, analysis, testing, optimisation, or simplification of programs, which are widely used by programmers nowadays. The purpose of this thesis is to introduce, through various concurrent programming languages, some analysis techniques that can help to improve the experience of the software development and release for concurrent models. This thesis introduces both static (approximating all possible executions) and dynamic (considering a specific execution) analysis. The topics considered here differ enough from each other to be fully independent. Nevertheless, they have a common link: they can be used to analyse properties of a concurrent programming language. All the analyses presented here have been formally defined and their correctness have been proved, ensuring that the results will have the reliability degree which is needed for some systems (for instance, for critical systems). It also includes a description of the software tools that implement the different ideas proposed. This gives the work a usefulness well beyond the theoretical aspect, allowing us to put it in practice and to test the different analyses with real-world examples All the ideas here presented are, by themselves, approaches that can be applied in many current contexts and problems. Moreover, individually they serve as a starting point for other derived analysis, as well as for the adaptation to other languages of the same family. This gives an added value to this work, a fact confirmed by some later works that are already benefiting from the results obtained in this thesis. / Tamarit Muñoz, S. (2013). Analysis Techniques for Concurrent Programming Languages [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/31651 / TESIS