Replay and testing for concurrent programs

Attention is given to the problems that arise during the testing and debugging cycle of concurrent programs because of their nondeterministic execution behavior, whereby multiple executions of a concurrent program with the same input may exercise different synchronization sequences and even produce different results. These problems are solved by using deterministic execution debugging and testing. The purpose of deterministic execution debugging to to replay executions of a concurrent program so that debugging information can be collected. Examples of semaphores and monitors are used to illustrate the approach and the process of designing replay tubes is described. The use of regression testing to see if earlier debugging and testing introduced new errors, is examined     

Reasoning about plan revision in BDI agent programs

Facilities for handling plan execution failures are essential for agents which must cope with the effects of nondeterministic actions, and some form of failure handling can be found in most mature agent programming languages and platforms. While such features simplify the development of more robust agents, they make it hard to reason about the execution of agent programs, e.g., to verify their correctness. In this paper, we present an approach to the verification of agent programs which admit exceptional executions. We consider executions of the BDI-based agent programming language 3APL in which plans containing non-executable actions can be revised using plan revision rules, and present a logic for reasoning about normal and exceptional executions of 3APL programs. We provide a complete axiomatization for the logic and, using a simple example, show how to express properties of 3APL programs as formulas of the logic.     

A formal semantics for debugging synchronous message passing-based concurrent programs

In this paper, we propose a semantic framework to debug synchronous message passing-based con- current programs, which are increasingly useful as parallel computing and distributed systems become more and more pervasive. We first design a concurrent programming language model to uniformly represent exist- ing concurrent programming languages. Compared to sequential programming languages, this model contains communication statements, i.e., sending and receiving statements, and a concurrent structure to represent com- munication and concurrency. We then propose a debugging process consisting of a tracing and a locating procedure. The tracing procedure re-executes a program with a failed test case and uses specially designed data structures to collect useful execution information for locating bugs. We provide for the tracing procedure a struc- tural operational semantics to represent synchronous communication and concurrency. The locating procedure backward locates the ill-designed statement by using information obtained in the tracing procedure, generates a fix equation, and tries to fix the bug by solving the fix equation. We also propose a structural operational semantics for the locating procedure. We supply two examples to test our proposed operational semantics.     

Using SPIN for automated debugging of infinite executions of Java programs

This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking and runtime monitoring. Runtime monitoring is used to transform the Java execution traces into the input for the model checker, the purpose of which is twofold. First, it checks these execution traces against properties written in linear temporal logic (LTL), which represent desirable or undesirable behaviors. Second, it produces several execution traces for a single Java program by generating test inputs and exploring different schedulings in multithreaded programs. As state explosion is the main drawback to model checking, we propose two abstraction approaches to reduce the memory requirements when storing Java states. We also present the formal framework to clarify which kinds of LTL safety and liveness formulas can be correctly analysed with each abstraction for both finite and infinite program executions. A major advantage of our approach comes from the model checker, which stores the trace of each failed execution, allowing the programmer to replay these executions to locate the bugs. Our current implementation, the tool TJT, uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as an Eclipse plug-in and it has been successfully applied to debug complex public Java programs.     

A new external reference management and distributed unification for KL1

This paper describes a new external reference management scheme for KL1, a committed choice logic programming language based on GHC. The significance of the new scheme is that it realizes incremental inter-processor garbage collection. Previous distributed implementations of committed choice languages had not seriously addressed inter-processor garbage collection. Incremental inter-precessor garbage collection is realized by the Weighted Export Counting (WEC). It is a first attempt to use the weighted reference counting technique in logic programming language implementation, and is also new in that it has introduced export and import tables for making independent local garbage collection possible and reducing the number of inter-processor read requests. The problems with exhaustion of reference counts and indirect exportation are discussed. Since the binding order rule adopted in our previous implementation for avoiding creation of reference loops is insufficient in the presence of indirect exportation, a new binding order rule is introduced. We prove that avoidance of reference loops is guaranteed and also prove that the unification procedure always terminates for non-circular structures.     

Designing a source-level debugger for cognitive agent programs

When an agent program exhibits unexpected behaviour, a developer needs to locate the fault by debugging the agent’s source code. The process of fault localisation requires an understanding of how code relates to the observed agent behaviour. The main aim of this paper is to design a source-level debugger that supports single-step execution of a cognitive agent program. Cognitive agents execute a decision cycle in which they process events and derive a choice of action from their beliefs and goals. Current state-of-the-art debuggers for agent programs provide insight in how agent behaviour originates from this cycle but less so in how it relates to the program code. As relating source code to generated behaviour is an important part of the debugging task, arguably, a developer also needs to be able to suspend an agent program on code locations. We propose a design approach for single-step execution of agent programs that supports both code-based as well as cycle-based suspension of an agent program. This approach results in a concrete stepping diagram ready for implementation and is illustrated by a diagram for both the Goal and Jason agent programming languages, and a corresponding full implementation of a source-level debugger for Goal in the Eclipse development environment. The evaluation that was performed based on this implementation shows that agent programmers prefer a source-level debugger over a purely cycle-based debugger.     

