Setac: A Framework for Phased Deterministic Testing of Actor Programs

Welcome to the Setac project homepage. Setac is a testing framework for Scala actor programs. It allows the programmers to write test cases by constraining the schedule of the system. Also it makes it easy to check test assertions that require actors to be in a stable state, i.e., no actor is processing any message and no message can be processed (until new messages are delivered)

Overview back to the top

In Setac, the programmer can mark relevant messages in the program under test as test messages for controlling schedules and checking assertions. Specifically, these are messages whose delivery/processing status is important for the purpose of testing. Controlling the schedule (to enforce a particular order between some messages) brings an element of determinism to test execution, hence a part of the name for Setac. Assertions should only be checked when the results are ready. In actor programs this usually happens when the individual actors process all the messages they can, i.e., the system reaches a stable state where no message can be processed (until new messages are delivered). This point of stability can be viewed as the end of a phase in the test execution. Indeed, Setac allows the programmer to break the entire execution of the test into multiple steps. Each step starts by delivering some messages, then lets the program run, and finally checks assertions. This feature creates a phased execution.

Compared to the current approaches for writing actor tests, Setac provides several advantages:

It allows the programmer to easier write tests with some explicit constraints on the message schedule. The schedule is the order of messages delivered to the actors. The constraints do not need to enforce order of all message from a test execution but can enforce ordering constraints only on a selected set of test messages. Allowing the programmer to enforce some partial constraints avoids two extreme situations: (1) the programmer has no control over the schedule, or (2) the programmer should specify all the details of the schedule although the order of some messages does not matter.
It makes it easy to check assertions in the stable state, which is usually the appropriate time for checking assertions. Without Setac, checking that the system is in a stable state is not straightforward in most cases.
It allows accessing the delivery/processing status of messages defined as test messages, which enables new types of assertions to be succinctly encoded. Additionally, providing a way to define test messages eliminates the need to change the program under test to keep track of the messages.
It reduces the cost of changing the program for the purpose of testing: the only change needed to use Setac is to make each actor class from the code under test a subclass of a Setac’s class rather than the standard Actor. Note that the programmer need not change literally every class in the program, but only the superclasses of those actors that are direct subclasses of Actor. Also note that this change can be easily automated.

Publication back to the top

Setac: A Framework for Phased Deterministic Testing of Scala Actor Programs

By Samira Tasharofi, Milos Gligoric, Darko Marinov, and Ralph Johnson.
Second Scala Workshop (Scala Days 2011)
Stanford, CA, June 2011. [pdf]. [ppt].

Illustrative Example back to the top

Bounded Buffer

As an example, consider the code for BoundedBuffer, which is used by Producer and Consumer:

class BoundedBuffer(size: Int) extends Actor { var content = new Array[Int](size) var head, tail, curSize = 0 start override def act() { loop { react { case Put(x) if (curSize < size) => { content(tail) = x tail = (tail + 1) % size curSize += 1 } case Get if (curSize > 0) => { val r = content(head) head = (head + 1) % size curSize -= 1 reply(r) } } } } } class Consumer(buf: Actor) extends Actor { var token = -1 start override def act() { loop { react { case Consume(count) => { for (i <- 0 to count-1) token = (buf !? Get).asInstanceOf[Int] } } } } } class Producer(buf: Actor) extends Actor { start override def act() { loop { react { case Produce(values) => { values.foreach(v => buf ! Put(v)) } } } } }

We want to test the following scenarios:

Testing empty buffer: check the behavior of an empty buffer. The test consists of three phases: (1) deliver a Get message and check if the consumer is blocked or not; (2) deliver two Put messages and check if the value received by consumer is the first value put in the buffer and the second Put message is processed; (3) deliver another Get message and check if what is received by the consumer is the same as the second value produced by the producer.

Testing full buffer: check the behavior of a full buffer. The test consists of three phases: (1) deliver two Put messages and check if the second one still remains in the mailbox; (2) deliver one Get message and check if the value received by the consumer is the same as the first value put in the buffer and also the second Put message is processed; (3) deliver another Get messages and then check if the value received by the consumer equals to the second value put in the buffer.

