Application of Model-Based Testing to a Stack

Today I would like to go back to basics, and also show how to easily switch the underlying implementation. Some of my most read posts are on applying Model-Based Testing to basic data structures, so why not pick up yet another basic data structure?

This time I’m keeping it ultra-simple: The Stack.

I’m sure we all know what a stack is, but to briefly remind you it’s a LIFO (Last-in, first-out) container. In a classic stack elements are added on top of the stack using the “Push” command and removed from the top one-by-one using “Pop”. When an element is popped it is removed from the stack and returned. It is not possible to reference elements that are not on the top of the stack.

A not-so-classic stack variation contains a “Peek” function that will return the top element of the stack without removing it.

So without further ado let’s jump into modeling!

Multi-Threaded Modeling – Barrier Synchronization

Okay, all my previous posts have been based on static system models, where rules and actions are static functions in classes. A lot can be accomplished with this, and it is also possible to wrap instance based applications inside static functions. However, Spec Explorer allows us to work with actual instance based models.

So what does this mean for us? Well, it means we are allowed to instantiate any number of objects of some type and Spec Explorer can reference each of these objects individually. For example, you could write a class that represents a complex number, and have Spec Explorer create two instances of this object and then add them together. This would be a basic example, but instead let’s jump to something more tricky – multi-threading!

You can imagine that instance based modeling and multi-threading are closely related. But there are some key issues one must understand first. Instance based modeling is not multi-threaded, it is exactly as sequential as any static model. Spec Explorer will not create a new thread for you when you instantiate an object. Any interaction by Spec Explorer will be from the “main”-thread, you have to handle communication with your threads.

Barrier synchronization

The example I have picked for this post is a barrier synchronization implementation. Barrier synchronization is a pattern for worker threads in multi-threaded application. With barrier synchronization each thread must wait for its co-workers to complete their cycle of work before the next cycle starts. Denoting the number of cycles completed by thread i as c_i, this can be stated by the following invariant:

          

Essentially each thread reaches a “barrier” upon completion of its work. This “barrier” is only lowered once all threads have reached it. Upon release of the “barrier” the worker threads continues their work.