并发环境中渐增式追踪重演机制

在基于消息传递的并发程序中,由于进程的调度顺序以及消息延时等特性,使得同样输入的不同执行呈现不同的结果,这种并发程序行为的不确定性直接导致了程序错误的不可再现性,即后续的执行无法再现前次执行的错误。以反复执行程序、重复再现故障为核心的循环调试方法变得不再可用。因此,对于并发程序的调试问题,我们将传统的循环调试方法加以扩充,引入追踪和重演的机制,重放程序的某次执行,以消除并发程序的错误不可再现性。     

Data structures for order-sensitive predicates in parallel nondeterministic systems

We study the problem of guaranteeing correct execution semantics in parallel implementations of logic programming languages in presence of built-in constructs that are sensitive to order of execution. The declarative semantics of logic programming languages permit execution of various goals in any arbitrary order (including in parallel). However, goals corresponding to extra-logical built-in constructs should respect the sequential order of execution to ensure correct semantics. Ensuring this correctness in presence of such built-in constructs, while efficiently exploiting maximum parallelism, is a difficult problem. In this paper, we propose a formalization of this problem in terms of operations on dynamic trees. This abstraction enables us to: (i) show that existing schemes to handle order-sensitive computations used in current parallel systems are sub-optimal; (ii) develop a novel, optimal scheme to handle order-sensitive goals that requires only a constant time overhead per operation. While we present our results in the context of logic programming, they will apply equally well to most parallel non-deterministic systems. Received: 20 April 1998 / 3 April 2000     

自适应推导下的统一化调试加速技术

在传统调试过程中,缺陷定位通常作为程序修复的前置步骤.最近,一种新型调试框架(统一化调试)被提出.不同于传统调试中缺陷定位和程序修复的单向连接方式,统一化调试首次建立了定位与修复之间的双向连接机制,从而达到同时提升两个领域的效果.作为首个统一化调试技术,ProFL利用程序修复过程中伴随产生的大量补丁执行信息逆向地提升已...     

Determining possible event orders by analyzing sequential traces

One of the fundamental problems encountered when debugging a parallel program is determining the possible orders in which events could have occurred. Various problems, such as data races and intermittent deadlock, arise when there is insufficient synchronization between the tasks in a parallel program. A sequential trace of an execution can be misleading, as it implies additional event orderings, distorting the concurrent nature of the computation. Algorithms to generate, from the trace of an execution, those event orderings that can be relied on by the programmer are described. By its very nature, the information in an execution trace pertains only to that execution of the program, and may not generalize to other executions. This difficulty is mitigated by defining an inferred program based on the trace and original program, analyzing this inferred program, and showing how the inferred program relates to the original. The results of the algorithms can be used by other automated tools such as a data race detector or constraint checker     

Extracting safe thread schedules from incomplete model checking results

Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort toward verifying the program is wasted. We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach—somewhat surprisingly—even leads to faster executions.

     

Guard: A Relative Debugger

A significant amount of software development is evolutionary, involving the modification of already existing programs. To a large extent, the modified programs produce the same results as the original program. This similarity between the original program and the development program is utilized by relative debugging. Relative debugging is a new concept that enables the user to compare the execution of two programs by specifying the expected correspondences between their states. A relative debugger concurrently executes the programs, verifies the correspondences, and reports any differences found. We describe our novel debugger, called Guard, and its relative debugging capabilities. Guard is implemented by using our library of debugging routines, called Dynascope, which provides debugging primitives in heterogeneous networked environments. To demonstrate the capacity of Guard for debugging in heterogeneous environments, we describe an experiment in which the execution of two programs is compared across Internet. The programs are written in different programming languages and executing on different computing platforms. © 1997 by John Wiley & Sons, Ltd.     

A lingua franca for concurrent logic programming

Two of the more important concurrent logic programming languages with nonflat guards are GHC and Parlog. They balance the requirements of having clean semantics and providing good control facilities rather differently, and their respective merits are compared and contrasted. Since concurrent logic programming would benefit from both, but neither language is able to express all the programs expressible in the other language, a lingua franca of these languages is defined and justified. A method is given for translating GHC and Parlog to and from it. The method preserves the arities and execution conditions of each clause. It enables a lingua franca implementation to support both languages transparently, and to provide a simple concurrent logic programming language suitable for programming in its own right     

