In this paper we present the design and usage of a debugging framework for the Relational Meta-Language (RML), which is a language for writing executable Natural Semantics specifications. The language is successfully used at our department for writing large specifications for a range of languages like Java, Modelica, Pascal, MiniML etc. The RML system previously had no debugging facilities, which made it hard for programmers to debug their specifications. With this work we address these issues by providing a debugging framework for debugging high level Natural Semantics specifications in RML.
Much of the current discussion around automated debugging systems is centered around various technical issues. In contrast, this paper focuses on user oriented usability criteria for automated debugging systems, and reviews several systems according to these criteria. We introduce four usability criteria: generality, cognitive plausibility, degree of automation and appreciation of the user's expertise. A debugging system which is general is able to understand a program without restrictive assumptions about the class of algorithms, the implementation, etc. A cognitively plausible debugging system supports debugging according to the user's mental model, e.g. by supporting several levels of abstraction and directions of bug localization. A high degree of automation means that fewer interactions with the user are required to find a bug. A debugging system that appreciates the user's expertise is suitable for both expert and novice programmers, and has the ability to take advantage of the additional knowledge of an expert programmer to speed up and improve the debugging process. Existing automated debugging systems fulfill these user-oriented requirements to a varying degree. However, many improvements are still needed to make automated debugging systems attractive to a broad range of users.
This paper illustrates the application of formal specifications to software documentation and debugging by presenting a real-life scenario involving the use of a garbage collection package. It illustrates the advantages of using formal specifications over informal documentation. The paper also illustrates the usefulness of run-time checking tools that compares program behavior with their formal specifications. The scenario presented in this paper goes through a series of steps that include formal specification, run-time checking, and modification of the specification and program based on the results of run-time checking — the typical steps involved in a debugging process, except that this scenario makes use of formal specifications. Although various research ideas presented in this paper have been published earlier, this paper assimilates all these ideas into a real-life scenario, and illustrates in an easy-to-understand way that these ideas are really useful to software documentation and debugging. The example has been developed in Ada, and formally specified using the Anna specification language. The tool used in the example is the Anna Run-Time Consistency Checking System developed at Stanford University.
This paper presents a twofold proposal to understand the Warren Abstract Machine. A stepwise definition of the WAM by using abstract data types (for every WAM component) is briefly presented. Furthermore, we describe a visual environment which can be used for the emulation of the Warren Abstract Machine. It has been designed as a high level debugger for object oriented programs, following a methodology sketched in the paper. The tool has the capability to show the user the internal behaviour of the WAM during a program execution by showing its components at the desired level of abstraction. The tool provides an interactive and friendly interface. Configurable tracing and dynamic breakpoint location can be used in a simple and coherent way. All the features included in the tool allow for an easy and powerful examination of the WAM.
This paper discusses application of the technique of algorithmic debugging, originating from logic programming, to automatic diagnosis of VLSI digital circuits. In particular, the main aim of the presented work is to provide a method for smooth combination of different diagnosis techniques, where the use of logic specifications and algorithmic debugging plays an essential role. Examples of the application of the proposed method to combinational and to sequential circuits are presented.
Software maintenance involves making changes to a program to correct errors, to improve efficiency, or to extend the program functionality. The existing algorithmic debuggers generally only take into account the modified software, i.e., they do not take into account the original software and modifications being made. However, in software maintenance the original software has been tested and analyzed previously. In software maintenance the goal of debugging is to identify those modifications that cause incorrect program behavior, rather than to identify faulty statements. In this paper we present an approach that uses the information about the original software and determines those modifications that more likely contain fault. In this approach, the modifications that are made to the program are first identified. Then, forward dynamic dependence analysis is used to determine the most suspicious modifications.
Modern software engineering uses abstract data types to allow modular programming. When debugging, abstract data types cause problems because the user does not understand the implementation of the type. This is particularly true in declarative debugging where users must determine the validity of an atom. As the user of the type does not know how the type is implemented the user is unable to determine its validity when presented with the implementation. Frequently, the user visualises a structure which the type represents. This view can be used when displaying terms of this type during debugging. We introduce the concept of a representer, which, establishes an equivalence between a term and this view. During debugging, the representers are used to translate terms to and from their view. When inputting abstract data types, the representer will produce the hidden term from the visible term the user gave. When outputting abstract data types, the representer will produce a visible term from the hidden term. We also extend the idea of representers to be able to handle large data efficiently.
Jockey is an execution record/replay tool for debugging Linux programs. It records invocations of system calls and CPU instructions with timing-dependent effects and later replays them deterministically. It supports process checkpointing to diagnose long-running programs efficiently. Jockey is implemented as a shared-object file that runs as a part of the target process. While this design is the key for achieving Jockey's goal of safety and ease of use, it also poses challenges. This paper discusses some of the practical issues we needed to overcome in such environments, including low-overhead system-call interception, techniques for segregating resource usage between Jockey and the target process, and an interface for fine-grain control of Jockey's behavior.
The paper extends the concept of justification to the context of Answer Set Programming---a recent paradigm that builds on the foundations of logic programming, answer set semantics, and non-monotonic reasoning. A justification describes the support for the truth value of each atom in an answer set of a logic program, and it can be employed as a tool for reasoning and debugging of answer set programs. The paper describes the implementation of the notion of justification in the ASP system along with some examples of its applications.
In a C compiler, function calls are difficult to implement correctly because they must respect a platform-specific calling convention. But they are governed by a simple invariant: parameters passed to a function must be received unaltered. A violation of this invariant signals an inconsistency in a compiler. We automatically test the consistency of C compilers using randomly generated programs. An inconsistency manifests itself as an assertion failure when compiling and running the generated code. The generation of programs is type-directed and can be controlled by the user with composable random generators in about 100 lines of Lua. Lua is a scripting language built into our testing tool that drives program generation. Random testing is fully automatic, requires no specification, yet is comparable in effectiveness with specification-based testing from prior work. Using this method, we uncovered 13 new bugs in mature open-source and commercial C compilers.
The capability to debug a program at the source level is useful and often indispensable. Debuggers use sophisticated techniques to provide a source view of a program, even though what is executing on the hardware is machine code. Debugging techniques evolve with significant changes in programming languages and execution environments. Recently, software dynamic translation (SDT) has emerged as a new execution mechanism. SDT inserts a run-time software layer between the program and the host machine, providing flexibility in execution and program monitoring. Increasingly popular technologies that use this mechanism include dynamic optimization, dynamic instrumentation, security checking, binary translation, and host machine virtualization. However, the run-time program modifications in a SDT environment pose significant challenges to a source level debugger. Currently debugging techniques do not exist for software dynamic translators. This thesis is the first to provide techniques for source level debugging of dynamically translated programs. The thesis proposes a novel debugging framework, called Tdb, that addresses the difficult challenge of maintaining and providing source level information for programs whose binary code changes as the program executes. The proposed framework has a number of important features. First, it does not require or induce changes in the program being debugged. In other words, programs are debugged is their deployment environment. Second, the framework is portable and can be applied to virtually any SDT system. The framework requires minimal changes to an SDT implementation, usually just a few lines of code. Third, the framework can be integrated with existing debuggers, such as Gdb, and does not require changes to these debuggers. This improves usability and adoption, eliminating the learning curve associated with a new debugging environment. Finally, the proposed techniques are efficient. The runtime overhead of the debugged programs is low and comparable to that of existing debuggers. Tdb's techniques have been implemented for three different dynamic translators, on two different hardware platforms. The experimental results demonstrate that source level debugging of dynamically translated programs is feasible, and our implemented systems are portable, usable, and efficient.
Dynamic slicing algorithms have been considered to aid in debugging for many years. However, as far as we know, no detailed studies on evaluating the benefits of using dynamic slicing for detecting faulty statements in programs have been carried out. We have developed a dynamic slicing framework that uses dynamic instrumentation to efficiently collect dynamic slices and reduced ordered Binary Decision Diagrams (roBDDs) to compactly store them. We have used the above framework to implement three variants of dynamic slicing algorithms including: data slicing, full slicing, and relevant slicing algorithms. We have carried out detailed experiments to evaluate these algorithms. Our results show that full slices and relevant slices can considerably reduce the subset of program statements that need to be examined to locate faulty statements. We expect that the observations presented here will enable development of new slicing based algorithms for automated debugging.
AMPLE locates likely failure-causing classes by comparing method call sequences of passing and failing runs. A difference in method call sequences, such as multiple deallocation of the same resource, is likely to point to the erroneous class. Such sequences can be collected from arbitrary Java programs at low cost; comparing object-specific sequences predicts defects better than simply comparing coverage. AMPLE comes as a plug-in for the Java IDE Eclipse that is automatically invoked as soon as a JUnit test fails.
We have implemented a declarative debugger for Mercury that is capable of finding bugs in large, long-running programs. This debugger implements several search strategies. We discuss the implementation of two of these strategies and the conditions under which each strategy is useful.The divide and query strategy tries to minimize the number of questions asked of the user. While divide and query can reduce the number of questions to roughly logarithmic in the size of the computation, implementing it presents practical difficulties for computations whose representations do not fit into memory. We discuss how we get around this problem, making divide and query practical.Our declarative debugger allows users to specify exactly which part of an atom is wrong. The subterm dependency tracking strategy exploits this extra information to jump directly to the part of the program that computed the wrong subterm. In many cases, only a few such jumps are required to arrive at the bug. Subterm dependency tracking can converge on the bug even more quickly than divide and query, and it tends to yield question sequences that are easier for users to answer.
We all understand that software defects are a problem, and we want to make it easy to build more reliable software. But finding bugs is embarrassingly easy, as is devising a new program analysis technique that is able to find some bugs. Actually improving software quality through bug detection or bug localization tools is hard, and requires careful thinking about what really impacts software reliability and how your tool can fit into the entire software development process. I'll discuss some observations and attempts to address these issues from the perspective of the FindBugs project.
Code coverage analysis, the process of finding code exercised by a particular set of test inputs, is an important component of software development and verification. Most traditional methods of implementing code coverage analysis tools are based on program instrumentation. These methods typically incur high overhead due to the insertion and execution of instrumentation code, and are not deployable in many software environments. Hardware-based sampling techniques attempt to lower overhead by leveraging existing Hardware Performance Monitoring (HPM) support for program counter (PC) sampling. While PC-sampling incurs lower levels of overhead, it does not provide complete coverage information. This paper extends the HPM approach in two ways. First, it utilizes the sampling of branch vectors which are supported on modern processors. Second, compiler analysis is performed on branch vectors to extend the amount of code coverage information derived from each sample. This paper shows that although HPM is generally used to guide performance improvement efforts, there is substantial promise in leveraging the HPM information for code debugging and verification. The combination of sampled branch vectors and compiler analysis can be used to attain upwards of 80% of the actual code coverage.
One of today's challenges is producing reliable software in the face of an increasing number of interacting components. Our system CHET lets developers define specifications describing how a component should be used and checks these specifications in real Java systems. Unlike previous systems, CHET is able to check a wide range of complex conditions in large software systems without programmer intervention. This paper explores the specification techniques that are used in CHET and how they are able handle the types of specifications needed to accurately model and automatically identify component checks.
We present a trace based approach for analyzing the runs of Inductive Logic Programming Data Mining systems, without needing to modify the actual implementation of the ILP mining algorithms. We discuss the use of traces as the basis for easy and fast, semi-automated debugging of the underlying (query) execution engine of the ILP system. Our approach also provides a way to monitor the behavior of queries generated by the ILP algorithm, allowing an evaluation and comparison of the impact of different execution mechanisms. The traces can be extended further, and as such be useful for visualization and monitoring of other aspects of ILP data mining systems.
In this article we address the fault localization problem in HDLs, particularly in VHDL designs. Our approach relies on the model-based diagnosis paradigm and, unlike to other approaches that rely on the design's gate-level representation, we accurately represent the program's syntax and semantics in a debugging model. This detailed modeling approach, however, may cause scalability problems for larger designs, thus reducing the model's complexity and size is a crucial issue. Creating a debugging model specifically for a given test case in terms of its execution trace is, although tractable in terms of the model's size, uneligible for source level debugging. We illustrate this result by a simple example and relate it to similar findings in the area of program slicing. Moreover, we present a solution to this problem and discuss implications on software debugging by means of our recent empirical results.
