SpringerLink
Log in

A Study of Shared-Memory Mutual Exclusion Protocols Using CADP

  • Conference paper
Formal Methods for Industrial Critical Systems (FMICS 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6371))

Abstract

Mutual exclusion protocols are an essential building block of concurrent systems: indeed, such a protocol is required whenever a shared resource has to be protected against concurrent non-atomic accesses. Hence, many variants of mutual exclusion protocols exist in the shared-memory setting, such as Peterson’s or Dekker’s well-known protocols. Although the functional correctness of these protocols has been studied extensively, relatively little attention has been paid to their non-functional aspects, such as their performance in the long run. In this paper, we report on experiments with the performance evaluation of mutual exclusion protocols using Interactive Markov Chains. Steady-state analysis provides an additional criterion for comparing protocols, which complements the verification of their functional properties. We also carefully re-examined the functional properties, whose accurate formulation as temporal logic formulas in the action-based setting turns out to be quite involved.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Anderson, J.H., Kim, Y.-J.: Adaptive mutual exclusion with local spinning. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 29–43. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Anderson, J.H., Kim, Y.-J., Herman, T.: Shared-memory mutual exclusion: major research trends since 1986. Distributed Computing 16, 75–110 (2003)

    Article  Google Scholar 

  3. Bar-David, Y., Taubenfeld, G.: Automatic discovery of mutual exclusion algorithms. In: Fich, F.E. (ed.) DISC 2003. LNCS, vol. 2848, pp. 136–150. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Botincan, M.: AsmL specification and verification of Lamport’s bakery algorithm. J. of Computing and Information Technology 13(4), 313–319 (2005)

    Article  Google Scholar 

  5. Burns, J.E., Lynch, N.A.: Mutual exclusion using indivisible reads and writes. In: Proc. of ACCCC’80, pp. 833–842 (1980)

    Google Scholar 

  6. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Lang, F., Serwe, W., Smeding, G.: Reference manual of the Lotos NT to Lotos translator (Version 5.0). INRIA/VASY, 107 pages (March 2010)

    Google Scholar 

  7. Chehaibar, G., Zidouni, M., Mateescu, R.: Modeling multiprocessor cache protocol impact on MPI performance. In: Proc. of QuEST’09. IEEE Press, Los Alamitos (2009)

    Google Scholar 

  8. Craig, T.S.: Building FIFO and priority-queuing spin locks from atomic swap. Technical Report 93-02-02, University of Washington, Seattle (February 1993)

    Google Scholar 

  9. Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Dijkstra, E.W.: Solution of a problem in concurrent programming control. ACM Commun. 8(9), 569–570 (1965)

    Article  Google Scholar 

  11. Dijkstra, E.W.: Co-operating sequential processes, pp. 43–112. Academic Press, New York (1968)

    Google Scholar 

  12. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proc. of LICS’86, pp. 267–278 (1986)

    Google Scholar 

  13. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)

    Article  MATH  Google Scholar 

  14. Garavel, H.: Open/Cæsar: an open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  15. Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410–429. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Proc. of FORTE’01, pp. 377–392 (2001)

    Google Scholar 

  17. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: a toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Garavel, H., Sighireanu, M.: Towards a second generation of FDTs – rationale for the design of E-LOTOS. In: Proc. of FMICS’98, pp. 187–230 (1998)

    Google Scholar 

  19. Hermanns, H. (ed.): Interactive Markov chains and the quest for quantified quality. LNCS, vol. 2428, p. 57. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  20. Hermanns, H., Joubert, C.: A set of performance and dependability analysis components for CADP. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 425–430. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Hermanns, H., Katoen, J.-P.: Performance evaluation:=(process algebra+model checking) Markov chains. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 59–81. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen, J.-P. (ed.) ARTS’99. LNCS, vol. 1601, pp. 244–265. Springer, Heidelberg (1999)

    Google Scholar 

  23. ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization, Genève (September 2001)

    Google Scholar 

  24. Jensen, H.E., Lynch, N.A.: A proof of Burns N-process mutual exclusion algorithm using abstraction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 409–423. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  25. Kessels, J.L.W.: Arbitration without common modifiable variables. Acta Informatica 17, 135–141 (1982)

    Article  MATH  Google Scholar 

  26. Knuth, D.E.: Additional comments on a problem in concurrent programming control. ACM Commun. 9(5), 321–322 (1966)

    Article  Google Scholar 

  27. Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5(1), 1–11 (1987)

    Article  Google Scholar 

  28. Magnusson, P.S., Landin, A., Hagersten, E.: Queue locks on cache coherent multiprocessors. In: Proc. of IPPS’94, pp. 165–171 (1994)

    Google Scholar 

  29. Manna, Z., Pnueli, A.: Tools and rules for the practicing verifier, pp. 125–159. ACM Press and Addison-Wesley (1991)

    Google Scholar 

  30. Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems, vol. I(specification). Springer, Heidelberg (1992)

    Book  MATH  Google Scholar 

  31. Mateescu, R.: CAESAR_SOLVE: a generic library for on-the-fly resolution of alternation-free boolean equation systems. STTT 8(1), 37–56 (2006)

    Article  Google Scholar 

  32. Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  33. Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Transactions on Computer Systems 9(1), 21–65 (1991)

    Article  Google Scholar 

  34. Nicola, R.D., Vaandrager, F.W.: Action versus state based logics for transition systems. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)

    Google Scholar 

  35. Peterson, G.L.: Myths about the mutual exclusion problem. IPL 12(3), 115–116 (1981)

    Article  MATH  Google Scholar 

  36. Puterman, M.L.: Markov decision processes: discrete stochastic dynamic programming. Wiley, Chichester (1994)

    Book  MATH  Google Scholar 

  37. Raynal, M.: Algorithmique du parallélisme : le problème de l’exclusion mutuelle. Dunod-Informatique, Paris (1984)

    Google Scholar 

  38. Shiryaev, A.: Probability. Springer, Heidelberg (1996)

    Book  MATH  Google Scholar 

  39. Streett, R.: Propositional dynamic logic of loo** and converse. Information and Control (54), 121–141 (1982)

    Google Scholar 

  40. Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: Proc. of ICSS’88, pp. 621–626 (1988)

    Google Scholar 

  41. Taubenfeld, G.: The black-white bakery algorithm and related bounded-space, adaptive, local-spinning and FIFO algorithms. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 56–70. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  42. Taubenfeld, G.: Synchronization algorithms and concurrent programming. Pearson, Prentice Hall (2006)

    Google Scholar 

  43. Yang, J.-H., Anderson, J.H.: A fast, scalable mutual exclusion algorithm. Distributed Computing 9(1), 51–60 (1995)

    Article  Google Scholar 

  44. Zhang, L., Neuhäußer, M.R.: Model checking interactive Markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 53–68. Springer, Heidelberg (2010)

    Google Scholar 

  45. Zhang, X., Yan, Y., Castaneda, R.: Evaluating and designing software mutual exclusion algorithms on shared-memory multiprocessors. IEEE Parallel Distributed Technology 4(1), 25–42 (1996)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria Grenoble – Rhône-Alpes, Inovallée, 655, av. de l’Europe, Montbonnot, F-38334, Saint Ismier, France

    Radu Mateescu & Wendelin Serwe

Authors
  1. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wendelin Serwe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Embedded Software Laboratory, RWTH Aachen, Ahornstr. 55, 52074, Aachen, Germany

    Stefan Kowalewski

  2. Fondazione Bruno Kessler — IRST, Via Sommarive 18, 38123, Povo (Trento), Italy

    Marco Roveri

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mateescu, R., Serwe, W. (2010). A Study of Shared-Memory Mutual Exclusion Protocols Using CADP. In: Kowalewski, S., Roveri, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2010. Lecture Notes in Computer Science, vol 6371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15898-8_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15898-8_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15897-1

  • Online ISBN: 978-3-642-15898-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation