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
Erschienen in:
Place Bisimulation and Liveness for Open Petri Nets Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Performance Evaluation of Concurrent Data Structures

verfasst von : Hao Wu, Xiaoxiao Yang, Joost-Pieter Katoen

Erschienen in: Dependable Software Engineering: Theories, Tools, and Applications

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

The speed-ups acquired by concurrent programming heavily rely on exploiting highly concurrent data structures. This has led to a variety of coarse-grained and fine-grained locking to lock-free data structures. The performance of such data structures is typically analysed by simulation or implementation. We advocate a model-based approach using probabilistic model checking. The main benefit is that our models can also be used to check the correctness of the data structures. The paper details the approach, and reports on experimental results on several concurrent stacks, queues, and lists. Our analysis yields worst- and best-case bounds on performance metrics such as expected time and probabilities to finish a certain number of operations within a deadline.

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 "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

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
Vorheriges Kapitel Divergence Detection for CCSL Specification via Clock Causality Chain
Nächstes Kapitel GPU-Accelerated Steady-State Computation of Large Probabilistic Boolean Networks
Fußnoten
1
The LNT language is a formal description technique standardized by ISO OSI (1989), please refer to: http://​www.​iso.​org/​iso/​catalogue_​detail.​htm?​csnumber=​16258.
 
3
The complete LNT models and their corresponding scripts of all aforementioned concurrent data structures follow the same principle described here and can be found under the link: https://​moves.​rwth-aachen.​de/​wp-content/​uploads/​LNT-models.​zip.
 
4
Thus, the thread behavior is not biased to certain scenarios.
 
5
In our experiments, we consider lists of natural numbers.
 
6
If for a given scenario, the number of states of a data structure is higher than for another data structure, it allows for more concurrency and has finer lock granularity.
 
Literatur
1.
Baier, C., Daum, M., Engel, B., Härtig, H., et al.: Locks: picking key methods for a scalable quantitative analysis. J. Comput. Syst. Sci. 81(1), 258–287 (2015)CrossRefMATH
2.
Cederman, D., Chatterjee, B., Tsigas, P.: Understanding the performance of concurrent data structures on graphics processors. In: Kaklamanis, C., Papatheodorou, T., Spirakis, P.G. (eds.) Euro-Par 2012. LNCS, vol. 7484, pp. 883–894. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-32820-6_​87 CrossRef
3.
4.
Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In: POPL, pp. 233–246. ACM (2015)
5.
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-30232-2_​7 CrossRef
6.
Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)
7.
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)CrossRefMATH
8.
Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. Log. Methods Comput. Sci. 10(3) (2014)
9.
Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168–184. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-11936-6_​13
10.
Heller, S., Herlihy, M., Luchangco, V., Moir, M., Scherer III, W.N., Shavit, N.: A lazy concurrent list-based set algorithm. Parallel Process. Lett. 17(4), 411–424 (2007)MathSciNetCrossRef
11.
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2008)
12.
Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843–861 (2013)CrossRef
13.
Michael, M.M.: Hazard pointers: safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst. 15(6), 491–504 (2004)CrossRef
14.
Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267–275. ACM (1996)
15.
Neuhäußer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412–427. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-74407-8_​28 CrossRef
16.
Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 239–255. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-23283-1_​16 CrossRef
Metadaten
Titel
Performance Evaluation of Concurrent Data Structures
verfasst von
Hao Wu
Xiaoxiao Yang
Joost-Pieter Katoen
Copyright-Jahr
2016
Buch
Dependable Software Engineering: Theories, Tools, and Applications

Print ISBN: 978-3-319-47676-6

Electronic ISBN: 978-3-319-47677-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-47677-3_3