nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

19.07.2016 | Regular Paper

A general model checking framework for various memory consistency models

verfasst von: Tatsuya Abe, Toshiyuki Maeda

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2017

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Relaxed memory consistency models are common and essential when multiple processes share a single global address space, such as when using multicore CPUs, distributed shared-memory programming languages, and so forth. Programming within these models is difficult and error prone, because of non-intuitive behaviors that could not occur in a strict consistency model. In addition, because the memory consistency models vary from language to language, and CPU to CPU, a program that may work correctly on one system may not work on another. To address the problem, this paper describes a model checking framework in which users are able to check their programs under various memory consistency models. More specifically, our framework provides a base model that exhibits very relaxed behaviors, and users are able to define various consistency models by adding constraints to the base model. This paper also describes McSPIN, a prototype implementation of a model checker based on the proposed framework. McSPIN can take a memory consistency model as an input, as well as a program and a property to be checked. We have specified the necessary constraints for three practical existing memory consistency models (Unified Parallel C, Coarray Fortran, and Itanium). McSPIN verified some example programs correctly, and confirmed the expected differences among the three models.

Vorheriger Artikel metaSMT: focus on your application and not on solver integration

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

In addition, McSPIN also supports a C-like language, provides high-level descriptions by if and while statements, and relieves us of using low-level descriptions by \(\texttt {Jump}\) in the modeling language.

Since the sample programs tell what are the UPC and Itanium MCMs, they contain programs that violate verified properties.

Abdulla, P.A., Atig, M.F., Chen, Y.F., Leonardsson, C., Rezine, A.: Automatic fence insertion in integer programs via predicate abstraction. In: Miné, A., Schmidt, D. (eds.) Static Analysis. LNCS, vol. 7460, pp. 164–180. Springer, Berlin (2012)CrossRef

Abdulla, P.A., Atig, M.F., Chen, Y.F., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 7795, pp. 530–536. Springer, Berlin (2013)CrossRef

Abe, T.: McSPIN. https://bitbucket.org/abet/mcspin/

Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. In: Proc. of HIPS, pp. 332–341 (2014)

Abe, T., Maeda, T.: Optimization of a general model checking framework for various memory consistency models. In: Proc. of PGAS (2014)

Abe, T., Maeda, T., Sato, M.: Model checking with user-definable abstraction for partitioned global address space languages. In: Proc. of PGAS (2012)

Abe, T., Maeda, T., Sato, M.: Model checking stencil computations written in a partitioned global address space language. In: Proc. of HIPS, pp. 365–374 (2013)

Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66–76 (1996)CrossRef

Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol. 7792, pp. 512–532. Springer, Berlin (2013)CrossRef

10.

Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. LNCS, vol. 8044, pp. 141–157. Springer, Berlin (2013)CrossRef

11.

Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. LNCS, vol. 6174, pp. 258–272. Springer, Berlin (2010)CrossRef

12.

Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Proc. of POPL, pp. 7–18 (2010)

13.

Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What’s decidable about weak memory models? In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 26–46. Springer, Berlin (2012)CrossRef

14.

Bacon, D., Bloch, J., Bogda, J., Click, C., Haahr, P., Lea, D., May, T., Maessen, J.W., Mitchell, J., Nilsen, K., et al.: The “double-checked locking is broken” declaration (2000)

15.

Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT 9(5–6), 505–525 (2007)

16.

Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)CrossRef

17.

Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1579, pp. 193–207. Springer, Berlin (1999)CrossRef

18.

Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol. 7792, pp. 533–553. Springer, Berlin (2013)CrossRef

19.

Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proc. of POPL, pp. 392–403 (2009)

20.

Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: Proc. of PLDI, pp. 12–21. ACM (2007)

21.

Clarke, E.M.: Counterexample-guided abstraction refinement. In: Proc. of TIME, p. 7 (2003)

22.

Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2988, pp. 168–176. Springer, Berlin (2004)CrossRef

23.

Crary, K., Sullivan, M.J.: A calculus for relaxed memory. In: Proc. of POPL, pp. 623–636 (2015)

24.

Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 84–104. Springer, Berlin (2013)CrossRef

25.

Ebnenasir, A.: UPC-SPIN: A framework for the model checking of upc programs. In: Proc. of PGAS. ACM (2011)