Memory requirements for parallel programs

Parallel execution is normally used to decrease the amount of time required to run a program. However, the parallel execution may require far more space than that required by the sequential execution. Worse yet, the parallel space requirement may be very much more difficult to predict than the sequential space requirement because there are more factors to consider. These include essentially nondeterministic factors that can influence scheduling, which in turn may dramatically influence space requirements. We survey some scheduling algorithms that attempt to place bounds on the amount of time and space used during parallel execution. We also outline a direction for future research. This direction takes us into the area of functional programming, where the declarative nature of the languages can help the programmer to produce correct parallel programs, a feat that can be difficult with procedural languages. Currently the high-level nature of functional languages can make it difficult for the programmer to understand the operational behavior of the program. We look at some of the problems in this area, with the goal of achieving a programming environment that supports correct, efficient parallel programs.     

基于确定性重演的并发程序调试

并发程序执行的不确定性导致了程序错误的不可再现性,后续的执行无法再现前次执行的错误,这使得以反复执行程序,重复再现故障为核心的循环调试方法变得不再可用。本文提出了一种基于确定性重演的并发程序的调试方法,确定化并发程序的执行轨迹,重现程序初始运行的错误状态。     

High-Level Views of Distributed Executions: Convex Abstract Events

Due to the complexity of distributed applications, understanding their behaviour is a challenging task. To remedy this problem, graphical visualizations of distributed executions in the form of process-time diagrams are frequently employed. However, such process-time diagrams do not scale for long-running and complex distributed applications. To reduce the display complexity, abstract graphical views of an execution are frequently suggested. One commonly used abstraction is to group primitive events into abstract events. This paper discusses some of the problems encountered when analyzing executions at abstract levels and introduces the concept of convex abstract events. Such abstract events can be used to reason about executions at higher levels, facilitating program development, debugging, and maintenance. We discuss some fundamental aspects, such as the precedence relation and its efficient detection, for abstract events. The paper also presents a graphical representation for convex abstract events which can easily be included in process-time diagrams. Poet, our visualization tool, was enhanced with a facility to display abstract events. Using a non-trivial distributed application, examples of the resulting abstract execution visualizations are discussed.     

基于逐步细化快照序列的多核并行程序调试

多核并行程序的调试是一个公认的困难问题,困难主要来自于程序执行的不确定性.可重现调试(replay debug)提供了消除程序中不确定性的能力,但是现有的可重现调试解决方案都无法应用于商用的软硬件平台中,且进行调试所带来的性能损失会随着并发度的增加而超线性地增长.提出了一种基于运行快照的新型并行程序调试方法SDT(snapshot debug tool).该方法以离线的断点设置、运行快照捕捉和运行快照细化为基础,提出了一套可以指导用户由粗到细发现错误的调试过程,并在通用的软硬件平台上进行了实现.实验结果显示,在8线程的并发条件下,使用SDT调试所带来的时间性能损耗平均为5188%;同时当线程数增长4倍时,使用SDT所带来的额外时间消耗最多增长1倍,具有很好的可扩展性.记录快照的数据量是影响SDT性能的重要挑战,实验证明通过使用增量式的快照记录方式可以有效地降低需要记录的数据量,减少记录快照花费的时间,提高SDT的整体性能.     

Reproducible execution of SR programs

Reproducing the execution of a concurrent program is important in debugging and testing. It requires that, regardless of the actual order in which processes may execute, the reproduced execution is identical, with respect to the order in which certain activities occur, to a previously recorded execution. This paper presents a solution to the reproducibility problem for programs written in the SR concurrent programming language. Our solution transforms an arbitrary SR program into one for recording an event sequence and one for replaying from an event sequence. SR provides a rich collection of synchronization mechanisms, including rendezvous, asynchronous message passing, remote procedure call, and dynamic process creation. SR language features allow: flexible invocation servicing (e.g. use of invocation parameters in selecting an invocation to service in message passing or rendezvous); dynamically created processes and resource (module) instances; dynamic communication paths between processes; and dynamic distribution of programs across multiple machines. Because of these features, adaptations of previous solutions to the reproducibility problem for other languages and notations do not work for SR. Our solution handles all the above features. It results in a naturally distributed control algorithm for programs that are distributed. This paper also describes the implementations of our transformation tools. Copyright © 1999 John Wiley & Sons, Ltd.