Presentation
When designing Plasma Lab we wanted to be able to use a distributed version either on a small network in our team or on a bigger network like a grid.
To test our distributed solution we used IGRIDA which is a computing cluster available to research teams at INRIA Rennes. For this experimentation we used the OAR scheduler which is in beta test phase on IGRIDA.
Test protocol
For our experimentation we used the Randomised dining philosophers (Lehmann & Rabin) problem in PRISM format. We used models with number of philosophers ranging from 3 to 300.
We have checked the property: ‘If a philosopher is hungry, then eventually some philosopher eats’ with a probability of 99% and a precision of 0.1% (Chernoff parameters epsilon = 0.001, delta = 0.99). These parameters result in more than 350000 generated traces for each experiments.
The Plasma Lab project containing all these models and properties can be downloaded here.
Results
Here are the results of our experiments.
Plasma Lab distributed algorithm performance
On this figure, duration of the experimentation in milliseconds is plotted against the number of IGRIDA nodes used for our experiments. The color of a plot indicate the number of philosophers for the experiment.
When multiplying the number of nodes by 2 we computed an average speedup of 1.66. The speedup increased with the complexity of the problem reaching the value of 1.79 for the 300 philosophers problem.
