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.     

A model-extraction approach to verifying concurrent C programs with CADP

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs.     

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 systematic approach to evaluating domain-specific modeling language environments for multi-agent systems

Multi-agent systems (MASs) include multiple interacting agents within an environment to provide a solution for complex systems that cannot be easily solved with individual agents or monolithic systems. However, the development of MASs is not trivial due to the various agent properties such as autonomy, responsiveness, and proactiveness, and the need for realization of the many different agent interactions. To support the development of MASs various domain-specific modeling languages (DSMLs) have been introduced that provide a declarative approach for modeling and supporting the generation of agent-based systems. To be effective, the proposed DSMLs need to meet the various stakeholder concerns and the related quality criteria for the corresponding MASs. Unfortunately, very often the evaluation of the DSML is completely missing or has been carried out in idiosyncratic approach. If the DSMLs are not well defined, then implicitly this will have an impact on the quality of the MASs. In this paper, we present an evaluation framework and systematic approach for assessing existing or newly defined DSMLs for MASs. The evaluation is specific for MAS DSMLs and targets both the language and the corresponding tools. To illustrate the evaluation approach, we first present SEA_ML, which is a model-driven MAS DSML for supporting the modeling and generation of agent-based systems. The evaluation of SEA_ML is based on a multi-case study research approach and provides both qualitative evaluation and quantitative analysis. We report on the lessons learned considering the adoption of the evaluation approach as well as the SEA_ML for supporting the generation of agent-based systems.     

A common intermediate language and its use in partitioning concurrent declarative programs

The plethora of concurrent declarative language families, each with subtly different semantics, makes the design and implementation of static analyses for these languages a demanding task. However, many of the languages share underlying structure, and if this structure can be exploited, static analysis techniques can be shared across language families. These techniques can thus provide a common kernel for the implementation of quality compilers for this entire language class. The purpose of this paper is to exploit the similarities of non-strict functional and concurrent logic languages in the design of a common intermediate language (CIL). The CIL is introduced incrementally, giving at each step the rationale for its extension. As an application, we present, in CIL form, some state-of-the-art static partitioning algorithms from the literature. This allows us to “uncover” the relative advantages and disadvantages of the analyses, and determine promising directions for improving static partitioning.     

并发程序中数据竞争检测方法

针对数据竞争检测过程中的误报和漏报问题，提出一种静态数据竞争检测方法。首先，使用控制流分析自动构造线程内和线程间函数调用图；然后，收集线程内变量访问事件信息，定义竞争产生条件并分析检测出所有可能的竞争；其次，为了提高检测的准确率，进行别名变量和别名锁的分析降低漏报和误报；最后，通过控制流分析来抽象访问事件之间的时序关系，并结合程序切片技术对访问事件的发生序关系进行判断，以此避免因忽略线程交互带来的误报。依据该方法，使用Java语言在Soot软件分析框架下实现了一个数据竞争检测工具。在实验中，对JGF和IBM Contest基准测试套件中的raytracer和airline等程序进行数据竞争检测，并与目前已有的数据竞争检测算法和工具（HB算法和RVPredict）进行对比。实验结果表明，与HB算法和RVPredict工具相比，该方法检测到的数据竞争总数分别增加了81%和16%，数据竞争检测的准确率分别提升了约14%和19%，有效地避免了数据竞争检测中的漏报和误报现象。     

DTL: A language for the design and implementation of concurrent programs as structured networks

DTL is an experimental programming language which has developed from an investigation of data structured design methods and data driven programming techniques. A DTL program is derived from a specification of the structure of its valid input and output languages. The program function is defined as a translation between these languages. A complex translation can be hierarchically structured into a network of simpler translations by stepwise refinement.     

A transformation‐based approach to testing concurrent programs using UML activity diagrams

Unified Modeling Language (UML) activity diagrams are widely used to model concurrent interaction among multiple objects. In this paper, we propose a transformation‐based approach to generating scenario‐oriented test cases for applications modeled by UML activity diagrams. Using a set of transformation rules, the proposed approach first transforms a UML activity diagram specification into an intermediate representation, from which it then constructs test scenarios with respect to the given concurrency coverage criteria. The approach then finally derives a set of test cases for the constructed test scenarios. The approach resolves the difficulties associated with fork and join concurrency in the UML activity diagram and enables control over the number of the resulting test cases. We further implemented a tool to automate the proposed approach and studied its feasibility and effectiveness using a case study. Experimental results show that the approach can generate test cases on demand to satisfy a given concurrency coverage criterion and can detect up to 76.5% of seeded faults when a weak coverage criterion is used. With the approach, testers can not only schedule the software test process earlier, but can also better allocate the testing resources for testing concurrent applications. Copyright © 2015 John Wiley & Sons, Ltd.     

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.     

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.     

