Here we will have a closer look at our distributed algorithm.
PLASMA Lab can be set to a distributed mode when running an experiment. This mode uses a second software called PLASMA Service. Local or Distributed mode use the same interface. For more details on PLASMA Lab architecture, refer to PLASMA Structure page.
Sequence diagram of a session between PLASMA Lab and PLASMA Service
Step 0: Publishing a Restlet service
PLASMA Lab: I need help to run this experiment.
When launching a distributed experimentation, PLASMA Lab publish an interface on a Restlet Server (this server being part of PLASMA Lab code). Publishing this interface will allow other program to retrieve the interface and use its functions.
We call Client a PLASMA Service instance and the Server the PLASMA Lab instance who published the interface.
Step 1: Connecting to PLASMA Lab
PLASMA Service: I can help you.
PLASMA Lab: Ok, here are the experiment parameters.
When a client connect itself to the server, it retrieves the RMI Interface and call the connect function. This function return the experiment parameters containing the model and the list of properties to check. These parameters also contains an id to allow clients to identify themselves.
Step 2: Getting a share of the work
PLASMA Service: I am ready to work.
PLASMA Lab: Run K simulation and check the properties.
The client then call the service ready function. This function will inform the server that this client is ready and will return an integer K. This integer represents the number of traces that the client has to generate. K can take several values:
- K = -1 means that the work is done, the client can disconnect.
- K = 0 tells the client to wait. This is used to wait for more client to connect before launching the simulation.
- K > 0 tells the client to generate K execution traces and check the properties on these traces.
Step 3: Returning the results
PLASMA Service: Here are my results.
The client call the work done function. This function send the results to the server. The client then return to step 2.
Work scheduling and avoiding biais
PLASMA Lab implements a scheduler as described in [You05a]. To summarize, because a negative trace (on which a property doesn not hold) is faster to check than a positive trace (you have to read the whole trace to see that it is a positive trace) a biais can form on a distributed Statistical Model Checking.
Our scheduler keep the order of each task assigned to a client and only take results into account on this order. This ensure that a task launched at time t will be taken into accound before a task launched at a time > t.
Moreover, this scheduler ensure that a faster client will be given more work and contribute more to the overall effort. We also implemented some ideas coming from the Slow-Start algorithm used in TCP to reduce the client-server communications.
