Modeling Multi-Threaded Applications

So last time we looked a bit at stochastic modeling and I introduced the concept in Spec Explorer for modeling random actions/decisions. The example we looked at was a stochastic counter – which is just a tiny bit contrived. Actually, I can’t think of anywhere I would like to use a stochastic counter. Thus, I want to spent some time modeling a real stochastic example in this post.

A very common use of stochasticity is multi-threading/parallel processing. In a parallel system more than one thread can work on solving a problem at the same time (often running on multiple CPUs at the same time). So why does this have to lead to stochastic systems? – you may ask. The fundamental answer to this question is timing. In a parallel environment, to make full use of system resources, you poll a pool of threads for the next available worker thread. Whichever thread is available is determined by “chance”, because it is impacted by the speed of the executing CPUs, latency of external dependencies (RAM, BUS, network, disk, etc.) which we (usually) cannot control.

Consider a fictitious parallel environment with 3 worker threads:

This component is used by assigning the Job Scheduler a Job to be processed, then the scheduler will hold this job in its internal queue and await a worker thread to be available, once a thread is available it will take the incoming Job and start processing it in its own execution context (i.e. CPU, RAM, etc.). After successfully processing the Job the worker thread stores the result in an aggregated result list (which has to be thread-safe).

A very common sunshine scenario to test would be to give the Job Scheduler a single Job and check that a worker thread starts working on it and finally check the result from the aggregated result list.

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.