Concurrency in programming is a way of interleaving tasks in order to enhance the performance of an application. Previous research has found that concurrency errors are hard to avoid, hard to find, and that they often degrade performance of the application. Reactive programming provides an abstraction, to make it easier to implement complex concurrent and asynchronous tasks. When programming reactively in Java, it is often done with a reactive framework, where RxJava and Project-Reactor are two of the more popular choices. Blocking a thread that is not supposed to be blocked will result in concurrency errors, without the Java compiler providing a warning. In order to find incorrect blocking, a tool called BlockHound can be used. BlockHound wraps the original code, intercepts any blocking calls, and provides an error if the blocking call was used incorrectly. In this study, BlockHound was used to detect erroneous blocking calls in open source projects which use RxJava or Project-Reactor. A JavaAgent was created to automate the process of adding BlockHound to a project. The selection of projects to test was done by evaluating the community usage, and selecting the projects with the most amount of stars and forks, as this indicates that the projects are widely used. The projects were tested with BlockHound, and the errors were saved to external log files for analysation. The study found that a considerable percentage of the projects investigated exhibited blocking violations. These violations were all caused by a low number of system calls, made from methods in threads that forbid blocking. Generalizable solutions to the violations were applied, and considered successful. / Samtidighet (concurrency) inom programmering är ett sätt att kombinera olika uppgifter, för att få utökad prestanda i ett program. Tidigare forskning har visat att concurrencybuggar är svåra att undvika, svåra att upptäcka och att dem ofta försämrar programmets prestanda. Reaktiv programmering skapar en abstraktion som gör det enklare att implementera komplexa samtidiga och asynkrona uppgifter. Reaktiv programmering i Java används ofta med hjälp av ett reaktivt ramverk, där två av de mer populära är RxJava och Project-reactor. Att blockera i en tråd som inte tillåter blockering kommer skapa concurrency buggar, som Javas kompilator inte varnar för. För att upptäcka felaktiga blockeringar kan ett verktyg som heter BlockHound användas. BlockHound omsluter den ursprungliga koden, fångar eventuella blockeringar, och skickar ett felmeddelande om en felaktig blockering har upptäckts. I den här studien har BlockHound använts för att hitta felaktiga blockeringar i open source projekt som använde sig av antingen RxJava eller Project-reactor. En JavaAgent skapades för att automatisera processen att lägga till BlockHound i projekten. Processen att välja projekt för testning gjordes genom att utvärdera hur stor användningen av projekten var, samt genom att välja de projekt med mest antal stjärnor och forks, eftersom de ger en bra indikering på att projekten används brett inom området. Projekten testades sedan med BlockHound, och loggarna sparades manuellt till externa loggfiler för analys. Studien fann att en betydande procent av projekten som undersöktes innehöll felaktiga blockeringar. Orsaken till dessa var ett fåtal systemanrop som kallades från trådar som inte tillåter blockering. Generaliserbara lösningar till dessa buggar testades, och ansågs vara lyckade.

Pour aborder le développement d'applications concurrentes et distribuées, le modèle de programmation à objets actifs procure une abstraction de haut niveau pour programmer de façon concurrente. Les objets actifs sont des entités indépendantes qui communiquent par messages asynchrones. Peu de systèmes à objets actifs considèrent actuellement une exécution multi-threadée. Cependant, introduire un parallélisme contrôlé permet d'éviter les coûts induits par des appels de méthodes distants. Dans cette thèse, nous nous intéressons aux enjeux que présentent les objets actifs multi-threadés, et à la coordination des threads pour exécuter de façon sûre les tâches d'un objet actif en parallèle. Nous enrichissons dans un premier temps le modèle de programmation, afin de contrôler l'ordonnancement interne des tâches. Puis nous exhibons son expressivité de deux façons différentes: d'abord en développant et en analysant les performances de plusieurs applications,puis en compilant un autre langage à objets actifs avec des primitives de synchronisation différentes dans notre modèle de programmation. Aussi, nous rendons nos objets actifs multi-threadés résilients dans un contexte distribué en utilisant les paradigmes de programmation que nous avons développé. Enfin, nous développons une application pair-à-pair qui met en scène des objets actifs multi-threadés. Globalement, nous concevons un cadre de développement et d'exécution complet pour les applications hautes performances distribuées. Nous renforçons notre modèle de programmation en formalisant nos contributions et les propriétés du modèle. Cela munit le programmeur de garanties fortes sur le comportement du modèle de programmation. / In order to tackle the development of concurrent and distributed applications, the active object programming model provides a high-level abstraction to program concurrent behaviours. Active objects are independent entities that communicate by mean of asynchronous messages. Very few of the existing active object frameworks consider a multi-threaded execution of active objects. Introducing a controlled parallelism enables removing some latency induced by remote method invocations. In this thesis, we take interest in the challenges of having multiple threads inside an active object, and in their safe coordination to execute tasks in parallel. We enhance this programming model by adding language constructs that control the internal scheduling of tasks. We then show its expressiveness in two ways: first with a classical approach, by developing and analysing the performance of several applications, and secondly, by compiling another active object language with different synchronisation primitives into our programming model. Also, we make multi-threaded active objects resilient in a distributed context through generic engineering constructs, and by using our programming abstractions. Finally, we develop a peer-to-peer application that shows multi-threaded active objects and their features in action. Overall, we design a thorough framework for the development and execution of high performance distributed applications. We reinforce our programming model by formalising our work and the model’s properties

