Multi-core processors require a program to be decomposable into independent parts that can execute in parallel in order to scale performance with the number of cores. But parallel programming is hard especially when the program requires state, which many system programs use for optimization, such as for example a cache to reduce disk I/O. Most prevalent parallel programming models do not support a notion of state and require the programmer to synchronize state access manually, i.e., outside the realms of an associated optimizing compiler. This prevents the compiler to introduce parallelism automatically and requires the programmer to optimize the program manually. In this dissertation, we propose a programming language/compiler co-design to provide a new programming model for implicit parallel programming with state and a compiler that can optimize the program for a parallel execution. We define the notion of a stateful function along with their composition and control structures. An example implementation of a highly scalable server shows that stateful functions smoothly integrate into existing programming language concepts, such as object-oriented programming and programming with structs. Our programming model is also highly practical and allows to gradually adapt existing code bases. As a case study, we implemented a new data processing core for the Hadoop Map/Reduce system to overcome existing performance bottlenecks. Our lambda-calculus-based compiler automatically extracts parallelism without changing the program's semantics. We added further domain-specific semantic-preserving transformations that reduce I/O calls for microservice programs. The runtime format of a program is a dataflow graph that can be executed in parallel, performs concurrent I/O and allows for non-blocking live updates.

Un programme concurrent est composé de plusieurs unités logiques : les processus. Chaque processus a un comportement qui lui est propre : il exécute ses actions de façon séquentielle. Un objectif important est de s'assurer que de tels systèmes concurrents complexes soient cependant exempts de défaut. Cette problématique est étudiée dans le cadre de la théorie de la concurrence. Quand plusieurs processus s’exécutent en parallèle, l’ordre d’exécution des actions du programme global n’est plus déterminé. On assiste au fameux phénomène "d’explosion combinatoire" faisant référence au très grand nombre d’exécutions globales possibles. Les diverses techniques et méthodes d'analyse existantes (model checking, analyse statique, tests automatisés, etc) se heurtent irrémédiablement à cette "explosion". Cette thèse s'inscrit dans un projet à long terme d'étude quantitative de ce phénomène et de développement des techniques d’analyse statistique basées sur la génération aléatoire uniforme. Notre objectif dans cette thèse est de traiter une composante fondamentale de la concurrence : la synchronisation. Ce mécanisme permet aux processus de communiquer entre eux. Dans cette thèse nous proposons un modèle combinatoire de structures croissantes pour modéliser les exécutions de programmes concurrents synchronisés. Avec des outils de combinatoire analytique nous obtenons plusieurs résultats exacts et asymptotiques sur le nombre moyen d'exécutions dans des sous-classes de programmes concurrents. Nous présentons aussi plusieurs algorithmes de génération aléatoire uniforme de structures croissantes et de leurs étiquetages. / A concurrent program is a composition of several logical blocks: the processes. Each process has its own behavior, independent from the others: it sequentially runs its actions. An important goal is to ensure that such concurrent complex systems are faultless. This problem is studied in the field of concurrency theory. When several process are running in parallel, the running order of the actions of the total program is no more decided. This is the well-known "combinatorial explosion" phenomena, meaning that the number of possible runs of the global program is huge. The analysis techniques and methods existing (model checking, static analysis, automated testing, etc) are irremediably limited by this "explosion". This thesis is a part of a long-term project about the quantitative study of this phenomena and the development of statistic analysis methods based on the uniform random generation. Our specific goal is to study a fundamental principle of the concurrency theory: the synchronization. This mechanism allows communications between the processes. In this thesis we propose a combinatorial model of increasingly labeled structures to deal with runs of synchronized concurrent programs. Using the tools of analytic combinatorics we obtain close formulas and asymptotic equivalents for the average number of runs in several subclasses of concurrent programs. We also present algorithms of uniform random generation of increasingly labeled structures and for their increasing labelings.

For software to take advantage of modern multicore processors, it must be safely concurrent and it must scale. Many techniques that allow safe concurrency do so at the expense of scalability. Coarse grain locking allows multiple threads to access common data safely, but not at the same time. Non-Blocking Synchronization and Transactional Memory techniques optimistically allow concurrency, but only for disjoint accesses and only at a high performance cost. Relativistic programming is a technique that allows low overhead readers and joint access parallelism between readers and writers. Most of the work on relativistic programming has assumed a single writer at a time (or, in partitionable data structures, a single writer per partition), and single writer solutions cannot scale on the write side. This dissertation extends prior work on relativistic programming in the following ways: 1) It analyses the ordering requirements of lock-based and relativistic programs in order to clarify the differences in their correctness and performance characteristics, and to define precisely the behavior required of the relativistic programming primitives. 2) It shows how relativistic programming can be used to construct efficient, scalable algorithms for complex data structures whose update operations involve multiple writes to multiple nodes. 3) It shows how disjoint access parallelism can be supported for relativistic writers, using Software Transactional Memory, while still allowing low-overhead, linearly-scalable, relativistic reads.

V dnešní době jsou vícevláknové programy běžné a s nimi i chyby v souběžnosti. Během posledních let bylo vytvořeno mnoho technik pro detekci takovýchto chyb, a i přesto mají vývojáři softwaru problém nalézt správné nástroje pro analýzu svých programů. Důvod je jednoduchý, fungující neznamená vždy praktický. Hodně nástrojů implementujících detekční techniky je obtížně použitelných, přizpůsobených pro konkrétní typy programů nebo synchronizace, nebo špatně škálují, aby zvládly analyzovat rozsáhlý software. Pro některé typy chyb v souběžnosti dokonce ani neexistují nástroje pro jejich detekci, i přesto že vývojáři softwaru na tyto chyby často narážejí ve svých programech. Hlavním cílem této práce je navrhnout nové techniky pro detekci chyb ve vícevláknových programech. Tyto techniky by měly být schopny analyzovat rozsáhlé programy, umožnit detekci méně studovaných typů chyb v souběžnosti, a podporovat širokou škálu programů s ohledem na to, jaké programové konstrukce používají.

This paper investigates alternative scheduling for game objects in a game engine by using priority based algorithms and comparing different priority assigning methods. Research concerning commercial game engines, game loops, concurrency and scheduling was performed. Three different scheduling algorithms were created and tested using a varying amount of game objects between two different testing scenarios. The results showed that using priority based scheduling gave a slight increase in average frames  per second (FPS) as well as boosting logical update performance of prioritized objects, however overall performance was decreased. The reason this decrease in performance occurred could have been due to the way the scheduler was implemented, and despite the decrease in performance using a priority based scheduling system was considered feasible within certain game engines. / Denna uppsats undersöker alternativa sätt för schemaläggning av spelobjekt i en spelmotor genom att använda prioriteringsbaserade algoritmer och jämföra olika tilldelningssätt för prioritetsmetoder. Forskning gällande kommersiella spelmotorer, ''game loops'', parallellisering och schemaläggning utfördes. Tre olika schemaläggningsalgoritmer skapades och testades med ett varierande antal spelobjekt i två olika testscenarion. Resultaten visade att användning av prioritetsbaserad schemaläggning gav en lätt ökning av det genomsnittliga antalet bilder per sekund (FPS) och gav bättre logikuppdateringsprestanda för prioriterade objekt. Den totala prestandan minskade dock. Anledningen till att denna minskning i prestanda skedde kan bero på hur schemaläggaren implementerades, men trots denna prestandaminskning ansågs schemaläggningssystemet vara möjlig inom vissa spelmotorer.

No description available.

With the increasing interest in Virtual/Augmented Reality, the next generation of application platforms is emerging in the form of immersive and engaging experiences. The company Dewire Knightec is exploring an application platform based on the web technology WebXR where users can interact with multiple applications simultaneously. However, numerous independent applications rendering content in the same 3D environment can lead to objects intersecting and occluding, leading to visual conflicts. In this thesis work, we discuss the concept of visual conflicts and avoidance strategies. We present a fully working prototype of a conflict mitigation framework for concurrent WebXR applications. The framework mitigates conflicts using two main collision avoidance strategies in the form of multiple render options and position offsetting. The proposed framework is demonstrated in a scenario where applications render contents on top of buildings in the user’s surroundings. By running multiple applications, a user can for example read a restaurant menu, see mall opening hours, and get travel directions simultaneously. The feasibility and efficiency of the proposed avoidance strategy in developed framework has been evaluated using a focus group of developers and software architects. After the evaluation, the framework can be summarized as a good foundation for future multi-application XR platforms.

Predicate abstraction is a key enabling technology for applying model checkers to programs written in mainstream languages. It has been used very successfully for debugging sequential system-level C code. Although model checking was originally designed for analysing concurrent systems, there is little evidence of fruitful applications of predicate abstraction to shared-variable concurrent software. The goal of the present thesis is to close this gap. We propose an algorithmic solution implementing predicate abstraction that targets safety properties in non-recursive programs executed by an unbounded number of threads, which communicate via shared memory or higher-level mechanisms, such as mutexes and broadcasts. As system-level code makes frequent use of such primitives, their correct usage is critical to ensure reliability. Monotonicity - the property that thread actions remain executable when other threads are added to the current global state - is a natural and common feature of human-written concurrent software. It is also useful: if every thread’s memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unspecified. In this thesis, we show that the process of obtaining finite-data thread abstrac tions for model checking is not always compatible with monotonicity. Predicate-abstracting certain mainstream asynchronous software such as the ticket busy-wait lock algorithm results in non-monotone multi-threaded Boolean programs, despite the monotonicity of the input program: the monotonicity is lost in the abstraction. As a result, the unbounded thread Boolean programs do not give rise to well quasi-ordered systems [1], for which sound and complete safety checking algorithms are available. In fact, safety checking turns out to be undecidable for the obtained class of abstract programs, despite the finiteness of the individual threads’ state spaces. Our solution is to restore the monotonicity in the abstract program, using an inexpensive closure operator that precisely preserves all safety properties from the (non-monotone) abstract program without the closure. As a second contribution, we present a novel, sound and complete, yet empirically much improved algorithm for verifying abstractions, applicable to general well quasi-ordered systems. Our approach is to gradually widen the set of safety queries during the search by program states that involve fewer threads and are thus easier to decide, and are likely to finalise the decision on earlier queries. To counter the negative impact of "bad guesses", i.e. program states that turn out feasible, the search is supported by a parallel engine that generates such states; these are never selected for widening. We present an implementation of our techniques and extensive experiments on multi-threaded C programs, including device driver code from FreeBSD and Solaris. The experiments demonstrate that by exploiting monotonicity, model checking techniques - enabled by predicate abstraction - scale to realistic programs even of a few thousands of multi-threaded C code lines.

The work presented in this document in an account of my work as a PhD student at LIX, Ecole Polytechnique, in the COMETE team under the supervision of Catuscia Palamidessi. During these studies, I have been in interested in the various aspects of concurrency covered by the COMETE team activities. The initial goal of my thesis was to investigate the aspects related to process calculi based formalisms to express and analyze Security Protocols. The ultimate goal was to makes some advances towards the automatic verification of security properties. In particular, I was interested in information-hiding protocols which require no cryptography, but normally use randomized mechanisms and therefore exhibit probabilistic behavior. Information hiding protocols are used typically in networks, and they are run by parties that reside in different locations of the system, and therefore interact asynchronously. The first work that I did was to try to give a correct meaning to the various notions of formal asynchronous communications used in various models, in particular between the field of concurrency and the field of distributed computing, where this was a recurrent question. These results are presented in the first part of this document. Being interested in the formal aspects of information-hiding problems, I took part in the preparation of the journal version of [BP09], and started preparing an automated probabilistic anonymity checker based on the formalism presented in this document. This lead to an initial draft of an implementation presented in http://vamp.gforge.inria.fr/. The formalism for this analysis is presented in the fourth part of this document. Another aspect of the verification of information hiding properties is that it requires to compute the probabilities of the possible outcomes for each scheduler. For this reason, this application quickly turned out to be highly inefficient. However, in an asynchronous system, a lot of transitions are confluent, which means that when evaluating a process, it is only necessary to choose one of the two confluent branches. Hence, I have worked on formalizing the possible optimizations based on the possible confluent computations. This work is presented in the second part of the document. Another interesting aspects of probabilistic protocols is the possibility to con- sider infinite runs. By doing such consideration, it is possible to verify the correction of some probabilistic protocols. For instance, in the case of the Crowds routing protocol, presented in Section 5.3, the protocol is considered correct because the probability of running into an infinite execution is null, hence the message will eventually be delivered. For this reason, I got interested in extending the meaning of a asynchronous probabilistic computations to the case of an infinite execution. As a matter of fact, the combination of infinite computation, confluence and probability is not easy to treat in the general case. The problem of confluence in concurrency is solved in an elegant way in an asyn- chronous paradigm called Concurrent Constraint Programming (CCP). Hence, I decided to study infinite computations in a probabilistic version of CCP. The problem, however, is that the meaning of the result of an infinite probabilistic computation was still an open problem also in that context. Hence, I studied a possible way to define this result, using the notion of valuations and sober spaces, and applied it to give a denotational semantics to probabilistic CCP, including infinite computations. This work is presented in the third part of the document. I have chosen a specific order for the various parts of this document that follows the various formal models that are used, in order to present each result along with the corresponding formalism. * In the first and second parts, I present the formal concurrent models, and in the particular asynchronous ones. * In the third part, I present the probabilistic CCP. This part also presents mathematic structures for the representation of infinite probabilistic executions. * Eventually, an application of both asynchronous and probabilistic models to the case of probabilistic information hiding is presented in the fourth part.

Model checking is an automatic formal verification technique for establishing correctness of systems. It has been widely used in industry for analysing and verifying complex safety-critical systems in application domains such as avionics, medicine and computer security, where manual testing is infeasible and even minor errors could have dire consequences. In our increasingly parallelised world, concurrency has become pivotal and seamlessly woven within programming paradigms, however, extremely challenging when it comes to modelling and establishing correctness of intended behaviour. Tools for model checking concurrent systems face severe limitations due to scalability problems arising from the need to examine all possible interleavings (schedules) of executions of parallel components. Moreover, concurrency poses additional challenges to model checking, giving rise to phenomena such as nondeterminism, deadlock, livelock, etc. In this thesis we focus on adapting and developing novel model-checking techniques for concurrent systems in the setting of the process algebra CSP and its primary model checker FDR. CSP allows for a compact modelling and precise analysis of event-based concurrency, grounded on synchronous message passing as a fundamental mechanism of inter-component communication. In particular, we investigate techniques based on symbolic model checking, static analysis and abstraction, all of them exploiting the compositionality inherent in CSP and targeting to increase the scale of systems that can be tractably analysed. Firstly, we investigate symbolic model-checking techniques based on Boolean satisfiability (SAT), which we adapt for the traces model of CSP. We tailor bounded model checking (BMC), that can be used for bug detection, and temporal k-induction, which aims at establishing inductiveness of properties and is capable of both bug finding and establishing the correctness of systems. Secondly, we propose a static analysis framework for establishing livelock freedom of CSP processes, with lessons for other concurrent formalisms. As opposed to traditional exhaustive state-space exploration, our framework employs a system of rules on the syntax of a process to calculate a sound approximation of its fair/co-fair sets of events. The rules either safely classify a process as livelock-free or report inconclusiveness, thereby trading accuracy for speed. Finally, we develop a series of abstraction/refinement schemes for the traces, stable-failures and failures-divergences models of CSP and embed them into a fully automated and compositional CEGAR framework. For each of those techniques we present an implementation and an experimental evaluation on a set of CSP benchmarks.