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.     

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

During a human-exoskeleton collaboration, the interaction torque on exoskeleton resulting from the human cannot be clearly determined and conducted by normal physical models. This is because the torque depends not only on direction and orientation of both human-operator and exoskeleton but also on the physical properties of each operator. In this paper, we present our investigations on the relationship between the interaction torques with the dynamic factors of the human-exoskeleton systems using state-of-the-art learning techniques （nonparametric regression techniques） and provide control applications based on the findings. Exper- imental data was collected from various human-operators when they were attached to the designed exoskeleton to perform unconstraint motions with and without control. The results showed that regardless of how the ex- periments were done and which learning method was chosen, the resulting interaction could be best represented by time varying non-linear mappings of the operator＇s angular position, and the exoskeleton＇s angular position, velocity, and acceleration during locomotion. This finding has been applied to advanced controls of the lower exoskeletal robots in order to improve their performance while interacting with human.     

A combinatorial testing strategy for concurrent programs

One approach to testing concurrent programs is called reachability testing, which derives test sequences automatically and on‐the‐fly, without constructing a static model. Existing reachability testing algorithms are exhaustive in that they are intended to exercise all possible synchronization sequences of a concurrent program with a given input. In this paper, we present a new testing strategy, called t‐way reachability testing, that adopts the dynamic framework of reachability testing but selectively exercises a subset of synchronization sequences. The selection of the synchronization sequences is based on a combinatorial testing strategy called t‐way testing. We present an algorithm that implements t‐way reachability testing, and report the results of several case studies that were conducted to evaluate its effectiveness. The results indicate that t‐way reachability testing can substantially reduce the number of synchronization sequences exercised during reachability testing while still effectively detecting faults. Copyright © 2007 John Wiley & Sons, Ltd.     

Instant replay debugging of concurrent logic programs

One problem with debugging (committed choice) concurrent logic programs is that their behaviour may be non-deterministic, in that successive executions of the same program may produce different results. We describe a scheme, based on the ‘Instant Replay’ scheme developed for more conventional parallel languages, that allows us to reproduce the execution behaviour of a concurrent logic program on subsequent executions, so that the execution may be examined for debugging purposes. The properties of concurrent logic programming languages allow us to simplify our scheme greatly. We have demonstrated our scheme with KLIC, and KL1 on the PIM multiprocessors, but it can also be applied to other committed choice concurrent logic programming languages.     

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     

Validating a demonstration tool for graphics-assisted debugging ofAda concurrent programs

A demonstration-quality graphics-assisted debugger is developed for intertask communication in Ada. Based on the static task-specification diagrams of G. Booch (Software Engineering with Ada, Benjamin/Cummings, 1983), the debugger animates the activity of a collection of communicating tasks, and it runs on a DEC GIGI terminal connected to a VAX 11-780 under TeleSoft's partial Ada compiler. The model has been subjected to empirical validation, using undergraduate students as experimental subjects. Subjects were required to debug erroneous tasking programs using both the graphical debugger and a textual one. It is concluded that although the problems to be addressed in the development and evaluation of a graphical debugging tool for Ada tasks are nontrivial, the benefits could be worth the effort     

A systematic review of approaches for testing concurrent programs

Concurrent programs are replacing the sequential programs as they utilize the true capabilities of multicore architecture. The extensive use of multicore systems and multithreaded paradigms warrants more attention to the testing of the concurrent programs. The testing concurrent program is not a new field as it has been more than 40 years because the first problem related to the testing concurrent program was addressed by the researchers. The field covers various domains, which include concurrency problems, testing approaches, techniques, graphical representations, tools, and subject systems. This paper aims at providing an overview of research in the domain of testing concurrent programs by classifying it into eight categories: (a) reachability testing, (b) structural testing, (c) model‐based testing, (d) mutation‐based testing, (e) slicing‐based testing, (f) formal methods, (g) random testing, and (h) search‐based testing. The survey is focused on the techniques applied, methodologies followed, and tools used in these aforementioned approaches. Furthermore, the gaps are also identified in different approaches. The paper concludes with the consolidation of various testing parameters along with the future directions. Copyright © 2015 John Wiley & Sons, Ltd.     