The recent development of multi-core computer architectures has largely affected the creation of everyday applications, requiring the adoption of concurrent programming to significantly utilize the divided processing power of computers. Applications must be split into sections able to execute in parallel, without any of these sections conflicting with one another, thereby necessitating some form of synchronization to be declared. The most commonly used methodology is lock-based synchronization; although, to improve performance the most, developers must typically form complex, low-level implementations for large applications, which can easily create potential errors or hindrances. An abstraction from database systems, known as transactions, is a rising concurrency control design aimed to circumvent the challenges with programmability, composability, and scalability in lock-based synchronization. Transactions execute their operations speculatively and are capable of being restarted (or rolled back) when there exist conflicts between concurrent actions. As such issues can occur later in the lifespans of transactions, entire rollbacks are not that effective for performance. One particular method, known as nesting, was created to counter that drawback. Nesting is the act of enclosing transactions within other transactions, essentially dividing the work into pieces called sub-transactions. These sub-transactions can roll back without affecting the entire main transaction, although general nesting models only allow one sub-transaction to perform work at a time. The first main contribution in this thesis is SPCN, an algorithm that parallelizes nested transactions while automatically processing any potential conflicts that may arise, eliminating the burden of additional processing from the application developers. Two versions of SPCN exist: Strict, which enforces the sub-transactions' work to be made visible in a serialized order; and Relaxed, which allows sub-transactions to distribute their information immediately as they finish (therefore invalidation may occur after-the-fact and must be handled). Despite the additional logic required by SPCN, it outperforms traditional closed nesting by 1.78x at the lowest and 3.78x at the highest in the experiments run. Another method to alter transactional execution and boost performance is to relax the rules of visibility for parallel operations (known as their isolation). Depending on the application, correctness is not broken even if some transactions see external work that may later be undone due to a rollback, or if an object is written while another transaction is using an older instance of its data. With lock-based synchronization, developers would have to explicitly design their application with varying amounts of locks, and different lock organizations or hierarchies, to change the strictness of the execution. With transactional systems, the processing performed by the system itself can be set to utilize different rulings, which can change the performance of an application without requiring it to be largely redesigned. This notion leads to the second contribution in this thesis: AsR, or As-Serializable transactions. Serializability is the general form of isolation or strictness for transactions in many applications. In terms of execution, its definition is equivalent to only one transaction running at a time in a given system. Many transactional systems use their own internal form of locking to create Serializable executions, but it is typically too strict for many applications. AsR transactions allow the internal processing to be relaxed while additional meta-data is used external to the system, without requiring any interaction from the developer or any changes to the given application. AsR transactions offer multiple orders of magnitude more in throughput in highly-contentious scenarios, due to their capability to outlast traditional levels of isolation. / Master of Science

