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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Assuming that x and y are not aliases in the sense that they refer to the same or “overlapping” memory locations.
- 2.
The latter is indirectly clear already as we have established that \(\lfloor \rfloor \) preserves well-formedness under the assumption of race-freedom (Lemma 19).
References
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Research Report 95/7, Digital WRL (1995)
Adve, S.V., Hill, M.D.: Weak ordering—a new definition. SIGARCH Comput. Archit. News 18(3a), 2–14 (1990)
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)
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_2
Aspinall, D., Ševčík, J.: Java memory model examples: good, bad and ugly. In: Proceedings of VAMP, vol. 7 (2007)
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_12
Becker: Programming languages — C++. ISO/IEC 14882:2001 (2011)
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)
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)
Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proceedings of POPL 2009, pp. 392–403. ACM (2009)
Castagna, G., Gordon, A.D. (eds.): 44th Symposium on Principles of Programming Languages (POPL). ACM (2017)
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)
Donovan, A.A.A., Kernighan, B.W.: The Go Programming Language. Addison-Wesley, Boston (2015)
Fava, D.: Operational semantics of a weak memory model with channel synchronization (2017). https://github.com/dfava/mmgo
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
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)
The Go programming language specification (2016). https://golang.org/ref/spec
The Go memory model (2014). https://golang.org/ref/mem. Version of 31 May 2014, covering Go version 1.9.1
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_26
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
Jones, G., Goldsmith, M.: Programming in Occam2. Prentice-Hall International, Hemel Hampstead (1988)
The K framework (2017). http://www.kframework.org/
Kang, J., Hur, C., Lahav, O., Vafeiadis, V., and Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: [11], pp. 175–189 (2017)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C–28(9), 690–691 (1979)
Lange, J., Ng, N., Toninho, B., and Yoshida, N.: Fencing off Go: liveness and safety for channel-based programming. In: [11] (2017)
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL 2005. ACM (2005)
Maranget, L., Sarkar, S., Sewell, P.: A tutorial introduction to the ARM and POWER relaxed memory models (version 120) (2012)
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)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I/II. Inf. Comput. 100, 1–77 (1992)
Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous \(\pi \)-calculus. In: Proceedings of POPL 1997, pp. 256–265. ACM (1997)
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_14
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)
Pugh, W.: Fixing the Java memory model. In: Proceedings of the ACM Java Grande Conference (1999)
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Methods Program. 79(6), 397–434 (2010)
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_26
Zhang, Y., Feng, X.: An operational happens-before memory model. Front. Comput. Sci. 10(1), 54–81 (2016)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Fava, D.S., Steffen, M., Stolz, V. (2018). Operational Semantics of a Weak Memory Model with Channel Synchronization. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-95582-7_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95581-0
Online ISBN: 978-3-319-95582-7
eBook Packages: Computer ScienceComputer Science (R0)