Model Checking for Integrating Dynamic Load Distribution into Parallel Applications

Many parallel applications running on a distributed memory cluster generate data dynamically to process during their execution. In this case it is possible that some cluster nodes become overloaded. To improve performance we can integrate a dynamic data distribution algorithm.The integration of a dynamic load distribution policy into an application must consider the correct programming of several synchronisation/communication points in order to avoid dead-lock or data lost problems. In this work we show how a Model checking technique can be used to verify formally and automatically whether an application along with a load distribution algorithm work properly.We first propose a model for a parallel application that uses a dynamic load distribution policy to transfer its generated data to other processors (when there are some processors that can help with data processing). In our model in particular we defined a cyclic distribution policy. We also propose a set of functioning properties that our model and all parallel application that uses dynamic load distribution must fulfill. Then we apply a formal verification technique using the model checker spin to ensure that such properties are satisfied. To show an application of our model we used the MPI tool to implement it and solve the N-Queens problem, where milliards of possible solutions (data)are generated and processed. We show some results obtained by using a 16 processors system.