The Intel Galileo, inspired by the well-known Arduino board, is a development board with many possibilities because of its strength. The Galileo is has an Intel processor capable of running GNU/Linux and can be connected to the internet, which opens up the possibility to be controlled remotely. The programming language that comes with the Intel Galileo is the same as for the Arduino development boards, and is therefore very limited and does not utilize the Galileo’s entire strength. Our aim with this project is to integrate a more suitable programming language; a language that can make better use of the relatively powerful processor to control the components of the board. The programming language of choice is Erlang, and the reason is obvious. Erlang can be described as a process-oriented programming language based on the functional programming paradigm and its power in concurrency. The result of the project was the successful integration of a complete version of GNU/Linux on the board and the cross-compilation of Erlang/OTP onto the board. Having Erlang running on the system opens up many possibilities for future work, amongst all: creating Erlang programs for the Intel Galileo, integrating an effective API, and measuring the pros and cons of using Erlang on an Intel Galileo. / Intel Galileo är ett utvecklingskort som bygger på Arduinos succe. Den kommer med en kraftigare processor jämfort med Arduino Uno, och den har möjlighet att kunna köra GNU/Linux. Den har också en port för att kunna kopplas till internet och på så sätt kommunicera med andra enheter. Programmeringsspråket som rekommenderas för Intel Galileo är densamma som används för Arduinos utvecklingskort. Det finns däremot en möjlighet att kunna kombinera utvecklingskortet med ett programmeringsspråk som kan erbjuda mer funktionalitet och fortfarande vara enkelt. Vårt val hamnade på Erlang för den är ett funktionellt språk och har möjlighet att hantera olika processer. Tanken är att kunna behandla olika komponenter kopplade till utvecklingskortet som processer, som kan kommunicera med andra komponenter och med internet. Projektarbetet bestod av att undersöka ifall det är möjligt att kunna kombinera Erlang/OTP med Intel Galileon samt skriva en guide för hur implementeringen gick till. Att kombinera de två var lyckat och det öppnar upp möjligheter för fortsätta arbeten och försök.

Headlong Developments' application HeadmasterDev is currently adapted for a single user. To turn their application into a multi-user system the programming language Swift will be used. Furthermore, this thesis will evaluate whether Swift is an appropriate programming language for developing a server application, how to handle concurrency of shared resources and if it is possible to deploy the application on a operative system other than macOS. The result is that the concurrency model is dependent on the system's needs and that one should not commit to using Swift as the programming language for a server application, with some regard to the size of the application and it's uses. / Headlong Developments applikation HeadmasterDev är endast anpassad för en användare. För att kunna transformera deras applikation till ett fleranvändarsystem så kommer detta arbete att använda sig av programmeringsspråket Swift. Utöver detta kommer det även undersökas om programmeringsspråket Swift är lämpligt för denna typ av applikation, hur man bäst hanterar samtidighet av delade resurser och om det är möjligt att använda applikationen på en annan plattform än macOS. Resultatet kom att bli att hur man löser samtidighetsproblemen beror på systemets behov och att Swift inte är lämpligt för denna applikation med tanke på dess storlek och användningsområden.

Concurrent software has been widely utilizing in computer systems owing to the highly efficient computation. However, testing and verifying concurrent software remain challenging tasks. This matter is not only because of the non-deterministic thread interferences which are hard to reason about but also because of the large state space due to the simultaneous path and interleaving explosions. That is, the number of program paths in each thread may be exponential in the number of branch conditions, and also, the number of thread interleavings may be exponential in the number of concurrent operations. This dissertation presents a set of new methods, built upon symbolic execution, a program analysis technique that systematically explores program state space, for testing concurrent programs. By modeling both functional and non-functional properties of the programs as assertions, these new methods efficiently analyze the viable behaviors of the given concurrent programs. The first method is assertion guided symbolic execution, a state space reduction technique that identifies and eliminates redundant executions w.r.t the explored interleavings. The second method is incremental symbolic execution, which generates test inputs only for the influenced program behaviors by the small code changes between two program versions. The third method is SYMPLC, a technique with domain-specific reduction strategies for generating tests for the multitasking Programmable Logic Controller (PLC) programs written in languages specified by the IEC 61131-3 standard. The last method is adversarial symbolic execution, a technique for detecting concurrency related side-channel information leaks by analyzing the cache timing behaviors of a concurrent program in symbolic execution. This dissertation evaluates the proposed methods on a diverse set of both synthesized programs and real-world applications. The experimental results show that these techniques can significantly outperform state-of-the-art symbolic execution tools for concurrent software. / Doctor of Philosophy / Software testing is a technique that runs software as a black-box on computer hardware multiple times, with different inputs per run, to test if the software behavior conforms to the designed functionality by developers. Nowadays, programmers have been increasingly developing multithreaded and multitasking software, e.g., web browser and web server, to utilize the highly efficient multiprocessor hardware. This approach significantly improves the software performance since a large computing job can now decompose to a set of small jobs which can then distribute to concurrently running threads (tasks). However, testing multithreaded (multitask) software is extremely challenging. The most critical problem is the inherent non-determinism. Typically, executing sequential software with the same input data always results in the same output. However, running a multithreaded (multitask) software multiple times, even under the same input data, may yield different output in each run. The root reason is that concurrent threads (tasks) may interleave their running progress at any time; thus the internal software execution order may be altered unexpectedly, causing runtime errors. Meanwhile, finding such faults is difficult, since the number of all possible interleavings can be exponentially growing in the number of concurrent thread (task) operations. This dissertation proposes four methods to test multithreaded/multitask software efficiently. The first method summarizes the already-tested program behaviors to avoid future testing runs that cannot lead to new faults. The second method only tests program behaviors that are impacted by program changes. The third method tests multitask Programmable Logic Controller (PLC) programs by excluding infeasible testing runs w.r.t the PLC semantics. The last method tests non-functional program properties by systematic concurrency analysis. This dissertation evaluates these methods upon a diverse set of benchmarks. The experimental results show that the proposed methods significantly outperform state-of-the-art techniques for concurrent software analysis.

