A novel framework for non-deterministic testing of message-passing programs

Message-passing programs are difficult to test because of their non-deterministic behavior. One approach, called non-deterministic testing, involves executing a message-passing program with the same input many times in hope that faults would be exposed by one of these executions. Non-deterministic testing has been widely used in practice, but unfortunately, in an ad-hoc manner. In this paper, we present a novel framework for non-deterministic testing of message-passing programs. The framework uses a coverage criterion to guide the testing process. During each test run, the sequence of send and receive events that are executed is recorded in an execution trace. After each test run, the trace is analyzed to identify race conditions, which are used to derive coverage elements that have not been covered yet. Then, random delays are inserted at a chosen set of program locations in order to increase the chance of covering the uncovered elements in the next test run. This framework provides a heuristic condition that can be used to decide when to stop testing. The condition is easy to compute and its satisfaction signals that the coverage criterion has likely been satisfied. This framework can be automated at the source code level and allows one to obtain a measure of test coverage at the end of the testing process. We describe a prototype tool and report some empirical results that demonstrate the effectiveness of our framework.