A deadlock detection tool for concurrent Java programs

This paper presents some issues related to the design and implementation of a concurrency analysis tool able to detect deadlock situations in Java programs that make use of multithreading mechanisms. An abstract formal model is generated from the Java source using the Java2Spin translator. The model is expressed in the PROMELA language, and the SPIN tool is used to perform its formal analysis. The paper mainly focuses on the design of the Java2Spin translator. A set of experiments, carried out to evaluate the performances of the analysis tool, is also presented. Copyright © 1999 John Wiley & Sons, Ltd.     

A probe effect in concurrent programs

This paper reports on an experimental study of the probe effect, defined as an alteration in the frequency of run-time computational errors observed when delays are introduced into concurrent programs. If the concurrent program being studied has no synchronization errors, then there is no probe effect. In the presence of synchronization errors, the frequency of observable output errors for a sample experimental program starts at a high value for small delays, oscillates rapidly as the delay is increased, and apparently settles at zero errors for larger values of delay. Thus, for sufficiently large delays, the probe effect can almost completely mask synchronization errors in concurrent programs. For sufficiently large concurrent process sets, even small values of embedded delay may mask synchronization errors, provided side effects in shared memory are not included in the observation.     

From sequential programs to concurrent threads

Chip multiprocessors are of increasing importance due to difficulties in achieving higher clock frequencies in uniprocessors, but their success depends on finding useful work for the processor cores. This paper addresses this challenge by presenting a simple compiler approach that extracts non-speculative thread-level parallelism from sequential codes. We present initial results from this technique targeting a validated dual-core processor model, achieving speedups ranging from 9-48% with an average of 25% for important benchmark loops over their single-threaded versions. We also identify important next steps found during our pursuit of higher degrees of automatic threading.     

An approach to the development of debuggers that use semantics of constructs of parallel programs

In the paper, a new approach to the development of interactive debuggers for parallel programs that use message-passing model is suggested. The basic idea of the approach is to design a debugger specific to a particular language or a parallel programming library and to use information about the semantics of constructs used in the parallel program for processing commands of the step-by-step execution and data representation. The development of the user interface and internal debugger structure, as well as their implementations in the debuggers for mpC programs and programs using the MPI library, are considered.Translated from Programmirovanie, Vol. 31, No. 1, 2005. Original Russian Text Copyright © 2005 by Kalinov, Karganov, Khorenko.     

A parallel algorithm for static slicing of concurrent programs

Slicing of concurrent programs is a compute‐intensive task. To speed up the slicing process, we have developed a parallel algorithm. For this purpose we used the concurrent control flow graph (CCFG) as the intermediate representation. We used a network of communicating processes to develop our parallel algorithm. We have implemented our parallel algorithm and the experimental results appear promising. Copyright © 2004 John Wiley & Sons, Ltd.     

A declarative approach to visualizing concurrent computations

The authors explore the graphical representation of objects and processes as a means for understanding programs consisting of large numbers of concurrent processes. Their goal is to establish a technical foundation for research into the monitoring and debugging of large-scale concurrent programs. They explain declarative visualization and introduce some shared-data-space concepts and notation by means of a simple, nondeterministic, parallel algorithm. They discuss visual abstraction and their visualization methodology, which they illustrate by applying it to region labeling. Thy examine the relaxation of nonintervention that visualization makes possible     

CONCUR: A language for continuous, concurrent processes

Hendrix's robot modeling system presented a simulation method in which time is represented as a continuous phenomenon. This paper introduces the language CONCUR, which realizes Hendrix's concept through an extension of the LISP environment. CONCUR uses generalized procedures (scenarios) operating in a data-driven mode to implement Hendrix's events. The heart of CONCUR is a generalized pattern-matcher which permits operators within the patterns to bind variables and modify the match process. We include several detailed examples in addition to an implementation of the pattern matcher.     

A tactic language for refinement of state-rich concurrent specifications

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.     

Symbolic predictive analysis for concurrent programs

Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.