We present CONCURRIT, a domain-specific language (DSL) for reproducing concurrency bugs. Given some partial information about the nature of a bug in an application, a programmer can write a CONCURRIT script to formally and concisely specify a set of thread schedules to explore in order to find a schedule exhibiting the bug. Further, the programmer can specify how these thread schedules should be searched to find a schedule that reproduces the bug. We implemented CONCURRIT as an embedded DSL in C++, which uses manual or automatic source instrumentation to partially control the scheduling of the software under test. Using CONCURRIT, we were able to write concise tests to reproduce concurrency bugs in a variety of benchmarks, including the Mozilla's SpiderMonkey JavaScript engine, Memcached, Apache's HTTP server, and MySQL.

Nondeterministic Sequential (NDSeq) specifications have been proposed as a means for separating the testing, debugging, and verifying of a program's parallelism correctness and its sequential functional correctness. In this work, we present a technique that, given a few representative executions of a parallel program, combines dynamic data flow analysis and Minimum-Cost Boolean Satisfiability (MinCostSAT) solving for automatically inferring a likely NDSeq specification for the parallel program. For a number of Java benchmarks, our tool NDetermin infers equivalent or stronger NDSeq specifications than those previously written manually.

In practice, it is quite difficult to write correct multithreaded programs due to the potential for unintended and nondeterministic interference between parallel threads. A fundamental correctness property for such programs is atomicity---a block of code in a program is atomic if, for any parallel execution of the program, there is an execution with the same overall program behavior in which the block is executed serially.We propose semantic atomicity, a generalization of atomicity with respect to a programmer-defined notion of equivalent behavior. We propose an assertion framework in which a programmer can use bridge predicates to specify noninterference properties at the level of abstraction of their application. Further, we propose a novel algorithm for systematically testing atomicity specifications on parallel executions with a bounded number of interruptions---i.e. atomic blocks whose execution is interleaved with that of other threads. We further propose a set of sound heuristics and optional user annotations that increase the efficiency of checking atomicity specifications in the common case where the specifications hold.We have implemented our assertion framework for specifying and checking semantic atomicity for parallel Java programs, and we have written semantic atomicity specifications for a number of benchmarks. We found that using bridge predicates allowed us to specify the natural and intended atomic behavior of a wider range of programs than did previous approaches. Further, in checking our specifications, we found several previously unknown bugs, including in the widely-used java.util.concurrent library.

High-performance concurrent libraries, such as lock-free data structures and custom synchronization primitives, are notoriously difficult to write correctly. Such code is often implemented without locks, instead using plain loads and stores and low-level operations like atomic compare-and-swaps and explicit memory fences. Such code must run correctly despite the relaxed memory model of the underlying compiler, virtual machine, and/or hardware. These memory models may reorder the reads and writes issued by a thread, greatly complicating parallel reasoning. We propose RELAXER, a combination of predictive dynamic analysis and software testing, to help programmers write correct, highly-concurrent programs. Our technique works in two phases. First, RELAXER examines a sequentially-consistent run of a program under test and dynamically detects potential data races. These races are used to predict possible violations of sequential consistency under alternate executions on a relaxed memory model. In the second phase, RELAXER re-executes the program with a biased random scheduler and with a conservative simulation of a relaxed memory model in order to create with high probability a predicted sequential consistency violation. These executions can be used to test whether or not a program works as expected when the underlying memory model is not sequentially consistent. We have implemented RELAXER for C and have evaluated it on several synchronization algorithms, concurrent data structures, and parallel applications. RELAXER generates many executions of these benchmarks with violations of sequential consistency, highlighting a number of bugs under relaxed memory models.

We propose to specify the correctness of a program's parallelism using a sequential version of the program with controlled nondeterminism. Such a nondeterministic sequential specification allows (1) the correctness of parallel interference to be verified independently of the program's functional correctness, and (2) the functional correctness of a program to be understood and verified on a sequential version of the program, one with controlled nondeterminism but no interleaving of parallel threads.

The trend towards multicore processors and graphic processing units is increasing the need for software that can take advantage of parallelism. Writing correct parallel programs using threads, however, has proven to be quite challenging due to nondeterminism. The threads of a parallel application may be interleaved nondeterministically during execution, which can lead to nondeterministic results---some interleavings may produce the correct result while others may not. We have previously proposed an assertion framework for specifying that regions of a parallel program behave deterministically despite nondeterministic thread interleaving. The framework allows programmers to write assertions involving pairs of program states arising from different parallel schedules. We propose an algorithm to dynamically infer likely deterministic specifications for parallel programs given a set of inputs and schedules. We have implemented our specification inference algorithm for Java and have applied it to a number of previously examined Java benchmarks. We were able to automatically infer specifications largely equivalent to or stronger than our manual assertions from our previous work. We believe that the inference of deterministic specifications can aid in understanding and documenting the deterministic behavior of parallel programs. Moreover, an unexpected deterministic specification can indicate to a programmer the presence of erroneous or unintended behavior.

Program analysis and automated test generation have primarily been used to find correctness bugs. We present complexity testing, a novel automated test generation technique to find performance bugs. Our complexity testing algorithm, which we call WISE (worst-case inputs from symbolic execution), operates on a program accepting inputs of arbitrary size. For each input size, WISE attempts to construct an input which exhibits the worst-case computational complexity of the program. WISE uses exhaustive test generation for small input sizes and generalizes the result of executing the program on those inputs into an ldquoinput generator.rdquo The generator is subsequently used to efficiently generate worst-case inputs for larger input sizes. We have performed experiments to demonstrate the utility of our approach on a set of standard data structures and algorithms. Our results show that WISE can effectively generate worst-case inputs for several of these benchmarks.

When a running program becomes unresponsive, it is often impossible for a user to determine if the program is performing some useful computation or if it has entered an infinite loop. We present LOOPER, an automated technique for dynamically analyzing a running program to prove that it is non-terminating. LOOPER uses symbolic execution to produce simple non-termination arguments for infinite loops dependent on both program values and the shape of heap. The constructed arguments are verified with an off-the-shelf SMT solver. We have implemented our technique in a prototype tool for Java applications, and we demonstrate our technique's effectiveness on several non-terminating benchmarks, including a reported infinite loop bug in open-source text editor jEdit. Our tool is able to dynamically detect infinite loops deep in the execution of large Java programs with no false warnings, producing symbolic arguments that can aid in debugging non-termination.

The trend towards processors with more and more parallel cores is increasing the need for software that can take advantage of parallelism. The most widespread method for writing parallel software is to use explicit threads. Writing correct multithreaded programs, however, has proven to be quite challenging in practice. The key difficulty is non-determinism. The threads of a parallel application may be interleaved non-deterministically during execution. In a buggy program, non-deterministic scheduling will lead to non-deterministic results - some interleavings will produce the correct result while others will not.

Recently there has been great success in using symbolic execution to automatically generate test inputs for small software systems. A primary challenge in scaling such approaches to larger programs is the combinatorial explosion of the path space. It is likely that sophisticated strategies for searching this path space are needed to generate inputs that effectively test large programs (by, e.g., achieving significant branch coverage). We present several such heuristic search strategies, including a novel strategy guided by the control flow graph of the program under test. We have implemented these strategies in CREST, our open source concolic testing tool for C, and evaluated them on two widely-used software tools, grep 2.2 (15 K lines of code) and Vim 5.7 (150 K lines). On these benchmarks, the presented heuristics achieve significantly greater branch coverage on the same testing budget than concolic testing with a traditional depth-first search strategy.