Systematic testing for actor programs

The growing use of multicore and networked computing systems is increasing the importance of developing reliable parallel and distributed code. Testing such code is notoriously difficult, especially for shared-memory models of programming. The actor model of programming offers a promising alternative for developing concurrent systems based on message passing. In actor-based systems, shared-memory access is not allowed, and the key source of non-determinism is the order in which messages are delivered to and processed by the actors. As a result, errors may occur in actor programs due to the incorrect interleaving of messages, conflicting constraints on what messages can be delivered, or errors in the sequential code within individual actors. The research community has expended a great deal of effort on the testing and verification of concurrent systems. However, much of this effort has been general in nature or focused on shared-memory models.;Given the differences in how errors manifest in actor programs, it seems natural that tools and techniques for testing such programs should take into account the particular nature of the actor model. To effectively and efficiently automate the detection of these errors, we propose a set of tools and techniques specifically designed to systematically explore the different behaviors of actor programs resulting from possible message delivery schedules.;Specifically, this dissertation presents Basset, a general framework for the systematic testing of actor systems developed with languages that compile to Java bytecode. This framework provides a common set of capabilities designed and implemented to take advantage of actor semantics. By building these capabilities into a language-independent core, they are available for use by any instantiation of the framework. This dissertation illustrates the practicality and effectiveness of this approach by presenting two tool instantiations of the Basset framework: one for the Scala programming language and the other for the ActorFoundry library for Java. The implementation of Basset was built as an extension to Java PathFinder, a popular model checker for Java, in order to leverage capabilities that already exist in that model checker. The Basset framework approach directly enables the relatively quick development of testing environments for actor-based languages and/or libraries that compile to Java bytecode.;This dissertation also considers the effectiveness of dynamic partial-order reduction techniques as they relate to the exploration of actor programs. The use of dynamic partial-order reduction speeds up systematic testing by pruning parts of the exploration space. However, the level of potential pruning is highly dependent on the order in which messages are considered for processing. This dissertation presents an evaluation of a number of heuristics for choosing the order in which messages are explored in Basset. The experiments show that the choice of heuristic can affect the number of execution paths that need to be explored by over two orders of magnitude.