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

Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models

verfasst von : Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda, Kousuke Matsumoto

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

Software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons for state explosion in model checking with multiple memory consistency models, provides some optimizations intended to mitigate the problem, and applies them to McSPIN, a model checker for memory consistency models that we are developing. The effects of the optimizations and the usefulness of McSPIN are demonstrated experimentally by verifying copying protocols of concurrent copying garbage collection algorithms. To the best of our knowledge, this is the first model checking of the concurrent copying protocols under relaxed memory consistency models.

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 Computing Specification-Sensitive Abstractions for Program Verification
Nächstes Kapitel Identifying XML Schema Constraints Using Temporal Logic
Literatur
1.
Abe, T., Maeda, T.: Model checking with user-definable memory consistency models. In: Proceedings of PGAS, short paper, pp. 225–230 (2013)
2.
Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. In: Proceedings of HIPS, pp. 332–341 (2014)
3.
Abe, T., Maeda, T.: Optimization of a general model checking framework for various memory consistency models. In: Proceedings of PGAS (2014)
4.
Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. J. Inform. Process. (2016, to appear)
5.
Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. Int. J. Softw. Tools Technol. Transf. (2016, to appear)
6.
Abe, T., Maeda, T.: Observation-based concurrent program logic for relaxed memory consistency models. In: Proceedings of APLAS (2016, to appear)
7.
Abe, T., Maeda, T., Sato, M.: Model checking with user-definable abstraction for partitioned global address space languages. In: Proceedings of PGAS (2012)
8.
Abe, T., Maeda, T., Sato, M.: Model checking stencil computations written in a partitioned global address space language. In: Proceedings of HIPS, pp. 365–374 (2013)
9.
10.
Abe, T., Ugawa, T., Maeda, T., Matsumoto, K.: Reducing state explosion for software model checking with relaxed memory consistency models (2016). arXiv:​1608.​05893
11.
Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66–76 (1996)CrossRef
12.
Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of PLDI, pp. 68–78 (2008)
13.
Cavada, R., Cimatti, A., Jochim, C.A., Olivetti, G.K.E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV User Manual. 2.5 edn. (2002)
14.
Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 84–104. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38856-9_​7 CrossRef
15.
Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Proceedings of POPL, pp. 70–83 (1994)
16.
17.
Gammie, P., Hosking, T., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Proceedings of PLDI, pp. 99–109 (2015)
18.
19.
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)
20.
Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. Softw. Eng. 28(4), 364–377 (2002)CrossRef
21.
IBM: PowerPC Architechture Book, Version 2.02 (2005)
22.
Intel: A Formal Specification of Intel Itanium Processor Family Memory Ordering (2002)
23.
Intel: Intel 64 and IA-32 Architectures Software Developer’s Manual (2016)
24.
ISO/IEC 14882: 2011: Programming Language C++ (2011)
25.
Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36(5), 65–71 (2008)CrossRef
26.
Kroening, D., Tautschnig, M.: CBMC – C bounded model checker (Competition Contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54862-8_​26 CrossRef
27.
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
28.
Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-16164-3_​16 CrossRef
29.
Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in relaxed memory systems. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 144–160. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22306-8_​10 CrossRef
30.
Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 339–353. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-36742-7_​24 CrossRef
31.
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL, pp. 378–391 (2005)
32.
McCloskey, B., Bacon, D.F., Cheng, P., Grove, D.: Staccato: a parallel and concurrent real-time compacting garbage collector for multiprocessors. Report RC24504, IBM (2008)
33.
Oracle: The Java Language Specification. Java SE 8 edn. (2015)
34.
Pizlo, F., Frampton, D., Petrank, E., Steensgaard, B.: Stopless: a real-time garbage collector for multiprocessors. In: Proceedings of ISMM, pp. 159–172 (2007)
35.
Pizlo, F., Petrank, E., Steensgaard, B.: A study of concurrent real-time garbage collectors. In: Proceedings of PLDI, pp. 33–44 (2008)
36.
37.
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of PLDI, pp. 175–186 (2011)
38.
SPARC International Inc: The SPARC Architecture Manual, Version 9 (1994)
39.
40.
The UPC Consortium: UPC Language Specifications Version 1.3 (2013)
41.
Travkin, O., Mütze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311–326. Springer, Heidelberg (2013). doi:10.​1007/​978-3-319-03077-7_​21 CrossRef
42.
Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: Proceedings of OOPSLA, pp. 867–884 (2013)
Metadaten
Titel
Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
verfasst von
Tatsuya Abe
Tomoharu Ugawa
Toshiyuki Maeda
Kousuke Matsumoto
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_8