We propose a fully automated and dynamic method for generating likely invariants from multithreaded programs and then leveraging these invariants to infer atomic regions and diagnose concurrency errors in the software code. Although existing methods for dynamic invariant generation perform reasonably well on sequential programs, for multithreaded programs, their effectiveness often reduces dramatically in terms of both the number of invariants that they can generate and the likelihood of them being true invariants. We solve this problem by developing a new dynamic invariant generator, which consists of a new LLVM based code instrumentation tool, an INSPECT based thread interleaving explorer, and a customized inference engine inside Daikon. We have evaluated the resulting system on public domain multithreaded C/C++ benchmarks. Our experiments show that the new method is effective in generating high-quality invariants. Furthermore, the state and transition invariants generated by our new method have been proved useful both in error diagnosis and in identifying likely atomic regions in the concurrent software code. / Master of Science

Mycket forskning har gjorts för att hitta förbättrade sätt att lära ut concurrency. Allt från visualiseringsverktyg till spel-baserad inlärning och flippat klassrum. Dock så saknas forskning som jämför metoder och modeller som lär ut concurrency. Den här artikeln tar upp och tittar på resultat från studenter som studerar concurrent programmering genom att jämföra två olika moderna sätt att lära ut. Den tittar också på vilken metod/modell studenterna f ̈oredrar och håller dem mer engagerade. Författarna av denna artikel jämför ett spel-inlärnings tillvägagångssätt med ett flippat klassrum tillvägagångssätt. Spel-inlärnings tillvägagångssättet som används i denna artikel är utvecklad av Dr. Robert Marmorstein och använder sig av spelet OpenTTD [1]. Studenterna lär sig om race condition, deadlock och starvation genom att använda semaforer(järnvägssignaler) för att förhindra kollisioner. Det flippade klassrum tillvägagångssättet i denna artikel används i en flertrådad programmeringskurs på Malmö Universitet. Efter att båda tillvägagångssätten har genomförts tar studenterna ett test och svarar på ett frågeformulär för att se hur mycket studenterna har lärt sig, hur engagerade de är och vad de föredrar. För att få mer exakta resultat får bara studenterna delta vid ett av tillfällena där tillvägagångssätten genomförs. Resultaten från den här studien gynnar OpenTTD labbens tillvägagångssätt då studenterna verkar vara mer engagerade och föredra den lite mer. Studenterna som deltog i OpenTTD labben gjorde bättre ifrån sig på testet när det kommer till att förstå hur man förhindrar/löser varje synkroniseringsproblem, medans de studenterna som deltog i det flippade klassrummet gjorde lite bättre ifrån sig när det kom till att förklara/beskriva problemet. / Much research has been done to find ways to improve teaching concurrency, from visualization tools to game-based learning and flipped classroom. However, research on comparing these methods or models when teaching concurrency are lacking. This paper looks at the different results from students who are studying concurrent programming by comparing two different modern ways of teaching. It also looks at which method/model students prefer and keeps them more engaged. The authors of this paper compare a game-based learning approach to a flipped classroom approach. The game-based learning approach used in this paper is developed by Dr. Robert Marmorstein and uses the game OpenTTD [1]. The students learn about race condition, deadlock and starvation by using semaphores (railway signals) to prevent collisions. The flipped classroom approach in this paper is used in a concurrent programming course at Malmö University. After both of the approaches have been completed, the students take a test and answer a survey to see how much the students learn, how engaged they are and what they prefer. To gain an accurate result, each student that took part in the study only participated in one of the approaches. The results of the survey favor the OpenTTD lab approach as the students were more engaged during the exercise and preferred the exercise more. The students that participated in the OpenTTD lab also did better on the test when it came to explaining how to prevent/solve each synchronization problem, while in the flipped classroom students did better when it came to describing the problem.

