abstract: Debugging is a boring, tedious, time consuming but inevitable step of software development and debugging multiple threaded applications with user interactions is even more complicated. Since concurrency and synchronism are normal features in Android mobile applications, the order of thread execution may vary in every run even with the same input. To make things worse, the target erroneous cases may happen just in a few specific runs. Besides, the randomness of user interactions makes the whole debugging procedure more unpredictable. Thus, debugging a multiple threaded application is a tough and challenging task. This thesis introduces a replay mechanism for debugging user interactive multiple threaded Android applications. The approach is based on the 'Lamport Clock' concept, 'Event Driven' implementation and 'Client-Server' architecture. The debugger tool described in this thesis provides a user controlled debugging environment where users or developers are allowed to use modified record application to generate a log file. During the record time, all the necessary events like thread creation, synchronization and user input are recorded. Therefore, based on the information contained in the generated log files, the debugger tool can replay the application off-line since log files provide the deterministic order of execution. In this case, user or developers can replay an application as many times as they need to pinpoint the errors in the applications. / Dissertation/Thesis / M.S. Computer Science 2012

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.

Concurrency bugs are extremely hard to detect due to huge interleaving space. They are happening in the real world more often because of the prevalence of multi-threaded programs taking advantage of multi-core hardware, and microservice based distributed systems moving more and more applications to the cloud. As the most common non-deadlock concurrency bugs, atomicity violations are studied in many recent works, however, those methods are applicable only to single-variable atomicity violation, and don't consider the specific challenge in distributed systems that have both pessimistic and optimistic concurrency control. This dissertation presents a tool using model checking to predict atomicity violation concurrency bugs involving two shared variables or shared resources. We developed a unique method inferring correlation between shared variables in multi-threaded programs and shared resources in microservice based distributed systems, that is based on dynamic analysis and is able to detect the correlation that would be missed by static analysis. For multi-threaded programs, we use a binary instrumentation tool to capture runtime information about shared variables and synchronization events, and for microservice based distributed systems, we use a web proxy to capture HTTP based traffic about API calls and the shared resources they access including distributed locks. Based on the detected correlation and runtime trace, the tool is powerful and can explore a vast interleaving space of a multi-threaded program or a microservice based distributed system given a small set of captured test runs. It is applicable to large real-world systems and can predict atomicity violations missed by other related works for multi-threaded programs and a couple of previous unknown atomicity violation in real world open source microservice based systems. A limitation is that redundant model checking may be performed if two recorded interleaved traces yield the same partial order model.

In this thesis an operational semantics for a subset of the Java Virtual Machine (JVM) is developed and presented. The subset contains standard operations such as control flow, computation, and memory management. In addition, the subset contains a treatment of parallel threads of execution. The operational semantics are embedded into a $µ$-calculus based proof assistant, called the VeriCode Proof Tool (VCPT). VCPT has been developed at the Swedish Institute of Computer Science (SICS), and has powerful features for proving inductive assertions. Some examples of proving properties of programs using the embedding are presented. / I det här examensarbetet  presenteras en operationell semantik för en delmängd av Javas virtuella maskin. Den delmängd som hanteras innehåller kontrollflöde, beräkningar och minneshantering. Vidare beskrivs  semantiken för parallella exekveringstrådar. Den operationella semantiken formaliseras i en bevisassistent for $µ$-kalkyl, VeriCode Proof Tool (VCPT). VCPT har utvecklats vid Swedish Institiute of Computer Science (SICS), och har kraftfulla tekniker för att bevisa induktiva påståenden. Några exempel på bevis av egenskaper hos program användandes formaliseringen presenteras också.

The demands for an increase in productivity and reduced assembly costs require engineers to automate solutions that replace manual labor. This work concentrated on a common assembly primitive, threaded fastener insertion, in an effort to determine the nature of contact between a bolt and nut during thread mating. The assembly problem was initially simplified as a two-dimensional analysis to gain an understanding about how contacts between the bolt and nut change during counter-clockwise motion. Tessellated solid models were used during three-dimensional collision analysis in such a way that the approximate location of the contact point was enumerated. The advent of a second contact point presented a more constrained contact state since we are interested in maintaining both contacts; thus the bolt rotated about a vector defined by the initial two contact points until a third contact location was found. By analyzing the depth of intersection of the bolt into the nut as well as the vertical movement of the origin of the bolt reference frame, we determined that there are three types of contacts states present: unstable two-point, quasi-stable two-point, stable three point. Though the unstable case remains to be deciphered, the parametric equations derived in this work can be used without modification to create a full spectrum of maps at any point in the history of a threaded assembly problem. We investigated 81 potential orientations, each of which has its own set of contact points. From this exhaustive examination, we are capable of detailing a contact state history and, from this, have the potential to develop a constraint network. / Master of Science

