Debugging | EPFL Graph Search

In computer programming and software development, debugging is the process of finding and resolving bugs (defects or problems that prevent correct operation) within computer programs, software, or systems. Debugging tactics can involve interactive debugging, control flow analysis, unit testing, integration testing, , monitoring at the application or system level, memory dumps, and profiling. Many programming languages and software development tools also offer programs to aid in debugging, known as debuggers. Etymology The terms "bug" and "debugging" are popularly attributed to Admiral Grace Hopper in the 1940s. While she was working on a Mark II computer at Harvard University, her associates discovered a moth stuck in a relay and thereby impeding operation, whereupon she remarked that they were "debugging" the system. However, the term "bug", in the sense of "technical error", dates back at least to 1878 and Thomas Edison who describes the "little faults and difficultie

Computer Algebraic Approach to Verification and Debugging of Galois Field Multipliers

Maciej Jerzy Ciesielski, Cunxi Yu

The paper presents a novel method to verify and debug gate-level arithmetic circuits implemented in Galois Field arithmetic. The method is based on forward reduction of the specification polynomials of the circuit in GF(2(m)) using GF(2) models of its logic gates. We define a forward variable order "FO >" and the rules of forward reduction that enable verification, bug detection, and automatic bug correction in the circuit. By analyzing the remainder generated by forward reduction, the method can determine whether the circuit is buggy, and finds the location and the type of the bug. The experiments performed on Mastrovito and Montgomery multipliers show that our debugging method is independent of the location of the bug(s) and the debugging time is comparable to the time needed to verify the bug-free circuit.

IEEE2018

Decrypting Local Type Inference

Hubert Plociniczak

Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages can reconstruct a termâs type using type inference algorithms. While helpful, programmers often find it hard to comprehend the choice of typing decisions that led to the derived type for a term. A particularly serious consequence is that the reporting of type errors yields cryptic messages and misleading program locations. In this thesis we propose a novel approach to explaining type checking decisions by exploring fragments of type derivation trees. Our approach applies to programming languages that use local type inference: typing decisions are made locally and the type information is only propagated between the adjacent AST nodes. We design an algorithm that backtracks through the nodes of type derivation trees in order to discover the typing decisions that introduce the types for the first time during the type inference process. Our algorithm has two properties: - it is type-driven, meaning that we only visit the nodes and their respective typing decisions if they participated in the inference of a type. - it is autonomous, meaning that it does not require any user-input in its operation. These properties allow us to identify the complete and precise set of locations defining the source of a type; previous work mostly focussed on heuristics or used approximations for locating the cause of an error. Our algorithm is not tied to a particular implementation of a type checker: our type derivation trees can be reconstructed from a pre-existing type checker without modifying its internal logic or affecting its regular compilation times. It therefore readily applies to existing programs: we can not only provide improved feedback for them, we also expose limitations of local type inference algorithms and their implementations, without artificially limiting the language features. We implement our type debugging algorithm on top of Scalaâs type checker. Our analysis applies to a range of erroneous scenarios. It provides better error locations than the standard type error reporter of the Scala compiler. This type debugging analysis is just a starting point from which many interesting and useful applications around type debugging can be built: - we implement an interactive type debugger that guides the users through the decisions of local type inference for erroneous and error-free programs alike. - with precise and minimal source code locations we can also offer surgical-level code modifications that fix for example the limitations of local type inference. - we open the door for programmatically defined, application-specific error feedback or corrections. To the best of our knowledge this thesis is the first to address the problem of type errors for programming languages that use local type inference. Current trends suggest that this scheme is gaining in popularity with mainstream languages other than Scala.

EPFL2016

Opis: Reliable Distributed Systems in OCaml

Pierre-Evariste Dagand, Dejan Kostic, Viktor Kuncak

Concurrency and distribution pose algorithmic and implementation challenges in developing reliable distributed systems, making the field an excellent testbed for evaluating programming language and verification paradigms. Several specialized domain-specific languages and extensions of memory-unsafe languages were proposed to aid distributed system development. We present an alternative to these approaches, showing that modern, higher-order, strongly typed, memory safe languages provide an excellent vehicle for developing and debugging distributed systems. We present Opis, a functional-reactive approach for developing distributed systems in Objective Caml. An Opis protocol description consists of a reactive function (called event function) describing the behavior of a distributed system node. The event functions in Opis are built from pure functions as building blocks, composed using the Arrow combinators. Such architecture aids reasoning about event functions both informally and using interactive theorem provers. For example, it facilitates simple termination arguments. Given a protocol description, a developer can use higher-order library functions of Opis to 1) deploy the distributed system, 2) run the distributed system in a network simulator with full-replay capabilities, 3) apply explicit-state model checking to the distributed system, detecting undesirable behaviors, and 4) do performance analysis on the system. We describe the design and implementation of Opis, and present our experience in using Opis to develop peer-to-peer overlay protocols, including the Chord distributed hash table and the Cyclon random gossip protocol. We found that using Opis results in high programmer productivity and leads to easily composable protocol descriptions. Opis tools were effective in helping identify and eliminate correctness and performance problems during distributed system development.

2009