Efficient and safe memory management is a hard problem. Garbage collection promises automatic memory management but comes with the cost of increased memory footprint, reduced parallelism in multi-threaded programs, unpredictable pause time, and intricate tuning parameters balancing the program's workload and designated memory usage in order for an application to perform reasonably well. Existing research mitigates the above problems to some extent, but programmer error could still cause memory leak by erroneously keeping memory references when they are no longer needed. We need a methodology for programmers to become resource aware, so that efficient, scalable, predictable and high performance programs may be written without the fear of resource leak. Linear logic has been recognized as the formalism of choice for resource tracking. It requires explicit introduction and elimination of resources and guarantees that a resource cannot be implicitly shared or abandoned, hence must be linear. Early languages based on linear logic focused on Curry-Howard correspondence. They began by limiting the expressive powers of the language and then reintroduced them by allowing controlled sharing which is necessary for recursive functions. However, only by deviating from Curry-Howard correspondence could later development actually address programming errors in resource usage. The contribution of this dissertation is a simple, safe, and efficient approach introducing linear resource ownership semantics into C++ (which is still a widely used language after 30 years since inception) through linear pointer, a smart pointer inspired by linear logic. By implementing various linear data structures and a parallel, multi-threaded memory allocator based on these data structures, this work shows that linear pointer is practical and efficient in the real world, and that it is possible to build a memory management stack that is entirely leak free. The dissertation offers some closing remarks on the difficulties a formal system would encounter when reasoning about a concurrent linear data algorithm, and what might be done to solve these problems.

L'intégration de composants dans un système peut s'avérer difficile lorsque ces composants ont été conçus selon différents paradigmes ou s'ils se basent sur différents cadres de temps devant être synchronisés. Cette synchronisation peut être dirigée par les évènements (un évènement est provoqué par un autre), ou dirigée par le temps (un évènement se produit parce qu'il en est l'heure). En considérant que chaque composant admet son propre cadre de temps et qu'ils peuvent ne pas être reliés, il est possible qu'une unique ligne de temps globale n'existe pas.Nous nous intéressons à la spécification de schémas de synchronisation pour de tels systèmes polychrones et polytemporisés. Notre étude nous a mené à la conception de modèles sémantiques pour un langage temporisé à évènements discrets, appelé TESL et développé par Boulanger et al. Ce langage a été utilisé pour coordonner la simulation de modèles composites et pour tester l'intégration de systèmes.Dans cette thèse, nous présentons une sémantique dénotationnelle fournissant une compréhension précise et logiquement cohérente du langage. Puis nous proposons une sémantique opérationnelle afin de dériver des traces d'exé-cutions satisfaisant une spécification TESL. Celui-ci a été utilisé pour les problématiques de test des systèmes, à travers l'implantation d'un solveur nommé Heron. Pour résoudre la question de cohérence et de correction de ces règles sémantiques, nous avons également développé une sémantique intermédiaire coinductive reliant les deux sémantiques dénotationnelles et opérationnelles. Nous établissons des propriétés sur la relation entre les deux sémantiques: correction, complétude, progrès ainsi que terminaison locale. Enfin, notre formalisation ainsi que les preuves associées ont été entièrement mécanisées dans l'assistant de preuve Isabelle/HOL. / Integrating components into systems turns out to be difficult when these components were designed according to different paradigms or when they rely on different time frames which must be synchronized. This synchronization may be event-driven (an event occurs because another event occurs) or time-driven (an event occurs because it is time for it to occur). Considering that each component admits its own time frame, and that they may not be related, a unique global time line may not exist.We are interested in specifying synchronization patterns for such polychronous and polytimed systems. Our study had led us to design semantic models for a timed discrete-event language, called the TESL language developed by Boulanger et al. This language has been used for coordinating the simulation of composite models and testing system integration.In this thesis, we present a denotational semantics providing an accurate and logic-consistent understanding of the language. Then we propose an operational semantics to derive satisfying runs from TESL specifications. It has been used for testing purposes, through the implementation of a solver, named Heron. To tackle the issue of the consistency and correctness of these semantic rules, we developed a co-inductive intermediate semantics that relates both the denotational and the operational semantics. Then we establish properties over the relation of our semantic models: soundness, completeness and progress, as well as local termination. Finally, our formalization and these proofs have been fully mechanized in the Isabelle/HOL proof assistant.