Structural testing of concurrent programs

Although structural testing techniques are among the weakest available with regard to developing confidence in sequential programs, they are not without merit. The authors extend the notion of structural testing criteria to concurrent programs and propose a hierarchy of supporting structural testing techniques. Coverage criteria described include concurrency state coverage, state transition coverage and synchronization coverage. Requisite support tools include a static concurrency analyzer and either a program transformation system or a powerful run-time monitor. Also helpful is a controllable run-time scheduler. The techniques proposed are suitable for Ada or CSP-like languages. Best results are obtained for programs having only static naming of tasking objects     

Reachability testing of concurrent programs

One approach to testing concurrent programs, called reachability testing, generates synchronization sequences automatically and on-the-fly, without constructing any static models. In this paper, we present a general execution model for concurrent programs that allows reachability testing to be applied to several commonly used synchronization constructs. We also present a new method for performing reachability testing. This new method guarantees that every partially ordered synchronization sequence will be exercised exactly once without having to save any sequences that have already been exercised. We describe a prototype reachability testing tool called RichTest and report some empirical results, including a comparison between RichTest and a partial order reduction-based tool called VeriSoft. RichTest performed significantly better for the programs in our study.     

Incremental integration testing of concurrent programs

We present a method for selecting test sequences for concurrent programs from labeled transitions systems (LTS). A common approach to selecting test sequences from a set of LTSs is to derive a global LTS, called the reachability graph, and then force deterministic program executions according to paths selected from the graph. However, using a reachability graph for test path selection introduces a state explosion problem. To overcome this problem, a reduced graph can be generated using incremental reachability analysis, which consists of repeatedly generating a reachability graph for a subset of LTSs, reducing this graph, and using the reduced graph in place of the original LTSs. Unfortunately, existing incremental reachability analysis techniques generate reduced graphs with insufficient information for deterministic testing. We present an incremental approach to testing concurrent programs. Incremental testing consists of incremental reachability analysis for test path selection and deterministic testing for test execution. We define a new type of reachability graph for incremental analysis, called an annotated labeled transition system (ALTS). An ALTS is an LTS annotated with information necessary for deterministic testing. We propose practical coverage criteria for selecting tests paths from an ALTS and present an ALTS reduction algorithm. The results of several case studies are reported     

Distributed reachability testing of concurrent programs

Reachability testing is an approach to verifying concurrent programs. During reachability testing, every partially ordered synchronization sequence of a program with a given input is exercised exactly once. In this paper, we present the design and implementation of a distributed reachability testing algorithm for a cluster of workstations. This algorithm allows different test sequences to be exercised concurrently by different workstations without any synchronization, and without any duplication of sequences among workstations. Dynamic load balancing is performed using a work‐stealing scheme. A novel aspect of this scheme is that work‐stealing requests progress in rounds. This round‐based structure identifies overloaded workstations to target for work stealing. Empirical studies show good speedup for four benchmark Java programs and one Lotos specification. Copyright © 2010 John Wiley & Sons, Ltd.     

An object-oriented class library for C++ programs

The Object-Oriented Program Support (OOPS) class library is a portable collection of classes similar to those of Smalltalk-80 that has been developed using the C++ programming language under the UNIX operating system. The OOPS library includes generally useful data types, such as String, Date and Time, and most of the Smalltalk-80 collection classes such as OrderedCtn (indexed arrays), LinkedList (singly linked lists), Set (hash tables), and Dictionary (associative arrays). Arbitrarily complex data structures comprised of OOPS and user-defined objects can be stored on disk files or moved between UNIX processes by means of an object I/O facility. The classes Process, Scheduler, Semaphore and SharedQueue provide multiprogramming with coroutines. This paper gives a brief introduction to object-oriented programming and how it is supported by the C+ + programming language. An overview of the OOPS library is also presented, followed by a programming example. The implementation details of two of the class library's more interesting features, object I/O and processes, are described. The paper concludes with a discussion of the differences between the OOPS library and Smalltalk-80 and some observations based on our programming experience with C++ and OOPS.     

