Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 3/2013

01.05.2013 | Original Article

Verifying a simplification of mutual exclusion by Lycklama–Hadzilacos

verfasst von: Wim H. Hesselink

Erschienen in: Acta Informatica | Ausgabe 3/2013

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

A simplification of the mutual exclusion algorithm of Lycklama and Hadzilacos (ACM Trans Program Lang Syst 13:558–576, 1991) is presented. It uses only four nonatomic shared bits per thread to guarantee mutual exclusion with the first-come-first-served property. The algorithm is verified by assertional methods, aided by the proof assistant PVS. A variation with five bits per thread is also given. This variation may give better performance when the number of threads is large. The use of the proof assistant made it easy to transfer the proof of the main algorithm to the variation.
Vorheriger Artikel Conjunctive grammars and alternating pushdown automata

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Literatur
Abraham, U.: Bakery algorithms. In: Proceedings of the Concurrency, Specification, and Programming, Workshop, pp. 7–40 (1993)
Anderson, J.H., Kim, Y.J., Herman, T.: Shared-memory mutual exclusion: major research trends since 1986. Discret. Comput. 16, 75–110 (2003)
Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison Wesley, Reading (2000)
Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Springer, New York (2009)MATHCrossRef
Burns, J.E.: Complexity of Communication Among Asynchronous Parallel Processes. Ph.D. Thesis, School of Information and Computer Science, Georgia Institute of Technology (1981)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification, Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)MATH
Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8, 569 (1965)CrossRef
Dijkstra, E.W.: Co-operating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43–112. NATO Advanced Study Institute, Academic Press, London (1968)
Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17, 643–644 (1974)MATHCrossRef
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)MATH
Doherty, S., Herlihy, M., Luchangco, V., Moir, M.: Bringing practical lock-free synchronization to 64-bit applications. In: Proceedings of the 23rd Annual ACM Symposium on Principles of Distributed Computing, pp. 31–39. ACM Press, New York, NY, USA (2004)
Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distr. Comput. 17, 21–42 (2005)CrossRef
Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free parallel and concurrent garbage collection by mark &sweep. Sci. Comput. Program. 64, 341–374 (2007)MathSciNetMATHCrossRef
Haldar, S., Vitanyi, P.: Bounded concurrent timestamp systems using vector clocks. J. ACM 49, 101–126 (2002)MathSciNetCrossRef
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, San Francisco (2008)
Hesselink, W.H.: Wait-free linearization with a mechanical proof. Distr. Comput. 9, 21–36 (1995)CrossRef
Hesselink, W.H.: A mechanical proof of Segall’s PIF algorithm. Formal Aspects Comput. 9, 208–226 (1997)MATHCrossRef
Hesselink, W.H.: The verified incremental design of a distributed spanning tree algorithm: extended abstract. Formal Aspects Comput. 11, 45–55 (1999)MATHCrossRef
Hesselink, W.H.: Using eternity variables to specify and prove a serializable database interface. Sci. Comput. Program. 51, 47–85 (2004)MathSciNetMATHCrossRef
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–583 (1969)MATHCrossRef
Holzmann, G.J.: The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2004)
Inoue, T., Hironaka, T., Sasaki, T., Fukae, S., Koide, T., Mattausch, H.J.: Evaluation of bank-based multiport memory architecture with blocking network. Electron. Commun. Japan 89, 498–510 (2006)CrossRef
Jayanti, P., Petrovic, S.: Efficient and practical constructions of LL/SC variables. In: PODC ’03: Proceedings of the twenty-second annual symposium on Principles of Distributed Computing, pp. 285–294. ACM Press, New York, NY, USA (2003)
Jayanti, P., Petrovic, S.: Efficient wait-free implementation of multiword LL/SC variables. In: Proceedings of the 25th IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 59–68. IEEE (2005)
Jayanti, P., Tan, K., Friedland, G., Katz, A.: Bounding Lamport’s Bakery algorithm. In: Proceedings of the SOFSEM, vol. 2234. LNCS, pp. 261–270 (2001)
Kim, Y.J., Anderson, J.H.: Nonatomic mutual exclusion with local spinning. Distr. Comput. 19, 19–61 (2006)CrossRef
Ladkin, P., Lamport, L., Olivier, B., Roegel, D.: Lazy caching in TLA. Distr. Comput. 12, 151–174 (1999)CrossRef
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3 2, 125–143 (1977)MathSciNetCrossRef
Lamport, L.: A new approach to proving the correctness of multiprocess programs. ACM Trans. Program. Lang. Syst. 1, 84–97 (1979)MATHCrossRef
Lamport, L.: The mutual exclusion problem—part I: a theory of interprocess communication, part II: statement and solutions. J. ACM 33, 313–348 (1986)MathSciNetMATHCrossRef
Lamport, L.: On interprocess communication. Parts I and II. Distr. Comput. 1, 77–101 (1986)MATHCrossRef
Lamport, L.: Win and sin: predicate transformers for concurrency. ACM Trans. Program. Lang. Syst. 12, 396–428 (1990)CrossRef
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 872–923 (1994)CrossRef
Lamport, L.: Composition: a way to make proofs harder. In: de Roever, W.-P., Pnueli, H. (eds.) Compositionality: The Significant Difference, vol. 1536. LNCS, pp. 402–423. Springer, Berlin (1997)
Lycklama, E.A., Hadzilacos, V.: A first-come-first-served mutual-exclusion algorithm with small communication variables. ACM Trans. Program. Lang. Syst. 13, 558–576 (1991)CrossRef
Lynch, N.A.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)MATH
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)CrossRef
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, New York (1995)CrossRef
Michael, M.M.: Practical lock-free and wait-free LL/SC/VL implementations using 64-bit CAS. In: Guerraoui, R. (ed.) 18th International Symposium on Distributed Computing, vol. 3274. LNCS, pp. 144–158 (2004)
Michael, M.M.: Scalable lock-free dynamic memory allocation. In: Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 35–46 (2004)
Raynal, M.: Algorithms for Mutual Exclusion. MIT Press, Cambridge (1986)MATH
Rusinoff, D.M.: A mechanically verified incremental garbage collector. Formal Aspects Comput. 6, 359–390 (1994)CrossRef
Shiue, W.-T., Chakrabarti, C.: Multi-module multi-port memory design for low power embedded systems. Des. Autom. Embed. Syst. 9, 235–261 (2004)CrossRef
Sundell, H., Tsigas, P.: Scalable and lock-free concurrent dictionaries. In: Proceedings of the 2004 ACM Symposium on Applied Computing, pp. 1438–1445. ACM Press (2004)
Takamura, M., Igarashi, Y.: Simple mutual exclusion algorithms based on bounded tickets on the asynchronous shared memory model. In: Proceedings of the COCOON, vol. 2387. LNCS, pp. 259–268 (2002)
Taubenfeld, G.: The black-white bakery algorithm and related bounded-space, adaptive, local-spinning and FIFO algorithms. In: Proceedings of the DISC, vol. 3274. LNCS, pp. 56–70 (2004)
Taubenfeld, G.: Synchronization Algorithms and Concurrent Programming. Pearson Education/Prentice Hall, London (2006)
Tel, G.: Distributed Algorithms. Cambridge University Press, Cambridge (1994)CrossRef
Vijayaraghavan, S.: A variant of the bakery algorithm with bounded values as a solution to Abraham’s concurrent programming problem. In: Proceedings of the Design, Analysis and Simulation of Distributed Systems (2003)
Welch, J., Lamport, L., Lynch, N.A.: A lattice-structured proof technique applied to a minimum-weight spanning tree algorithm. In: Proceedings 7th ACM Symposium on Principles of, Distributed Computing (1988)
Woo, T.-K.: A note on Lamport’s mutual exclusion algorithm. SIGOPS Oper. Syst. Rev. 24(4), 78–81 (1990)CrossRef
Zuo, W., Qi, Z., Jiaxing, L.: An intelligent multi-port memory. In: Proceedings of the IEEE International Symposium on Information Technology Application Workshops, pp. 251–254 (2008)
Metadaten
Titel
Verifying a simplification of mutual exclusion by Lycklama–Hadzilacos
verfasst von
Wim H. Hesselink
Publikationsdatum
01.05.2013
Verlag
Springer-Verlag
Erschienen in
Acta Informatica / Ausgabe 3/2013
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-013-0178-2