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 ci,
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.