Efficient testing of actor programs with non-deterministic behaviors

The actor model is a model of concurrent programming that consists of concurrent entities called actors. Actors communicate using asynchronous messages, and depending on the order in which they receive messages, they may exhibit different behaviors. This non-determinism brings significant challenges in testing techniques; to make sure that an actor program is correct, conceptually all possible interleavings of message receives should be explored. However, exploring all possible interleavings is not practical because the number of interleavings grows exponentially in the number of messages. This dissertation targets the problem of efficiently testing actor programs. Specifically, it considers three solutions for reducing the number of explored interleavings. Partial-order reduction (POR) techniques can substantially prune the number of explored interleavings. These techniques require defining a dependency relation on transitions in the program, and exploit independency among certain transitions to prune the state-space. We observe that actor systems exhibit a dependency relation among co-enabled transitions with an interesting property: transitivity. We propose a novel dynamic POR technique, TransDPOR, that exploits the transitivity of the dependency relation in actor systems. Empirical results show that leveraging transitivity speeds up exploration by up to two orders of magnitude compared to existing POR techniques. While TransDPOR makes exploration more efficient, experiments with TransDPOR on large programs reveal that the improvement may not overcome the exponential growth of the state-space. An observation is that a small subset of all possible interleavings might be sufficient to expose potential concurrency bugs. Having the fact that programmers—who have the knowledge of program specification—would be able to identify those interleavings, we developed two testing frameworks, Setac and Setak. These frameworks are developed for testing actor programs implemented in two popular actor libraries in the Scala language, namely Scala actor and Akka respectively. These frameworks allow programmers to specify constraints on order of messages—called schedule—and during execution, they enforce the specified schedule. In addition, Setac/Setak make it easy to check test assertions that require actors to be in a stable state. From our experience with the users of Setac/Setak, it turns out that in some cases specifying schedules is not straightforward for programmers. To address this problem, we propose Bita, a scalable and coverage-guided technique which automatically generates schedules. The key idea is to generate schedules that are likely to reveal concurrency bugs because these schedules increase the interleaving coverage. We present three interleaving coverage criteria for actor programs, an algorithm to generate feasible schedules whose executions increase coverage, and a technique to force a program execution to comply with a schedule. Applying Bita to real-world actor programs implemented in Akka reveals eight previously unknown concurrency bugs, of which six have already been fixed by the developers. Furthermore, we show Bita finds bugs 122x faster than random scheduling, on average.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2014

Author dc:creator

• Tasharofi, Samira

Contributors dc:contributor

• Johnson, Ralph E.
• Agha, Gul A.
• Marinov, Darko
• Musuvathi, Madan

• The Actor Model
• Concurrent Programs
• Testing Non-determinism
• Model Checking
• Testing Frameworks
• Coverage-based Testing.

Statement dc:rights

• Copyright 2013 Samira Tasharofi

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/46695

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/46695