Steps in writing tests

Each test class is a test suite that consists of three parts: setUp, test methods, and tearDown. Each test method is a test case that contains the test scenario.

Prepare the program under test: to make the test control the execution of the program under test, each class that extends Actor should be replaced with TestActor. Declaration of the classes from our example would change as follows:

class BoundedBuffer(size: Int) extends TestActor class Consumer(buf: Actor) extends TestActor class Producer(buf: Actor) extends TestActor

Recall that this is the only change to the original code under test.

Define test messages: test messages that are used for constraining the schedule (schedule messages) should be defined before the test starts. So, setUp is a good place to define them

class BufferTest extends SetacTest { var buf: BoundedBuffer = _ var con: Consumer = _ var pr: Producer = _ var put1: TestMessage = _ var put2: TestMessage = _ var get1: TestMessage = _ var get2: TestMessage = _ override def setUp() { buf = new BoundedBuffer(1) consumer = new Consumer(buf) producer = new Producer(buf) put1 = createScheduleMessage(producer, buf, Put(1)) put2 = createScheduleMessage(producer, buf, Put(2)) get1 = createScheduleMessage(consumer, buf, Get) get2 = createScheduleMessage(consumer, buf, Get) producer ! Produce(List(1, 2)) consumer ! Consume(2) } @Test def testEmptyBuffer(){ // ... } @Test def testFullBuffer(){ // ... } }

Writing the test scenario by controlling schedule and checking assertions: two APIs, setSchedule (to constraint schedule) and assertWhenStable (check assertions in the stable state of the system), can be used for this purpose.

@Test def testEmptyBuffer() { // Phase1 setSchedule(get1) assertWhenStable(consumer.isBlocked, "consumer is not blocked") assertWhenStable(consumer.token == -1, "something is received by the consumer") // Phase2 setSchedule(put1 -> put2) assertWhenStable(consumer.token == 1, "consumer did not receive the first value") assertWhenStable(put2.isProcessed, "the second put should is not processed") // Phase3 setSchedule(get2) assertWhenStable(consumer.token == 2, "the second value is not received") } @Test def testFullBuffer() { // Phase1 setSchedule(put1 -> put2) assertWhenStable(buf.msgCountInMailbox(put2) == 1, "the second put is processed") // Phase2 setSchedule(get1) assertWhenStable(put2.isProcessed, "the second put should is not processed") assertWhenStable(consumer.token == 1, "the first value is not received") // Phase3 setSchedule(get2) assertWhenStable(consumer.token == 2, "the second value is not received" ) }

Downloads back to the top

Prerequisites

Java version 1.6 or higher
Scala version 2.8.0 or higher: the latest version of Scala can be downloaded from: http://www.scala-lang.org/downloads
Apache Ant that can be downloaded from: http://ant.apache.org/
Set SCALA_HOME variable to scala directory and add scala bin directory to the PATH variable. For example:
For Windows: set the variable %SCALA_HOME% to C:/Progra~1/Scala, and set the variable %PATH% to %PATH%;%SCALA_HOME%/bin
For Unix: set the variable $SCALA_HOME to /usr/local/share/scala, and set the variable $PATH to $PATH:$SCALA_HOME/bin

Setac

The latest version of Setac can be downloaded from :

http://mir.cs.illinois.edu/setac/setac.zip

How to use Setac?back to the top

Here are the instructions for installing and using Setac to write test cases.

After downloading Setac, extract the zip file.
In order to compile Setac, together with the examples, execute the following command:

> ant

To run a test (e.g., the test for bounded buffer), use setac command with the name of the test class as its argument:

> ./setac.sh -t edu.illinois.cs.setac.examples.boundedbuffer.BufferTest

src/edu/illinois/cs/setac/examples directory contains example programs and their test cases.

Setac: A Framework for Phased Deterministic Testing of Actor Programs

On This Page

Overviewback to the top

Publicationback to the top