A debugger for concurrent programs

This paper reports on an experimental debugger for concurrent programs. Design objectives include a showing of greatest usefulness when dealing with multiprocess interactions, creation of a simplified more approachable interface for programmers, allowance for the systematic organization (and limitation) of debugging information by programmers, reflection of a natural view of concurrency, and portability. The design responds to a perceived need for debugging techniques applicable in systems of concurrent, communicating, asynchronous processes. During debugging sessions, a user is able to dynamically explore interprocess synchronization points, parallel actions and deadlock situations. The programmer interface is based on a transparent window multiplexer providing a set of windows for each concurrent process. The window manager interactively maps interesting windows to programmer-specified viewscreen locations, while relegating temporarily uninteresting windows to the background. In implementing a debugger for concurrent programs, a principal concern is the probe effect, or the possibility that the debugger itself masks synchronization errors in the program being debugged. For the examples explored, the probe effect was not observed to limit the localization of implanted synchronization errors.     

A graphical development and debugging environment for parallel programs

To provide high-level graphical support for PVM (Parallel Virtual Machine) based program development, a complex programming environment (GRADE) is being developed. GRADE currently provides tools to construct, execute, debug, monitor and visualize message-passing parallel programs. It offers a high-level graphical programming abstraction mechanism to construct parallel applications by introducing a new graphical language called GRAPNEL. GRADE also provides the programmer with the same graphical user interface during the program design and debugging stages. A distributed debugging engine (DDBG) assists the user in debugging GRAPNEL programs on distributed memory computer architectures. Tape/PVM and PROVE support the performance monitoring and visualization of parallel programs developed in the GRADE environment.     

Variable strength combinatorial testing of concurrent programs

Reachability testing is an important approach to testing concurrent programs. It generates and exercises synchronization sequences automatically and on-the-fly without saving any test history. Existing reachability testing can be classified into exhaustive and t-way testing. Exhaustive testing is impractical in many cases while t-way testing may decrease the capability of fault detection in some cases. In this paper, we present a variable strength reachability testing strategy, which adopts the dynamic framework of reachability testing and uses a variable strength combinatorial strategy. Different parameter groups are provided with different covering strength. Variable strength testing covers no t-way combinations but the necessary combinations of parameters having mutual interactions in a concurrent program. It is more reasonable than t-way testing because uniform interactions between parameters do not often exist in concurrent systems. We propose a merging algorithmthat implements the variable strength combinatorial testing strategy and conduct our experiment on several concurrent programs. The experimental results indicate that our variable strength reachability testing reaches a good tradeoff between the effectiveness and efficiency. It can keep the same capability of fault detection as exhaustive reachability testing while substantially reducing the number of synchronization sequences and decreasing the execution time in most cases.     

A simulator for real-time software debugging and testing

A software simulator can be built to facilitate debugging and testing of real-time programs. This paper describes a simulator designed to operate in three modes: simulation, debugging and process monitoring. In the simulation mode, it simulates a Z80-based microcomputer and can be used to execute programs written in the Z80-assembler language. In the debugging mode, it provides facilities for interactive debugging on the instruction level. The simulator's unique feature is the process monitoring mode. It displays the activities among processes being executed concurrently under the control of a real-time executive and thus allowing direct observation of dynamic program behaviour at the process level.     

A workbook-based methodology for implementing concurrent engineering

Concurrent Engineering demands a new way of working and many organisations experience difficulty during implementation. The research described in this paper has the aim to develop a paper-based workbook style methodology that companies can use to increase the benefits generated by Concurrent Engineering, while reducing implementation costs, risk and time.

The three-stage methodology provides guidance based on knowledge accumulated from implementation experience and best practitioners. It encourages companies to learn to manage their Concurrent Engineering implementation by taking actions which expose them to new and valuable experiences. This helps to continuously improve understanding of how to maximise the benefits from Concurrent Engineering.

