Skip to main content
SpringerLink
Log in

Operational Characterization of Weak Memory Consistency Models

  • Conference paper
  • First Online:
Architecture of Computing Systems – ARCS 2018 (ARCS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10793))

Included in the following conference series:

  • 1596 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

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

    Article  Google Scholar 

  2. Adve, S., Hill, M.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst. (TPDS) 4(6), 613–624 (1993)

    Article  Google Scholar 

  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. Alglave, J.: A formal hierarchy of weak memory models. Form. Methods Syst. Des. (FMSD) 41(2), 178–210 (2012)

    Article  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Book  Google Scholar 

  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. 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. 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. Goodman, J.: Cache consistency and sequential consistency. Technical report 1006, Computer Sciences Department, University of Wisconsin-Madison, February 1991

    Google Scholar 

  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. Hennessy, J., Patterson, D.: Computer Architecture: A Quantitative Approach, 3rd edn. Morgan Kaufmann, Burlington (2003)

    MATH  Google Scholar 

  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. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. (T-C) 28(9), 690–691 (1979)

    Article  MATH  Google Scholar 

  15. Lawrence, R.: A survey of cache coherence mechanisms in shared memory multiprocessors (1998)

    Google Scholar 

  16. Lipton, R., Sandberg, J.: PRAM: a scalable shared memory. Technical report CS-TR-180-88, Princeton University (1988)

    Google Scholar 

  17. Lipton, R., Sandberg, J.: Oblivious memory computer networking. Patent US 5276806, January 1994

    Google Scholar 

  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

    Chapter  Google Scholar 

  19. McKenney, P.: Memory barriers: a hardware view for software hackers, June 2010. http://www.rdrop.com/users/paulmck

  20. Mosberger, D.: Memory consistency models. ACM SIGOPS: Oper. Syst. Rev. 27(1), 18–26 (1993)

    Article  Google Scholar 

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

    Chapter  Google Scholar 

  23. Schneider, K.: The synchronous programming language Quartz. Internal report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, December 2009

    Google Scholar 

  24. Senftleben, M.: Operational characterization of weak memory consistency models. Master’s thesis, Department of Computer Science, University of Kaiserslautern, Germany, March 2013

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  28. Weaver, D., Germond, T. (eds.): The SPARC Architecture Manual-Version 9. Prentice-Hall Inc., Upper Saddle River (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Kaiserslautern, 67653, Kaiserslautern, Germany

    M. Senftleben & K. Schneider

Authors
  1. M. Senftleben
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. K. Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to M. Senftleben .

Editor information

Editors and Affiliations

  1. Chair for Chip Design for Embedded Computing, Technische Universität Braunschweig, Braunschweig, Germany

    Mladen Berekovic

  2. Chair for Chip Design for Embedded Computing, Technische Universität Braunschweig, Braunschweig, Germany

    Rainer Buchty

  3. Institute of Computer Engineering, Universität zu Lübeck, Lübeck, Germany

    Heiko Hamann

  4. School of Computer Science, The University of Manchester, Manchester, United Kingdom

    Dirk Koch

  5. Institute for Information Technology and Communications, Otto-von-Guericke Universität Magdeburg, Magdeburg, Germany

    Thilo Pionteck

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Senftleben, M., Schneider, K. (2018). Operational Characterization of Weak Memory Consistency Models. In: Berekovic, M., Buchty, R., Hamann, H., Koch, D., Pionteck, T. (eds) Architecture of Computing Systems – ARCS 2018. ARCS 2018. Lecture Notes in Computer Science(), vol 10793. Springer, Cham. https://doi.org/10.1007/978-3-319-77610-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-77610-1_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-77609-5

  • Online ISBN: 978-3-319-77610-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation