Operational Characterization of Weak Memory Consistency Models

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10793)

Abstract

To improve their overall performance, all current multicore and multiprocessor systems are based on memory architectures that allow behaviors that do not exist in interleaved (sequential) memory systems. The possible behaviors of such systems can be described by so-called weak memory consistency models. Several of these models have been introduced so far, and different ways to specify these models have been considered like axiomatic or view-based formalizations which have their particular advantages and disadvantages. In this paper, we propose the use of operational/architectural models to describe the semantics of weak memory consistency models in an operational, i.e., executable way. The operational semantics allow a more intuitive understanding of the possible behaviors and clearly point out the differences of these models. Furthermore, they can be used for simulation, formal verification, and even to automatically synthesize such memory systems.

Keywords

Memory models Weak memory consistency Processor architecture Memory architecture 

References

  1. 1.
    Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. IEEE Comput. 29(12), 66–76 (1996)CrossRefGoogle Scholar
  2. 2.
    Adve, S., Hill, M.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst. (TPDS) 4(6), 613–624 (1993)CrossRefGoogle Scholar
  3. 3.
    Ahamad, M., Bazzi, R., John, R., Kohli, P., Neiger, G.: The power of processor consistency. In: Snyder, L. (ed.) Symposium on Parallel Algorithms and Architectures (SPAA), pp. 251–260. ACM, Velen (1993)Google Scholar
  4. 4.
    Alglave, J.: A formal hierarchy of weak memory models. Form. Methods Syst. Des. (FMSD) 41(2), 178–210 (2012)CrossRefMATHGoogle Scholar
  5. 5.
    Bataller, J., Bernabeu, J.: Synchronized DSM models. In: Lengauer, C., Griebl, M., Gorlatch, S. (eds.) Euro-Par 1997. LNCS, vol. 1300, pp. 468–475. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0002771 CrossRefGoogle Scholar
  6. 6.
    Bruni, R., Montanari, U.: Models of Computation. Texts in Theoretical Computer Science. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-42900-7 CrossRefGoogle Scholar
  7. 7.
    Flur, S., Gray, K., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., Sewell, P.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Principles of Programming Languages (POPL), pp. 608–621. ACM (2016)Google Scholar
  8. 8.
    Furbach, F., Meyer, R., Schneider, K., Senftleben, M.: Memory model-aware testing - a unified complexity analysis. In: Application of Concurrency to System Design (ACSD), pp. 92–101. IEEE Computer Society, Tunis La Marsa (2014)Google Scholar
  9. 9.
    Furbach, F., Meyer, R., Schneider, K., Senftleben, M.: Memory-model-aware testing – a unified complexity analysis. Trans. Embed. Comput. Syst. (TECS) 14(4), 63:1–63:25 (2015)Google Scholar
  10. 10.
    Goodman, J.: Cache consistency and sequential consistency. Technical report 1006, Computer Sciences Department, University of Wisconsin-Madison, February 1991Google Scholar
  11. 11.
    Heddaya, A., Sinha, H.: Coherence, non-coherence and local consistency in distributed shared memory for parallel computing. Technical report BU-CS-92-004, Department of Computer Science, Boston University (1992)Google Scholar
  12. 12.
    Hennessy, J., Patterson, D.: Computer Architecture: A Quantitative Approach, 3rd edn. Morgan Kaufmann, Burlington (2003)MATHGoogle Scholar
  13. 13.
    Higham, L., Kawash, J., Verwaal, N.: Weak memory consistency models - part I: definitions and comparisons. Technical report 98/612/03, Department of Computer Science, University of Calgary (1998)Google Scholar
  14. 14.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. (T-C) 28(9), 690–691 (1979)CrossRefMATHGoogle Scholar
  15. 15.
    Lawrence, R.: A survey of cache coherence mechanisms in shared memory multiprocessors (1998)Google Scholar
  16. 16.
    Lipton, R., Sandberg, J.: PRAM: a scalable shared memory. Technical report CS-TR-180-88, Princeton University (1988)Google Scholar
  17. 17.
    Lipton, R., Sandberg, J.: Oblivious memory computer networking. Patent US 5276806, January 1994Google Scholar
  18. 18.
    Mador-Haim, S., et al.: 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).  https://doi.org/10.1007/978-3-642-31424-7_36 CrossRefGoogle Scholar
  19. 19.
    McKenney, P.: Memory barriers: a hardware view for software hackers, June 2010. http://www.rdrop.com/users/paulmck
  20. 20.
    Mosberger, D.: Memory consistency models. ACM SIGOPS: Oper. Syst. Rev. 27(1), 18–26 (1993)CrossRefGoogle Scholar
  21. 21.
    Mosberger, D.: Memory consistency models. Technical report TR 93/11, Department of Computer Science, The University of Arizona, Tucson, Arizona, USA (1993)Google Scholar
  22. 22.
    Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03359-9_27 CrossRefGoogle Scholar
  23. 23.
    Schneider, K.: The synchronous programming language Quartz. Internal report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, December 2009Google Scholar
  24. 24.
    Senftleben, M.: Operational characterization of weak memory consistency models. Master’s thesis, Department of Computer Science, University of Kaiserslautern, Germany, March 2013Google Scholar
  25. 25.
    Senftleben, M., Schneider, K.: Specifying weak memory consistency with temporal logic. In: Ghazel, M., Jmaiel, M. (eds.) Verification and Evaluation of Computer and Communication Systems (VECoS). CEUR Workshop Proceedings, vol. 1689, pp. 107–122. Sun SITE Central Europe, Tunis (2016). http://ceur-ws.org/Vol-1689/
  26. 26.
    Sindhu, P., Frailong, J.M., Cekleov, M.: Formal specification of memory models. In: Dubois, M., Thakkar, S. (eds.) Scalable Shared Memory Multiprocessors, pp. 25–41. Kluwer, Dordrecht (1992)CrossRefGoogle Scholar
  27. 27.
    Steinke, R., Nutt, G.: A unified theory of shared memory consistency. J. ACM (JACM) 51(5), 800–849 (2004)MathSciNetCrossRefMATHGoogle Scholar
  28. 28.
    Weaver, D., Germond, T. (eds.): The SPARC Architecture Manual-Version 9. Prentice-Hall Inc., Upper Saddle River (1994)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.TU KaiserslauternKaiserslauternGermany

Personalised recommendations