Systematic testing of actor systems: Systematic testing of actor systems

Testing concurrent systems requires exploring all possible nondeterministic interleavings that the concurrent execution may have, as any of the interleavings may reveal the erroneous behavior. In testing of actor systems, we can distinguish 2 sources of nondeterminism: (1) actor selection, the order in which actors are explored, and (2) task selection, the order in which the tasks within each actor are explored. This article provides new strategies and heuristics for pruning redundant state-exploration when testing actor systems by reducing the amount of unnecessary nondeterminism of both types. Furthermore, we extend these techniques to handle synchronization primitives that allow awaiting for the completion of an asynchronous task. We report on an implementation and experimental evaluation of the proposed techniques in SYCO, a testing tool for actor-based concurrency.