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:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Verification of Concurrent Programs on Weak Memory Models

verfasst von : Oleg Travkin, Heike Wehrheim

Erschienen in: Theoretical Aspects of Computing – ICTAC 2016

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Modern multi-core processors equipped with weak memory models seemingly reorder instructions (with respect to program order) due to built-in optimizations. For concurrent programs, weak memory models thereby produce interleaved executions which are impossible on sequentially consistent (SC) memory. Verification of concurrent programs consequently needs to take the memory model of the executing processor into account. This, however, makes most standard software verification tools inapplicable.
In this paper, we propose a technique (and present its accompanying tool Weak2SC) for reducing the verification problem for weak memory models to the verification on SC. The reduction proceeds by generating – out of a given program and weak memory model (here, TSO or PSO) – a new program containing all reorderings, thus already exhibiting the additional interleavings on SC. Our technique is compositional in the sense that program generation can be carried out on single processes without ever needing to inspect the state space of the concurrent program. We formally prove compositionality as well as soundness of our technique.
Weak2SC takes standard C programs as input and produces program descriptions which can be fed into automatic model checking tools (like SPIN) as well as into interactive provers (like KIV). Thereby, we allow for a wide range of verification options. We demonstrate the effectiveness of our technique by evaluating Weak2SC on a number of example programs, ranging from concurrent data structures to software transactional memory algorithms.

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
Nächstes Kapitel Petri Nets and Semilinear Sets (Extended Abstract)
Fußnoten
1
See T. Lane. Yes, waitlatch is vulnerable to weak-memory-ordering bugs, http://​www.​postgresql.​org/​message-id/​24241.​1312739269@sss.​pgh.​pa.​us, 2011, or D. Dice. A race in LockSupport park() arising from weak memory models, https://​blogs.​oracle.​com/​dave/​entry/​a_​race_​in_​locksupport_​park, 2009.
 
2
This restriction is of course lifted in our implementation.
 
4
Input to Spin can then be generated from a set of operations.
 
7
With the exception of max. 1 auxiliary variable per write in a loop.
 
Literatur
1.
2.
Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353–367. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​28
3.
Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 204–219. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28756-5_​15 CrossRef
4.
Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512–532. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-37036-6_​28 CrossRef
5.
Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39799-8_​9 CrossRef
6.
Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1–7:74 (2014)CrossRef
7.
Arora, N.S., Blumofe, R.D., Plaxton, C.G.: Thread scheduling for multiprogrammed multiprocessors. In: Proceedings of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1998, pp. 119–129. ACM, New York (1998)
8.
Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99–115. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​9 CrossRef
9.
Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 267–282. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46675-9_​18
10.
Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp. 12–21. ACM (2007)
11.
12.
Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 11–25. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-19835-9_​3 CrossRef
13.
Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. In: Dwyer, M.B., Tip, F. (eds.) ISSTA 2011, pp. 122–132. ACM (2011)
14.
Burns, J., Lynch, N.A.: Mutual exclusion using indivisible reads and writes. In: 18th Allerton Conference on Communication, Control, and Computing, pp. 833–842 (1980)
15.
Cohen, E., Schirmer, B.: From Total Store Order to Sequential Consistency: a practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 403–418. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14052-5_​28 CrossRef
16.
I. Corporate SPARC International. The SPARC architecture manual: version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1992)
17.
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)CrossRef
18.
Dalessandro, L., Dice, D., Scott, M., Shavit, N., Spear, M.: Transactional mutex locks. In: D’Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 2–13. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-15291-7_​2 CrossRef
19.
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
20.
Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Effective abstractions for verification under relaxed memory models. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 449–466. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46081-8_​25
21.
Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Institute, pp. 43–112. Academic Press, New York (1968)
22.
Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and VerifyThis competition. Softw. Tools Techn. Transfer 17(6), 1–18 (2014)
23.
Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)
24.
Intel, Santa Clara, CA, USA. Intel 64 and IA-32 Architectures Software Developer’s Manual Volume 3A: System Programming Guide, Part 1, May 2012
25.
Inverso, O., Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy-cseq: a context-bounded model checking tool for multi-threaded C-programs. In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, pp. 807–812. IEEE, 9–13 November 2015
26.
27.
Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. SIGACT News 43(2), 108–123 (2012)CrossRef
28.
29.
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)CrossRefMATH
30.
Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE/ACM International Symposium on Code Generation and Optimization (CGO 2004), San Jose, CA, USA, pp. 75–88. IEEE Computer Society, 20–24 March 2004
31.
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
32.
Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495–512. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31424-7_​36 CrossRef
33.
Meshman, Y., Rinetzky, N., Yahav, E.: Pattern-based synthesis of synchronization for the C++ memory model. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, pp. 120–127. IEEE, 27–30 September 2015
34.
Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)MATH
35.
Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (Relaxed Memory Order). In: SPAA, pp. 34–41 (1995)
36.
Peterson, G.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)CrossRefMATH
37.
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, pp. 46–57. IEEE Computer Society, 31 October–1 November 1977
38.
Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)CrossRef
39.
Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: Proceedings of the 2nd International Conference on Supercomputing, ICS 1988, pp. 621–626. ACM, New York (1988)
40.
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
41.
Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132–147. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-13338-6_​11
42.
Treiber, R.K.: Systems programming: coping with parallelism. Technical report RJ 5118, IBM Almaden Res. Ctr. (1986)
43.
44.
Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurrency Comput. Pract. Experience 17(5–6), 465–487 (2005)CrossRef
Metadaten
Titel
Verification of Concurrent Programs on Weak Memory Models
verfasst von
Oleg Travkin
Heike Wehrheim
Copyright-Jahr
2016
Buch
Theoretical Aspects of Computing – ICTAC 2016

Print ISBN: 978-3-319-46749-8

Electronic ISBN: 978-3-319-46750-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46750-4_1