Debugging nondeterministic parallel programs is a difficult and tedious task. In this project we propose to investigate the use of program specifications, which can serve as enhanced debugging aids in existing parallel debugging tools. The principal idea is to formulate a specification of expected program behavior, translate this specification into runtime assertions, and check them during execution. With this sophisticated approach, the user may select a subset of all possible executions on which checking should be performed and collect for each check a consistent global state of the observed application.
Testing and debugging are two important activities of the software lifecycle, which try to improve the quality of software by addressing two important quality criteria - correctness and reliability. The correctness of a program is always expressed relative to its specification, while software reliability defines the probability of future satisfactory operation [12].
Describing the behavior of sequential programs can be performed with classical logic by a predicate (the output condition) that must hold after the execution of the program. Furthermore, the output condition can be translated (by the technique of weakest preconditions) into conditions that must hold at every step of the program. Such a condition can thus be considered as an assertion that must hold at a particular program step; if we restrict our attention to a particular subclass of formulas, such an assertion can be checked at runtime. Annotating a program by runtime assertions is a simple but very effective way of increasing the code's reliability and thus the user's confidence in a program's correct behavior. While the fact that a particular assertion holds does not prove correctness of a program, the fact that it fails exhibits an error in (at least the understanding of) it.
For parallel programs, an adequate framework for specifying program behavior is provided by temporal logic, which allows to describe the dynamic behavior of a system (program) consisting of multiple asynchronously executing components (processes) [4]. Therefore, a temporal logic formula can be considered as the specification of a concurrent program. An implementation of the program is thus correct if every possible program execution satisfies the formula [5] [6] [7]. This area of formal models is one of the main points of expertise at RISC-Linz [1].
In concurrent programs, however an assertion should not only be checked in one program path but in many of the possible program paths. Especially nondeterministic programs may yield different results in successive program executions, even if the same input data are provided. In fact, in the general case there will be too many paths to check the assertion in all the possible execution paths. Thus, it is not sufficient to execute the program a number of times, but instead we need a way to control the behavior of a nondeterministic program in order to select those paths that should be investigated. Furthermore, if the program state is physically distributed, we need a global snapshot of the partial states on which to perform the assertion check.
Corresponding to the importance of program debugging for the program's correctness and reliability, many on-going research projects are developing tools to support users in this area [14]. Two contrary approaches are taken by MTA-SZTAKI and GUP Linz, which have both developed tools for the development of parallel message-passing programs including debuggers which allow to monitor the states of arbitrary parallel nondeterministic programs.
The P-GRADE environment [8] developed by MTA-SZTAKI is a visual programming environment that includes the distributed debugger DIWIDE [2]. In debugging mode, DIWIDE controls the execution of the target program by providing commands to create breakpoints, step-by-step execution, animation, etc. In trace mode, DIWIDE generates a trace file containing all the trace events defined by the user for later semi-online-visualization. More recently, as a third mode, macrostepping has been added as a new method for searching bugs coming from nondeterministic behavior which gives the possibility to test all branches of the application in a concurrent manner [9]. This means that all possible timing conditions can be tested with the help of macrostep debugging in DIWIDE by controlling the channel or port selection at every alternative input block. DIWIDE is able to force any process to receive the message from the selected port or process when it reached an alternative input (CAIALT) communication block. It is achieved by stopping every process at the next communication point and scanning the possible communicating process pairs. Each communicating process pair will continue its execution at the next macrostep and at CAIALT communication the user can choose the sender process.
A contrary approach is taken by GUP Linz, who developed the record&replay tool NOPE (NOndeterministic Program Evaluator) for testing and debugging of nondeterministic message passing programs within the MAD environment [10]. The operation of NOPE is divided into a record phase and a replay phase [13]. The initial record phase is used to generate partial traces containing only ordering information of critical events. During replay these trace data are used to enforce the same event ordering as occurred during record, which guarantees equivalent execution. Additionally, complete traces can be generated to serve as input for the corresponding post-mortem analysis tool [11]. In order to avoid the probe effect of monitoring program execution, the monitor instruments only receive statements and produces trace records only for wild card receive events (non-deterministic choice points). These data are sufficient to produce complete traces with exhaustive information about the execution during subsequent replay phases. Furthermore, the automatic race condition detection and manipulation mechanism of NOPE allows to evaluate other possible program runs for the supplied input. It searches the complete traces for all occurrences of wild card receives and evaluates race candidates. These are messages that are possibly accepted at a specific wild card receive. Then additional replay steps can be initiated to uncover previously hidden executions. The idea is that at each wild card receive every race candidate arrives first during one execution. NOPE automatically changes the ordering with event manipulation and starts a reply phase for each permutation. The follow-up replays deliver all possible executing that are directly connected to the original program run. The evaluation of message race candidates has to be repeated iteratively, in order to detect indirectly connected executions as well.
Both tools therefore address the same problem by different techniques. In DIWIDE, the user may interactively control the investigation of program paths by providing a selection strategy (e.g. depth-first) or by manual choice. In NOPE, a particular run of an instrumented program is recorded from which afterwards related program runs can be automatically generated.
The goal of this project is to generate from a temporal logic specification of a distributed program runtime assertions that can be used by the MTA-SZTAKI DIWIDE and the GUP Linz NOPE to check the correctness of particular sets of program runs. This requires
This project thus applies the idea of model checking temporal logic specifications to the area of parallel and distributed debugging, something that has to our knowledge not been investigated before. Therefore, this cooperation between RISC-Linz, GUP Linz, and MTZ-SZTAKI, offers a unique opportunity for each of the participants in this project with their complementary approaches and the corresponding fields of expertise.
The first task of this project is performed by RISC-Linz under the supervision of Dr. Schreiner with the help of a Ph.D. student (Gabor Kusper); the second and the third part are performed by MTZ-SZTAKI under the supervision of Prof. Kacsuk and by GUP-Linz under the supervision of Prof. Volkert for their respective tools. Consequently, a tight collaboration and information exchange is required.
In every year of the project,
The main results of the project are the two enhanced debugger tools providing a novel testing and debugging technology for developers of parallel and distributed programs. P-GRADE and MAD are applied in several international universities and research institutions and thus, its novel development and testing techniques can spread quickly among the new generation of software developers.
We expect to jointly publish a number of refereed publications at scientific conferences and in journals, as well as technical reports describing our experiences during this project.
In addition, we will stimulate further integration of this research project with the teaching at each participating institution, and we will foster future cooperation with a series of seminars. It will also be considered to integrate invited lectures of MTA-SZTAKI in the project-oriented subjects included in the Computer Science curriculum at Johannes Kepler University Linz.
As another perspective of this project, we will organize and prepare a proposal for a successor project submitted to national or international funding organizations (FWF, European Union, ...).