Abstracts

Debugging in the Context of Charm++ (Abstract) R. Jyothi, O. S. Lawlor and L. V. Kale This paper describes a parallel debugger and the related debugging support implemented for CHARM++, a data-driven parallel programming language. Because we build extensive debugging support into the parallel runtime system, applications can be debugged at a very high level. "Towards the Proper "Step" Command in Parallel Debuggers" (Abstract) A. Kalinov, K. Karganov and K. Khorenko The article is devoted to the concept of the stepping commands in parallel debuggers. It reviews the main existing schemes (synchronous and asynchronous step implementations) and introduces a new kind of synchronous scheme that has several advantages over existing ones. In this scheme the debugger performs the dynamic analysis of the program state thus simplifying the program state presentation and control. The possible implementation of suggested scheme in MPI debuggers is discussed and the existing implementation in mpC Workshop parallel debugger is presented. Program Monitoring with LTL in EAGLE (Abstract) H. Barringer, A. Goldberg, K. Havelund and Koushik Sen We briefly present a rule-based framework, called EAGLE, shown to be capable of defining and implementing finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time and metric temporal logics (MTL), interval logics, forms of quantified temporal logics, and so on. In this paper we focus on a linear temporal logic (LTL) specialisation of EAGLE. For an initial formula of size m , we establish upper bounds of O(m22–logm) and O(m422–log2m) for the space and time complexity, respectively, of single step evaluation over an input trace. EAGLE has been successfully used, in both LTL and metric LTL forms, to test a real-time controller of an experimental NASA planetary rover. Concurrent and Distributed Desk Checking (Abstract) A. Hayardeny, S. Fienblit and E. Farchi Desk checking is known to be an effective reading technique for early detection of sequential program errors. This paper discusses how to extend desk checking for concurrent and distributed programs. In addition to unbounded possible schedules, concurrent and distributed programs have execution states that include more than one process. The new concurrent and distributed desk checking technique supports the selection of schedules and execution states to be reviewed. The cross-product technique assists in the selection process. Schedule selection guidelines that facilitate early detection and coverage are introduced. Industrial pilots show that concurrent and distributed desk checking is a promising review technique for early error detection. Mutation-Based Exploration of a Method for Verifying Concurrent Java Components (Abstract) B. Long, R. Duke, D. Goldson, P. Strooper and L. Wildman The Java programming language supports concurrency. Concurrent programs are harder to verify than their sequential counterparts due to their inherent non-determinism and a number of specific concurrency problems such as interference and deadlock. In previous work, we proposed a method for verifying concurrent Java components based on a mix of code inspection, static analysis tools, and the ConAn testing tool. The method was derived from an analysis of concurrency failures in Java components, but was not applied in practice. In this paper, we explore the method by applying it to an implementation of the well-known readers-writers problem and a number of mutants of that implementation. We only apply it to a single, well-known example, and so we do not attempt to draw any general conclusions about the applicability or effectiveness of the method. However, the exploration does point out several strengths and weaknesses in the method, which will enable us to fine-tune the method before we carry out a more formal evaluation on other, more realistic components. Compiling a Benchmark of Documented Multi-threaded Bugs (Abstract) Y. Eytani and S. Ur Testing multi-threaded, concurrent, or distributed programs is acknowledged to be a very difficult task. We decided to create a benchmark of programs containing documented multi-threaded bugs that can be used in the development of testing tool for the domain. In order to augment the benchmark with a sizable number of programs, we assigned students in a software testing class to write buggy multi-threaded Java programs and document the bugs. This paper documents this experiment. We explain the task that was given to the students, go over the bugs that they put into the programs both intentionally and unintentionally, and show our findings. We believe this part of the benchmark shows typical programming practices, including bugs, of novice programmers. In grading the assignments, we used our technologies to look for undocumented bugs. In addition to finding many undocumented bugs, which was not surprising given that writing correct multi-threaded code is difficult, we also found a number of bugs in our tools. We think this is a good indication of the expected utility of the benchmark for multi-threaded testing tool creators. Keynote: Atomizer - A Dynamic Atomicity Checker For Multithreaded Programs (Abstract) C. Flanagan Multithreaded programs are prone to unexpected interference between concurrent threads. "Atomic" methods are immune to such interference, and their execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies (formal and informal) correctness arguments. This talk presents a dynamic analysis for detecting atomicity violations. This analysis combines ideas from both Lipton's theory of reduction and earlier dynamic race detectors. Experience with a prototype checker for multithreaded Java programs demonstrates that this approach is effective for detecting errors due to unintended interference between threads. In particular, our checker detects errors that would be missed by standard race detectors. Our experimental results also indicate that the majority of methods in our benchmarks are atomic, supporting our hypothesis that atomicity is a standard methodology in multithreaded programming. Fidgeting Till the Point of No Return (Abstract) M. Biberstein, E. Farchi and S. Ur In previous work, we introduced the alternative pasts algorithm that delays the assignment of values to variables until their usage. Whenever a variable is used, the algorithm chooses one of its past values that is consistent with some possible execution. The alternative pasts algorithm can be seen as belonging to a class of algorithms that shadow the execution and may choose at any point to modify the values of some of the variables. We build on this work and extend it in two directions. First we show a more powerful shadowing algorithm that can delay not only writes but also reads and other kinds of instructions, at most until a relevant control decision is taken, which is the longest possible delay for algorithms of this class. We prove that this algorithm inherits the ability of the alternative pasts algorithm to generate significantly different interleavings, which are guaranteed to execute differently. In addition, we show a new use for the two algorithms, namely alternative replay. Unlike regular replay, where the exe-cution of the program is reproduced, alternative replay is an execution that did not happen before but could have happened. For example, if a bug did not materialize, alternative replay can be used to show the user alternative execution in which the impact of the bug can be observed. Automatic Simulation of Network Problems in UDP-based Java Programs (Abstract) E. Farchi, Y. Nir and Y. Krasny This paper describes a tool for black-box testing of UDP-based distributed Java programs. UDP provides little guarantee for correct delivery of data, and therefore requires the application to verify the integrity of communication according to its needs. Debugging such application is hard, since it is hard to create at will bad network conditions. The tool describes here creates an intermediary layer above the Java API which simulates network noises. It therefore enables stress-testing the application even on a flawless network environment. We describe a field experience of testing an application, using the tool vs. using specially-written testing code. We show the two approaches to be complementary. Visual Formal Specification Using (N)TLCharts: Statechart Automata with Temporal Logic and Natural Language Conditioned Transitions (Abstract) D. Drusinsky This paper describes TLCharts, a visual specification language that combines the visual and intuitive appeal of non-deterministic Harel Statecharts with formal specifications written in Linear-time (Metric) Temporal Logic (LTL and MTL). The formalism is described using a practical infusion pump requirement example. The infusion pump TLChart specification is then compared with two competing representations: temporal logic and deterministic Harel statecharts. The infusion pump example will also be used to point out the strength of each constituent TLCharts component. We provide an informal semantics for TLCharts using non-deterministic automata with negation and overlapping states. Finally, we show how natural language snippets are used instead of TLChart temporal logic conditions thereby inducing a formalism we call NTLCharts. An Instrumentation Technique for Online Analysis of Multithreaded Programs (Abstract) G. Rosu and K. Sen A formal analysis technique aiming at finding safety errors in multithreaded systems at runtime is investigated. An au-tomatic code instrumentation procedure based on multithreaded vector clocks for generating the causal partial order on relevant state update events from a running multithreaded program is first presented. Then, by means of several examples, it is shown how this technique can be used in a formal testing environment, not only to detect, but especially to predict safety errors in multithreaded programs. The prediction process consists of rigorously analyzing other potential executions that are consistent with the causal partial order: some of these can be erroneous despite the fact that the particular observed execution is successful. The proposed technique has been implemented as part of a Java program analysis tool. A bytecode instrumentation package is used, so the Java source code of the tested programs is not necessary.