{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:17:06Z","timestamp":1762460226966,"version":"3.37.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319955810"},{"type":"electronic","value":"9783319955827"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-95582-7_15","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T10:31:17Z","timestamp":1531305077000},"page":"258-276","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Operational Semantics of a Weak Memory Model with Channel Synchronization"],"prefix":"10.1007","author":[{"given":"Daniel Schnetzer","family":"Fava","sequence":"first","affiliation":[]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Stolz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Research Report 95\/7, Digital WRL (1995)","DOI":"10.21236\/ADA638015"},{"issue":"3a","key":"15_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/325096.325100","volume":"18","author":"SV Adve","year":"1990","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering\u2014a new definition. SIGARCH Comput. Archit. News 18(3a), 2\u201314 (1990)","journal-title":"SIGARCH Comput. Archit. News"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"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)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-12904-4_2","volume-title":"Rewriting Logic and Its Applications","author":"Y Abd Alrahman","year":"2014","unstructured":"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\u201341. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_2"},{"key":"15_CR5","unstructured":"Aspinall, D., \u0160ev\u010d\u00edk, J.: Java memory model examples: good, bad and ugly. In: Proceedings of VAMP, vol. 7 (2007)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-662-46669-8_12","volume-title":"Programming Languages and Systems","author":"M Batty","year":"2015","unstructured":"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\u2013307. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12"},{"key":"15_CR7","unstructured":"Becker: Programming languages \u2014 C++. ISO\/IEC 14882:2001 (2011)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/1375581.1375591"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"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\u20137:6. ACM, New York (2014)","DOI":"10.1145\/2618128.2618134"},{"issue":"1","key":"15_CR10","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1145\/1594834.1480930","volume":"44","author":"G\u00e9rard Boudol","year":"2009","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proceedings of POPL 2009, pp. 392\u2013403. ACM (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR11","unstructured":"Castagna, G., Gordon, A.D. (eds.): 44th Symposium on Principles of Programming Languages (POPL). ACM (2017)"},{"issue":"1","key":"15_CR12","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1145\/2480359.2429110","volume":"48","author":"Delphine Demange","year":"2013","unstructured":"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\u2013342. ACM (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR13","volume-title":"The Go Programming Language","author":"AAA Donovan","year":"2015","unstructured":"Donovan, A.A.A., Kernighan, B.W.: The Go Programming Language. Addison-Wesley, Boston (2015)"},{"key":"15_CR14","unstructured":"Fava, D.: Operational semantics of a weak memory model with channel synchronization (2017). https:\/\/github.com\/dfava\/mmgo"},{"key":"15_CR15","unstructured":"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"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/1806596.1806625"},{"key":"15_CR17","unstructured":"The Go programming language specification (2016). https:\/\/golang.org\/ref\/spec"},{"key":"15_CR18","unstructured":"The Go memory model (2014). https:\/\/golang.org\/ref\/mem . Version of 31 May 2014, covering Go version 1.9.1"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-02658-4_26","volume-title":"Computer Aided Verification","author":"R Guerraoui","year":"2009","unstructured":"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\u2013336. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_26"},{"issue":"8","key":"15_CR20","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"15_CR21","volume-title":"Programming in Occam2","author":"G Jones","year":"1988","unstructured":"Jones, G., Goldsmith, M.: Programming in Occam2. Prentice-Hall International, Hemel Hampstead (1988)"},{"key":"15_CR22","unstructured":"The K framework (2017). http:\/\/www.kframework.org\/"},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/3093333.3009850","volume":"52","author":"Jeehoon Kang","year":"2017","unstructured":"Kang, J., Hur, C., Lahav, O., Vafeiadis, V., and Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: [11], pp. 175\u2013189 (2017)","journal-title":"ACM SIGPLAN Notices"},{"issue":"7","key":"15_CR24","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"issue":"9","key":"15_CR25","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C\u201328","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C\u201328(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Lange, J., Ng, N., Toninho, B., and Yoshida, N.: Fencing off Go: liveness and safety for channel-based programming. In: [11] (2017)","DOI":"10.1145\/3009837.3009847"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL 2005. ACM (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"15_CR28","unstructured":"Maranget, L., Sarkar, S., Sewell, P.: A tutorial introduction to the ARM and POWER relaxed memory models (version 120) (2012)"},{"key":"15_CR29","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the Second International Joint Conference on Artificial Intelligence, pp. 481\u2013489. William Kaufmann, London (1971)"},{"key":"15_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I\/II. Inf. Comput. 100, 1\u201377 (1992)","journal-title":"Inf. Comput."},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous $$\\pi $$\u03c0-calculus. In: Proceedings of POPL 1997, pp. 256\u2013265. ACM (1997)","DOI":"10.1145\/263699.263731"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-28729-9_14","volume-title":"Foundations of Software Science and Computational Structures","author":"K Peters","year":"2012","unstructured":"Peters, K., Nestmann, U.: Is it a \u201cgood\u201d encoding of mixed choice? In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 210\u2013224. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28729-9_14"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2837614.2837616"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Pugh, W.: Fixing the Java memory model. In: Proceedings of the ACM Java Grande Conference (1999)","DOI":"10.1145\/304065.304106"},{"issue":"6","key":"15_CR35","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Methods Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Logic Algebraic Methods Program."},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-30734-3_26","volume-title":"Theory and Practice of Formal Methods","author":"M Steffen","year":"2016","unstructured":"Steffen, M.: A small-step semantics of a concurrent calculus with goroutines and deferred functions. In: \u00c1brah\u00e1m, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 393\u2013406. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30734-3_26"},{"issue":"1","key":"15_CR37","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/s11704-015-4492-4","volume":"10","author":"Y Zhang","year":"2016","unstructured":"Zhang, Y., Feng, X.: An operational happens-before memory model. Front. Comput. Sci. 10(1), 54\u201381 (2016)","journal-title":"Front. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T12:29:33Z","timestamp":1571574573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}