The methodology is particularly designed to cater for organisational and contextual uniqueness, as Concurrent Engineering implementations will vary from company to company. Using key actions which improve the Concurrent Engineering implementation process, individual companies can develop their own ‘best practice’ for product development. The methodology ensures that key implementation issues, which are primarily human and organisational, are addressed using simple but proven techniques.

This paper describes the key issues that the majority of companies face when implementing Concurrent Engineering. The structure of the methodology is described to show how the issues are addressed and resolved. The key actions used to improve the Concurrent Engineering implementation process are explained and their inclusion in the implementation methodology described.

Relevance to industry

Implementation of Concurrent Engineering concepts in manufacturing industry has not been a straightforward process. This paper describes a workbook-style tool that manufacturing companies can use to accelerate and improve their Concurrent Engineering implementation.     

A performance debugging tool for high performance Fortran programs

Parallel languages allow the programmer to express parallelism at a high level. The management of parallelism and the generation of interprocessor communication is left to the compiler and the runtime system. This approach to parallel programming is particularly attractive if a suitable widely accepted parallel language is available. High Performance Fortran (HPF) has emerged as the first popular machine independent parallel language, and remarkable progress has been made towards compiling HPF efficiently. However, the performance of HPF programs is often poor and unpredictable, and obtaining adequate performance is a major stumbling block that must be overcome if HPF is to gain widespread acceptance. The programmer is often in the dark about how to improve the performance of an HPF program since poor performance can be attributed to a variety of reasons, including poor choice of algorithm, limited use of parallelism, or an inefficient data mapping. This paper presents a profiling tool that allows the programmer to identify the regions of the program that execute inefficiently, and to focus on the potential causes of poor performance. The central idea is to distinguish the code that is executing efficiently from the code that is executing poorly. Efficient code uses all processors of a parallel system to make progress, while inefficient code causes processors to wait, execute replicated code, idle, communicate, or perform compiler bookkeeping. We designate the latter code as non-scalable, since adding more processors generally does not lead to improved performance for such code. By analogy, the former code is called scalable. The tool presented here separates a program into scalable and non-scalable components and identifies the causes of non-scalability of different components. We show that compiler information is the key to dividing the execution times into logical categories that are meaningful to the programmer. We present the design and implementation of a profiler that is integrated with Fx, a compiler for a variant of HPF. The paper includes two examples that demonstrate how the data reported by the profiler are used to identify and resolve performance bugs in parallel programs. © 1997 John Wiley & Sons, Ltd.     

A debugging and testing tool for supporting software evolution

This paper describes a tool for debugging programs which develop faults after they have been modified or are ported to other computer systems. The tool enhances the traditional debugging approach by automating the comparison of data structures between two running programs. Using this technique, it is possible to use early versions of a program which are known to operate correctly to generate values for comparison with the new program under development. The tool allows the reference code and the program being developed to execute on different computer systems by using open distributed systems techniques. A data visualisation facility allows the user to view the differences in data structures. By using the data flow of the code, it is possible to locate faulty sections of code rapidly. An evaluation is performed by using three case studies to illustrate the power of the technique.     

A proof system for concurrent ADA programs

A subset of ADA is introduced, ADA-CF, to study the basic synchronization and communication primitive of ADA, the rendezvous. Basing ourselves on the techniques introduced by Apt, Francez and de Roever for their CSP proof system, we develop a Hoare-style proof system for proving partial correctness properties which is sound and relatively complete. The proof system is then extended to deal with safety, deadlock, termination and failure. No prior exposure of the reader to parallel program proving techniques is presupposed. Two non-trivial example proofs are given of ADA-CF programs; the first one concerns a buffered producer-consumer algorithm, the second one a parallel sorting algorithm due to Brinch Hansen. Features of ADA expressing dynamic process creation and realtime constraints are not covered by our proof methods. Consequently, we do not claim that the methods described can be extended to full ADA without serious additional further research.