26.

Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) Programming Languages and Systems. LNCS, vol. 6012, pp. 267–286. Springer, Berlin (2010)CrossRef

27.

Gligoric, M., Mehlitz, P.C., Marinov, D.: X10X: Model checking a new programming language with an “old” model checker. In: Proc. of ICST, pp. 11–20 (2012)

28.

Haggar, P.: Practical java: programming language guide. Addison-Wesley, Menlo Park (2000)

29.

Holzmann, G.J.: The SPIN model checker. Addison-Wesley, Menlo Park (2003)

30.

Huynh, T., Roychoudhury, A.: A memory model sensitive checker for C#. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods. LNCS, vol. 4085, pp. 476–491. Springer, Berlin (2006)CrossRef

31.

Intel Corp.: A formal specification of intel itanium processor family memory ordering (2002)

32.

ISO/IEC 14882:2011: Programming Language C++ (2011)

33.

Jagadeesan, R., Pitcher, C., Riely, J.: Generative operational semantics for relaxed memory models. In: Gordon, A.D. (ed.) Programming Languages and Systems. LNCS, vol. 6012, pp. 307–326. Springer, Berlin (2010)CrossRef

34.

Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36(5), 65–71 (2008)

35.

Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 212–226. Springer, Berlin (2010)CrossRef

36.

Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in relaxed memory systems. In: Groce, A., Musuvathi, M. (eds.) Model Checking Software. LNCS, vol. 6823, pp. 144–160. Springer, Berlin (2011)

37.

Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 7795, pp. 339–353. Springer, Berlin (2013)CrossRef

38.

Mador-Haim, S., Alur, R., Martin, M.: Generating litmus tests for contrasting memory consistency models. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. LNCS, vol. 6174, pp. 273–287. Springer, Berlin (2010)CrossRef

39.

Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: Proc. of POPL, pp. 378–391 (2005)

40.

Pugh, W.: Causality test cases (2004). http://www.cs.umd.edu/pugh/java/memoryModel/CausalityTestCases.html

41.

Reid, J., Numrich, R.W.: Co-arrays in the next Fortran standard. Sci. Program. 15(1), 9–26 (2007)

42.

Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: Proc. of PPoPP, pp. 161–172 (2007)

43.

Shen, X., Arvind, Rudolph, L.: Commit-reconcile & fences (CRF): a new memory model for architects and compiler writers. In: Proc. of ISCA, pp. 150–161 (1999)

44.

Siegel, S.F.: Model checking nonblocking MPI programs. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 4349, pp. 44–58. Springer, Berlin (2007)CrossRef

45.

Steinke, R.C., Nutt, G.J.: A unified theory of shared memory consistency. J. ACM 51(5), 800–849 (2004)MathSciNetCrossRefMATH

46.

The UPC Consortium: UPC language specifications version 1.3 (2013)

47.

Travkin, O., Mütze, A.: SPIN as a linearizability checker under weak memory models. In: Proc. of Haifa Verification Conference, vol. 8244. Springer, Berlin, pp. 311–326 (2013)

48.

Vakkalanka, S.S., Sharma, S., Gopalakrishnan, G., Kirby, R.M.: ISP: a tool for model checking MPI programs. In: Proc. of PPoPP, pp. 285–286 (2008)

49.

XcalableMP Specification Working Group: XcalableMP application program interface version 1.2.1 (2014)

50.

Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) Formal Methods and Software Engineering. LNCS, vol. 3308, pp. 30–45. Springer, Berlin (2004)CrossRef

51.

Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurr. Comput. Pract. Exp. 17(5–6), 465–487 (2005)CrossRef

52.

Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos : A framework for axiomatic and executable specifications of memory consistency models. In: Proc. of IPDPS (2004)

Titel: A general model checking framework for various memory consistency models
verfasst von: Tatsuya Abe
Toshiyuki Maeda
Publikationsdatum: 19.07.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 5/2017
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-016-0429-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 5/2017

An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

metaSMT: focus on your application and not on solver integration

Advances in verification presented in TACAS’13

Flexible SAT-based framework for incremental bounded upgrade checking

Synthesis of circular compositional program proofs via abduction

Efficient family-based model checking via variability abstractions