Advertisement

Operational Semantics of a Weak Memory Model with Channel Synchronization

  • Daniel Schnetzer Fava
  • Martin Steffen
  • Volker Stolz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, such models must be lax enough to account for hardware and compiler optimizations; on the other, the more lax the model, the harder it is to understand and program for. Though the right balance is up for debate, a memory model should provide what is known as the SC-DRF guarantee, meaning that data-race free programs behave in a sequentially consistent manner.

We present a weak memory model for a calculus inspired by the Go programming language. Thus, different from previous approaches, we focus on a memory model with buffered channel communication as the sole synchronization primitive. We formalize our model via an operational semantics, which allows us to prove the SC-DRF guarantee using a standard simulation technique. Contrasting against an axiomatic semantics, where the notion of a program is abstracted away as a graph with memory events as nodes, we believe our semantics and simulation proof can be clearer and easier to understand. Finally, we provide a concrete implementation in \(\mathbb {K}\), a rewrite-based executable semantic framework, and derive an interpreter for the proposed language.

References

  1. 1.
    Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Research Report 95/7, Digital WRL (1995)Google Scholar
  2. 2.
    Adve, S.V., Hill, M.D.: Weak ordering—a new definition. SIGARCH Comput. Archit. News 18(3a), 2–14 (1990)CrossRefGoogle Scholar
  3. 3.
    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 (2014)CrossRefGoogle Scholar
  4. 4.
    Abd Alrahman, Y., Andric, M., Beggiato, A., Lafuente, A.L.: Can we efficiently check concurrent programs under relaxed memory models in Maude? In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 21–41. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-12904-4_2CrossRefGoogle Scholar
  5. 5.
    Aspinall, D., Ševčík, J.: Java memory model examples: good, bad and ugly. In: Proceedings of VAMP, vol. 7 (2007)Google Scholar
  6. 6.
    Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283–307. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46669-8_12CrossRefGoogle Scholar
  7. 7.
    Becker: Programming languages — C++. ISO/IEC 14882:2001 (2011)Google Scholar
  8. 8.
    Boehm, H.-J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM (2008)Google Scholar
  9. 9.
    Boehm, H.-J., Demsky, B.: Outlawing ghosts: avoiding out-of-thin-air results. In: Proceedings of the Workshop on Memory Systems Performance and Correctness, MSPC 2014, pp. 7:1–7:6. ACM, New York (2014)Google Scholar
  10. 10.
    Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proceedings of POPL 2009, pp. 392–403. ACM (2009)CrossRefGoogle Scholar
  11. 11.
    Castagna, G., Gordon, A.D. (eds.): 44th Symposium on Principles of Programming Languages (POPL). ACM (2017)Google Scholar
  12. 12.
    Demange, D., Laporte, V., Zhao, L., Jagannathan, S., Pichardie, D., Vitek, J.: Plan B: a buffered memory model for Java. In: Proceedings of POPL 2013, pp. 329–342. ACM (2013)CrossRefGoogle Scholar
  13. 13.
    Donovan, A.A.A., Kernighan, B.W.: The Go Programming Language. Addison-Wesley, Boston (2015)Google Scholar
  14. 14.
    Fava, D.: Operational semantics of a weak memory model with channel synchronization (2017). https://github.com/dfava/mmgo
  15. 15.
    Fava, D., Steffen, M., Stolz, V.: Operational semantics of a weak memory model with channel synchronization: proof of sequential consistency for race-free programs. Technical report 477, University of Oslo, Faculty of Mathematics and Natural Sciences, Department of Informatics (2018). http://www.ifi.uio.no/~msteffen/download/18/oswmm-chan-rep.pdf
  16. 16.
    Flanagan, C., Freund, S.N.: Adversarial memory for detecting destructive races. In: Zorn, B., Aiken, A. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM (2010)Google Scholar
  17. 17.
    The Go programming language specification (2016). https://golang.org/ref/spec
  18. 18.
    The Go memory model (2014). https://golang.org/ref/mem. Version of 31 May 2014, covering Go version 1.9.1
  19. 19.
    Guerraoui, R., Henzinger, T.A., Singh, V.: Software transactional memory on relaxed memory models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 321–336. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_26CrossRefGoogle Scholar
  20. 20.
    Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)CrossRefGoogle Scholar
  21. 21.
    Jones, G., Goldsmith, M.: Programming in Occam2. Prentice-Hall International, Hemel Hampstead (1988)Google Scholar
  22. 22.
    The K framework (2017). http://www.kframework.org/
  23. 23.
    Kang, J., Hur, C., Lahav, O., Vafeiadis, V., and Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: [11], pp. 175–189 (2017)CrossRefGoogle Scholar
  24. 24.
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefGoogle Scholar
  25. 25.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C–28(9), 690–691 (1979)CrossRefGoogle Scholar
  26. 26.
    Lange, J., Ng, N., Toninho, B., and Yoshida, N.: Fencing off Go: liveness and safety for channel-based programming. In: [11] (2017)Google Scholar
  27. 27.
    Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL 2005. ACM (2005)Google Scholar
  28. 28.
    Maranget, L., Sarkar, S., Sewell, P.: A tutorial introduction to the ARM and POWER relaxed memory models (version 120) (2012)Google Scholar
  29. 29.
    Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the Second International Joint Conference on Artificial Intelligence, pp. 481–489. William Kaufmann, London (1971)Google Scholar
  30. 30.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I/II. Inf. Comput. 100, 1–77 (1992)CrossRefGoogle Scholar
  31. 31.
    Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous \(\pi \)-calculus. In: Proceedings of POPL 1997, pp. 256–265. ACM (1997)Google Scholar
  32. 32.
    Peters, K., Nestmann, U.: Is it a “good” encoding of mixed choice? In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 210–224. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28729-9_14CrossRefMATHGoogle Scholar
  33. 33.
    Pichon-Pharabod, J., Sewell, P.: A concurrency-semantics for relaxed atomics that permits optimisation and avoids out-of-thin-air executions. In: Proceedings of POPL 2016. ACM (2016)Google Scholar
  34. 34.
    Pugh, W.: Fixing the Java memory model. In: Proceedings of the ACM Java Grande Conference (1999)Google Scholar
  35. 35.
    Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Methods Program. 79(6), 397–434 (2010)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Steffen, M.: A small-step semantics of a concurrent calculus with goroutines and deferred functions. In: Ábrahám, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 393–406. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-30734-3_26CrossRefGoogle Scholar
  37. 37.
    Zhang, Y., Feng, X.: An operational happens-before memory model. Front. Comput. Sci. 10(1), 54–81 (2016)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Department of InformaticsUniversity of OsloOsloNorway
  2. 2.Western Norway University of Applied SciencesBergenNorway

Personalised recommendations