Thema dieser Arbeit ist die Entwicklung eines Kommunikationsteilsystems fuer das Experimentiersystem CHEOPS zur Ermoeglichung einer Interobjektkommunika- tion zwischen Objekten auf dem gleichen bzw. verschiedenen Systemen. Ausgangspunkte stellen dabei eine verfuegbare Implementation eines Ethernet- Treibers der Kartenfamilie WD80x3 fuer MS-DOS, eine geforderte Kommunikations- moeglichkeit mit UNIX-Prozessen sowie die dort benutzbaren Protokoll-Familien dar. Die Arbeit beschaeftigt sich mit der Analyse und Konzipierung des Ethernet- Treibers sowie der Internet-Protokoll-Familie fuer CHEOPS als auch deren Implementation resultierend in einem minimalen Grundsystem. Weiterhin wird ein erster Entwurf fuer ein spaeter weiterzuentwickelndes bzw. zu vervoll- staendigendes Netz-Interface vorgeschlagen und durch eine Beispiel-Implemen- tierung belegt.

The aim of this study is to offer a new perspective on both interpersonal communication andcomputer-mediated communication (CMC), by means of conducting a pragma-linguisticanalysis and comparison of a semi-threaded discussion forum and a fully threaded discussionforum; analysing features such as linguistic markers, dialogic listening, politeness, cooperation,elaborate or laconic greetings, farewell expressions and other conversational rituals. Aqualitative study was conducted, employing two methods of gathering data: (a) participantobservation and (b) document and material analysis. The major question for discussion in thisstudy is whether there are any differences with respect to linguistic and non-linguistic featuresbetween the semi-threaded and fully threaded forums? The study concludes that there aredifferences in linguistic and non-linguistic features between semi-threaded and fully threadedforums, but these differences are minimal and can more likely be attributed to the forum subjectmatter and social context than to the forum structure itself.

This thesis proposes a new methodology to extend the software performance engineering process. Common performance measurement and tuning principles mainly target to improve the software function itself. Hereby, the application source code is studied and improved independently of the overall system performance behavior. Moreover, the optimization of the software function has to be done without an estimation of the expected optimization gain. This often leads to an under- or overoptimization, and hence, does not utilize the system sufficiently. The proposed performance improvement methodology and framework, called dynamic performance stubs, improves the before mentioned insufficiencies by evaluating the overall system performance improvement. This is achieved by simulating the performance behavior of the original software functionality depending on an adjustable optimization level prior to the real optimization. So, it enables the software performance analyst to determine the systems’ overall performance behavior considering possible outcomes of different improvement approaches. Moreover, by using the dynamic performance stubs methodology, a cost-benefit analysis of different optimizations regarding the performance behavior can be done. The approach of the dynamic performance stubs is to replace the software bottleneck by a stub. This stub combines the simulation of the software functionality with the possibility to adjust the performance behavior depending on one or more different performance aspects of the replaced software function. A general methodology for using dynamic performance stubs as well as several methodologies for simulating different performance aspects is discussed. Finally, several case studies to show the application and usability of the dynamic performance stubs approach are presented.

The goal of this dissertation is to present new and improved techniques for fully automatic verification of sequential and concurrent software libraries. In most cases, automatic software verification is plagued by undecidability, while in many others it suffers from prohibitively high computational complexity. Model checking -- a highly successful technique used for verifying finite state hardware circuits against logical specifications -- has been less widely adapted for software, as software verification tends to involve reasoning about potentially infinite state-spaces. Two of the biggest culprits responsible for making software model checking hard are heap-allocated data structures and concurrency. In the first part of this dissertation, we study the problem of verifying shape properties of sequential data structure libraries. Such libraries are implemented as collections of methods that manipulate the underlying data structure. Examples of such methods include: methods to insert, delete, and update data values of nodes in linked lists, binary trees, and directed acyclic graphs; methods to reverse linked lists; and methods to rotate balanced trees. Well-written methods are accompanied by documentation that specifies the observational behavior of these methods in terms of pre/post-conditions. A pre-condition [phi] for a method M characterizes the state of a data structure before the method acts on it, and the post-condition [psi] characterizes the state of the data structure after the method has terminated. In a certain sense, we can view the method as a function that operates on an input data structure, producing an output data structure. Examples of such pre/post-conditions include shape properties such as acyclicity, sorted-ness, tree-ness, reachability of particular data values, and reachability of pointer values, and data structure-specific properties such as: "no red node has a red child'', and "there is no node with data value 'a' in the data structure''. Moreover, methods are often expected not to violate certain safety properties such as the absence of dangling pointers, absence of null pointer dereferences, and absence of memory leaks. We often assume such specifications as implicit, and say that a method is incorrect if it violates such specifications. We model data structures as directed graphs, and use the two terms interchangeably. Verifying correctness of methods operating on graphs is an instance of the parameterized verification problem: for every input graph that satisfies [phi], we wish to ensure that the corresponding output graph satisfies [psi]. Control structures such as loops and recursion allow an arbitrary method to simulate a Turing Machine. Hence, the parameterized verification problem for arbitrary methods is undecidable. One of the main contributions of this dissertation is in identifying mathematical conditions on a programming language fragment for which parameterized verification is not only decidable, but also efficient from a complexity perspective. The decidable fragment we consider can be broadly sub-divided into two categories: the class of iterative methods, or methods which use loops as a control flow construct to traverse a data structure, and the class of recursive methods, or methods that use recursion to traverse the data structure. We show that for an iterative method operating on a directed graph, if we are guaranteed that if the number of destructive updates that a method performs is bounded (by a constant, i.e., O(1)), and is guaranteed to terminate, then the correctness of the method can be checked in time polynomial in the size of the method and its specifications. Further, we provide a well-defined syntactic fragment for recursive methods operating on tree-like data structures, which assures that any method in this fragment can be verified in time polynomial in the size of the method and its specifications. Our approach draws on the theory of tree automata, and we show that parameterized correctness can be reduced to emptiness of finite-state, nondeterministic tree automata that operate on infinite trees. We then leverage efficient algorithms for checking the emptiness of such tree automata to obtain a tractable verification framework. Our prototype tool demonstrates the low theoretical complexity of our technique by efficiently verifying common methods that operate on data structures. In the second part of the dissertation, we tackle another obstacle for tractable software verification: concurrency. In particular, we explore application of a static analysis technique based on interprocedural dataflow analysis to predict and document deadlocks in concurrent libraries, and analyze deadlocks in clients that use such libraries. The kind of deadlocks that we focus result from circular dependencies in the acquisition of shared resources (such as locks). Well-written applications that use several locks implicitly assume a certain partial order in which locks are acquired by threads. A cycle in the lock acquisition order is an indicator of a possible deadlock within the application. Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in a manner that violates the partial ordering between lock acquisitions that is implicit within the library. Given a concurrent library, we present a technique for inferring interface contracts that speciy permissible concurrent method calls and patterns of aliasing among method arguments that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a satisfiability modulo theories (SMT) solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signalling primitives such as wait-notify for cooperative synchronization. We demonstrate its scalability and efficiency with a prototype tool that analyzed over a million lines of code for some widely-used open-source Java libraries in less than 50 minutes. Furthermore, the contracts inferred by our approach have been able to pinpoint real bugs, i.e. deadlocks that have been reported by users of these libraries. / text

There is no established method of measuring load accurately in a threaded connection at working temperatures exceeding 500°C. At these conditions conventional methods can not be used due to the sensitivity of the instruments and it is suggested that a non contact method should be used. The laser strain gauge was developed by the Loughborough University Optical Research Group and it is a non contact way of measuring surface strain. With the help of finite element analysis (FEA) a special nut was developed that can be used to measure the load on the connection by relating the surface strain of the nut to the load. Experimental work later revealed that due to the threads sticking in the connection there is hysteresis present between the load and surface strain relationship. To eliminate the hysteresis a new part was added to the connection which could be used to relate the surface strain on it to the load without any hysteresis. This new part was a specially designed washer with three grooves to allow easy access for the user to measure the surface strain using the laser strain gauge. Part of the design specification was that the load has to be determined to an accuracy of 0.5%. Using sensitivity analysis the washer was analysed in terms of how manufacturing imperfections affect the accuracy of the load measuring device. The results revealed that to achieve the required 0.5% accuracy the washer would have to be manufactured to very tight tolerances. To achieve these tight tolerances the manufacturing process would not be cost effective so it was proposed that individual calibration is required for each load measuring washer. Tests showed that with sufficient calibration the specially designed washer and the laser strain gauge can be combined and used as an accurate non contact load measuring device. As it is a non contact method it can be used in extreme environments including high temperatures. This thesis describes how background research, finite element analysis and experimental testing were used to develop the load measuring washer. Also it is shown, how in-depth sensitivity analysis was used to determine the accuracy of the prototype and that how manufacturing imperfections influence the working life of a threaded connection.