No description available.

No description available.

Concurrency errors are notoriously difficult to debug because they may occur only under unexpected thread interleavings that are difficult to identify and reproduce. These errors are increasingly important as recent hardware trends compel developers to write more concurrent software and to provide more concurrent abstractions. This thesis presents algorithms that dynamically and systematically explore a program's thread interleavings to manifest concurrency bugs quickly and reproducibly, and to provide precise incremental coverage guarantees. Dynamic concurrency testing tools should provide (1) fast response -- bugs should manifest quickly if they exist, (2) reproducibility -- bugs should be easy to reproduce and (3) coverage -- precise correctness guarantees when no bugs manifest. In practice, most tools provide either fast response or coverage, but not both. These goals conflict because a program's thread interleavings exhibit exponential state- space explosion, which inhibits fast response. Two approaches from prior work alleviate state-space explosion. (1) Partial-order reduction provides full coverage by exploring only one interleaving of independent transitions. (2) Bounded search provides bounded coverage by enumerating only interleavings that do not exceed a bound. Bounded search can additionally provide guarantees for cyclic state spaces for which dynamic partial-order reduction provides no guarantees. Without partial-order reduction, however, bounded search wastes most of its time exploring executions that reorder only independent transitions. Fast response with coverage guarantees requires both approaches, but prior work failed to combine them soundly. We combine bounded search with partial-order reduction and extensively analyze the space of dynamic, bounded partial-order reduction strategies. First, we prioritize with a best-first search and show that heuristics that combine these approaches find bugs quickly. Second, we restrict partial-order reduction to combine approaches while maintaining bounded coverage. We specialize this approach for several bound functions, prove that these algorithms guarantee bounded coverage, and leverage dynamic information to further reduce the state space. Finally, we bound the partial order on a program's transitions, rather than the total order on those transitions, to combine these approaches without sacrificing partial-order reduction. This algorithm provides fast response, incremental coverage guarantees, and reproducibility. We manifest bugs an order of magnitude more quickly than previous approaches and guarantee incremental coverage in minutes or hours rather than weeks, helping developers find and reproduce concurrency errors. This thesis makes bounded stateless model checking for concurrent programs substantially more efficient and practical. / text

Context: Standard transport layer protocols like UDP, TCP, andSCTP use only one access technology at a time. Concurrent MultipathTransmission (CMT), has been developed for parallel use of the access technologies. The main theme of this thesis work is to implement CMT in real-time and evaluate the impact of various scheduling algorithms on its performance. Objectives: The main objectives of this thesis are to implement a de-multiplexer at the source, re-sequencer at the receiver and to investigate some of the heuristics and analyzing their impact based on some performance metrics. Methods: Thorough understanding on this topic is attained by literature review of related works. To implement and evaluate the different scheduling patterns an experimental test bed is set up. For thetransmission of data, socket programming in Python is used. Varying various parameters that are involved in the experiment, performance metrics were measured and based on them statistical analysis is carried out for proper evaluation. Results: CMT is implemented in real-time test bed and concurrency is validated. Weighted Round-Robin has better performance compared to that of Round-Robin when the size of the packet is large whereas both exhibit nearly same behavior for smaller packet sizes. Conclusions: It can be concluded that Weighted Round-Robin attains higher throughput. It can be possibly due to more load of fragmentation when large packets are transmitted on the high reliable path and hence better performance than Round-Robin. There is need for further evaluation of other metrics like delay, jitter and using other scheduling mechanisms and in other environments as well.

Concurrency has recently come to the forefront of computing as multi-core processors become more and more common. General purpose graphics processing unit computing brings with them new language support for dealing with co-processor environments such as OpenCL and CUDA. Programming language support for multi-core architectures introduces a fundamentally new mechanism for modularity--a kernel. Developers attempting to leverage these mechanism to separate concerns often incur unanticipated performance penalties. My proposed solution aims to preserve the benefits of kernel boundaries for modularity, while at the same time eliminate these inherent costs at compile time and execution. KFusion is a prototype tool for transforming programs written in OpenCL to make them more efficient. By leveraging loop fusion and deforestation, it can eliminate the costs associated with compositions of kernels that share data. Case studies show that Kfusion can address key memory bandwidth and latency bottlenecks and result in substantial performance improvements. / Graduate

In this thesis, we propose a family of concurrency control protocols for high data contention database environments. The first one is called the Prudent-Precedence Concurrency Control (PPCC) protocol. It is prudently more aggressive in permitting more serializable schedules than two-phase locking and maintains a restricted precedence among conflicting transactions and commits the transactions according to the serialization order established in the executions. The second one is a family of hierarchical concurrency control protocols called the Hierarchical Precedence Concurrency Control (HPCC) protocols. It maintains cycle-free precedence hierarchies for conflicting transactions. Conflicting operations are allowed to proceed only if the hierarchical orderings of precedence is not violated. Transactions also commit based on the serialization order established during the executions. Detailed simulation models have been implemented for all these protocols and extensive experiments have been conducted to evaluate the performance of the proposed approaches. The results demonstrate that the proposed algorithms outperform the two-phase locking and optimistic concurrency control over a wide range of system workloads.

Mazurkiewicz traces were introduced by A. Mazurkiewicz in 1977 as a language representation of partial orders to model "true concurrency". The theory of Mazurkiewicz traces has been utilised to tackle not only various aspects of concurrency theory but also problems from other areas, including combinatorics, graph theory, algebra, and logic. However, neither Mazurkiewicz traces nor partial orders can model the "not later than" relationship. In 1995, comtraces (combined traces) were introduced by Janicki and Koutny as a formal language counterpart to finite stratified order structures. They show that each comtrace uniquely determines a finite stratified order structure, yet their work contains very little theory of comtraces. This thesis aims at enriching the tools and techniques for studying the theory of comtraces. Our first contribution is to introduce the notions of absorbing monoids, generalised comtrace monoids, partially commutative absorbing monoids, and absorbing monoids with compound generators, all of which are the generalisations of Mazurkiewicz trace and comtrace monoids. We also define and study the canonical representations of these monoids. Our second contribution is to define the notions of non-serialisable steps and utilise them to study the construction which Janicki and Koutny use to build stratified order structures from comtraces. Moreover, we show that any finite stratified order structure can be represented by a comtrace. Our third contribution is to study the relationship between generalised comtraces and generalised stratified order structures. We prove that each generalised comtrace uniquely determines a finite generalised stratified order structure. / Thesis / Master of Computer Science (MCS)

International Telemetering Conference Proceedings / October 26-29, 1992 / Town and Country Hotel and Convention Center, San Diego, California / Today's complex implementations of integrated packet and circuit switched digital communications networks demand that the software used for controlling these systems be robust, fault tolerant, and capable of runtime recovery from all but the most severe of operational errors. The typical modern switched communications system includes the use of multiple circuit switches, each with potentially thousands of end-user interfaces. Further, these switches are often inter-connected to each other via high-capacity trunks. A single connection between two end-user interfaces often traverses a number of intermediate circuit switches in order to effect the end-to-end communications desired. In this complex, distributed environment, the establishment and dissolution of end-to-end user connections involve far more than simple binary connection states indicating the existence, or non-existence, of a link. More commonly, a single end-to-end connection requires multiple node links across multiple, heterogeneous interfaces. The command and control software used to establish, monitor, and dissolve these connections must be capable of dealing with errors which arise at any node along the way in a consistent and reliable manner. Most critically, the system software must be capable of maintaining an accurate, multi-level mapping of distributed resources' availability, allocation, and status. Further, the software must have the capability of "healing itself" during operational run-time when it can, and of accurately reporting the nature of inconsistencies caused by anomalous events that cannot be fixed on the fly. The Edwards Digital Switch (EDS), developed by CSTI, provides a case study of possible solutions, and potential pitfalls, that can arise in the design, development, and implementation of the controlling software in today's dynamic, distributed communications' system architectures.

Ces travaux portent sur l'étude des jeux concurrents et temporisés. Ces deux types de jeux sont des modèles très utilisés en synthèse de contrôleur. Dans des situations où plusieurs agents interagissent, les notions de stratégies gagnantes utilisés jusqu'ici ne suffisent plus et il est nécessaires de s'inspirer de notions issus de la théorie des jeux. Le principal concept étudié dans ce domaine est celui d'équilibre de Nash. Nous proposons une transformation qui permet de calculer les équilibres dans les jeux concurrents en se ramenant à un calcul de stratégies gagnantes. Beaucoup de travaux ont déjà porté sur les calculs des stratégies gagnantes, et nous pouvons tirer parti des algorithmes à notre disposition. Pour le calcul des équilibres dans les jeux temporisés, nous montrons qu'il est possible de se ramener au cas des jeux concurrents. Nous proposons des algorithmes pour le calcul des équilibres, d'abord avec des objectifs classiques, puis nous proposons un cadre plus général qui permet de décrire des préférences plus quantitatives. Nous étudions également la complexité théorique des problèmes de décisions associés. Enfin, nous présentons un outil implémentant l'un des algorithmes que nous avons développé. / This work focuses on the study of concurrent and timed games. These two classes of games have been useful models in controller synthesis. In situations where several agents interact, the notion of winning strategies used so far is not adapted and it is necessary to adopt concepts from game theory. The main concept considered in this area is that of Nash equilibrium. For concurrent games, we propose a transformation which draw a parallel between equilibria and winning strategies. Many works have focused on the computation of winning strategies and we can take advantage of the available algorithms. To compute equilibria in timed games we show that it is possible to reduce them to concurrent games. We propose algorithms for the computation of equilibria, first with classical objectives. Then, we propose a more general framework, in which more quantitative preferences can be described. We also study the theoretical complexity of the associated decision problems. Finally, we present a tool that implements one of the algorithms that we developed.

Multicore processors have become prevalent and spurred interest in scalable synchronization mechanisms, such as Read-Copy Update. While RCU is popular in monolithic operating system kernels it has yet to see an implementation in a microkernel environment. In this thesis we design and implement RCU for the microkernel operating system HelenOS. Moreover, we explore potential uses of RCU in HelenOS and illustrate its utility in both the kernel and user space. Benchmarks demonstrate that the RCU implementation provides linearly scalable read-sides and incurs significantly less overhead than traditional locking even if uncontended. Furthermore, RCU was used in user space to speed up traditional locking 2.6 times in the common case. In the kernel, RCU ensured linear scalability of a previously non-scalable futex subsystem. Powered by TCPDF (www.tcpdf.org)