Verification of a Hierarchical Generic Mutual Exclusion Algorithm

  • Souheib Baarir
  • Julien Sopena
  • Fabrice Legond-Aubry
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)


In distributed environments, the shared resources access control by mutual exclusion paradigm is a recurrent key problem. To cope with the new constraints implied by recently developed large scale distributed systems like grids, mutual exclusion algorithms become more and more complex and thus much harder to prove and/or verify. In this article, we propose the formal modeling and the verification of a new generic hierarchical approach. This approach is based on the composition of classical already proof checked distributed algorithms. It overcomes some limitations of these classical algorithms by taking into account the network topology latencies and have a high scalability where centralized ones don’t. We also have formalized the properties of the mutual exclusion paradigm in order to verify them against our solution. We prove that our compositional approach preserves theses properties under the assumption that all used plain algorithms assert them. This verification by formal method checkers was eased by the efficient use of already proved mutual exclusion algorithms and the reduction of state spaces by exploiting the symmetries.


distributed algorithm composition mutual exclusion grid computing colored Petri nets model checking 


  1. 1.
    Baarir, S., Haddad, S., Ilié, J.-M.: Exploiting Partial Symmetries in Well-formed nets for the Reachability and the Linear Time Model Checking Problems. In: Proceeding of IFAC Workshop on Discrete Event Systems, part of 7th CAAP, Reims - France. Springer, Heidelberg (2004)Google Scholar
  2. 2.
    Bertier, M., Arantes, L., Sens, P.: Distributed mutual exclusion algorithms for grid applications: A hierarchical approach. Journal of Parallel and Distributed Computing 66, 128–144 (2006)CrossRefzbMATHGoogle Scholar
  3. 3.
    Chang, I., Singhal, M., Liu, M.: A hybrid approach to mutual exclusion for distributed system. In: IEEE International Computer Software and Applications Conference, pp. 289–294 (1990)Google Scholar
  4. 4.
    Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed coloured nets for symmetric modelling applications. IEEE Transactions on Computers 42(11), 1343–1360 (1993)CrossRefGoogle Scholar
  5. 5.
    Dijkstra, E.W.: Solution of a problem in concurrent programming control. Comm. ACM 8(9), 569 (1965)CrossRefGoogle Scholar
  6. 6.
    Erciyes, K.: Distributed mutual exclusion algorithms on a ring of clusters. In: Laganá, A., Gavrilova, M.L., Kumar, V., Mun, Y., Tan, C.J.K., Gervasi, O. (eds.) ICCSA 2004. LNCS, vol. 3045, pp. 518–527. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Fu, S., Tzeng, N., Li, Z.: Empirical evaluation of distributed mutual exclusion algorithms. pp. 255–259Google Scholar
  8. 8.
    Housni, A., Trhel, M.: Distributed mutual exclusion by groups based on token and permission. In: International Conference on Computational Science and Its Applications, June 2001, pp. 26–29 (2001)Google Scholar
  9. 9.
    Jensen, K.: High-level petri nets. In: Pagnoni, A., Rozenberg, G. (eds.) Proceedings of the 3rd European Workshop on Application and Theory of Petri Nets, Varenna, Italy. Informatik - Fachberichte, vol. 66, pp. 166–180. Springer, Heidelberg (1983)CrossRefGoogle Scholar
  10. 10.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125–143 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)zbMATHGoogle Scholar
  12. 12.
    Madhuram, K.: A hybrid approach for mutual exclusion in distributed computing systems. In: IEEE Symposium on Parallel and Distributed Processing (1994)Google Scholar
  13. 13.
    Maekawa, M.: A \(\sqrt{N}\) algorithm for mutual exclusion in decentralized systems. ACM-Transactions on Computer Systems 3(2), 145–159 (1985)CrossRefGoogle Scholar
  14. 14.
    Martin, A.J.: Distributed mutual exclusion on a ring of processes. Sci. Comput. Program. 5(3), 265–276 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Mueller, F.: Prioritized token-based mutual exclusion for distributed systems. In: International Parallel Processing Symposium, March 1998, pp. 791–795 (1998)Google Scholar
  16. 16.
    Naimi, M., Trehel, M.: An improvement of the log(n) distributed algorithm for mutual exclusion. In: IEEE Intern. Conf. on Distributed Computing Systems, pp. 371–377 (1987)Google Scholar
  17. 17.
    Omara, F., Nabil, M.: A new hybrid algorithm for the mutual exclusion problem in the distributed systems. International Journal of Intelligent Computing and Information Sciences 2(2), 94–105 (2002)Google Scholar
  18. 18.
    Raymond, K.: A tree-based algorithm for distributed mutual exclusion. ACM Transactions on Computer Systems 7(1), 61–77 (1989)CrossRefGoogle Scholar
  19. 19.
    Ricart, G., Agrawala, A.: An optimal algorithm for mutual exclusion in computer networks. Communications of the ACM 24 (1981)Google Scholar
  20. 20.
    Singhal, M.: A dynamic information structure for mutual exclusion algorithm for distributed systems. IEEE Trans. on Parallel and Distributed Systems 3(1), 121–125 (1992)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Sopena, J., Legond-Aubry, F., Arantes, L., Sens, P.: A composition approach to mutual exclusion algorithms for grid applications. In: Proc. of the International Conference on Parallel Processing, p. 65 (2007)Google Scholar
  22. 22.
    Suzuki, I., Kasami, T.: A distributed mutual exclusion algorithm. ACM Transactions on Computer Systems 3(4), 344–349 (1985)CrossRefGoogle Scholar
  23. 23.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Souheib Baarir
    • 1
  • Julien Sopena
    • 2
  • Fabrice Legond-Aubry
    • 2
  1. 1.Department of Computer ScienceUniv. degli Studi del Piemonte OrientaleAlessandriaItaly
  2. 2.LIP6 - Université de Paris 6ParisFrance

Personalised recommendations