{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T01:40:16Z","timestamp":1769046016185,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119569","type":"print"},{"value":"9783642119576","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_17","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"307-326","source":"Crossref","is-referenced-by-count":34,"title":["Generative Operational Semantics for Relaxed Memory Models"],"prefix":"10.1007","author":[{"given":"Radha","family":"Jagadeesan","sequence":"first","affiliation":[]},{"given":"Corin","family":"Pitcher","sequence":"additional","affiliation":[]},{"given":"James","family":"Riely","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"12","key":"17_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-74591-4_4","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., Sevc\u00edk, J.: Formalising Java\u2019s data race free guarantee. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 22\u201337. Springer, Heidelberg (2007)"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1145\/1065010.1065042","volume-title":"PLDI 2005","author":"H.-J. Boehm","year":"2005","unstructured":"Boehm, H.-J.: Threads cannot be implemented as a library. In: PLDI 2005, pp. 261\u2013268. ACM, New York (2005)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI 2008, pp. 68\u201378 (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: POPL, pp. 392\u2013403 (2009)","DOI":"10.1145\/1594834.1480930"},{"issue":"4","key":"17_CR6","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10766-007-0051-4","volume":"35","author":"G. Bronevetsky","year":"2007","unstructured":"Bronevetsky, G., de Supinski, B.R.: Complete formal specification of the OpenMP memory model. Int. J. Parallel Program.\u00a035(4), 335\u2013392 (2007)","journal-title":"Int. J. Parallel Program."},{"key":"17_CR7","unstructured":"Burckhardt, S., Musuvath, M., Singh, V.: Verifying compiler transformations for concurrent programs. MSR-TR-2008-171 (2008)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-71316-6_23","volume-title":"Programming Languages and Systems","author":"P. Cenciarelli","year":"2007","unstructured":"Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: Operationally, denotationally, axiomatically. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 331\u2013346. Springer, Heidelberg (2007)"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/155090.155113","volume-title":"PLDI 1993","author":"C. Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI 1993, vol.\u00a028(6), pp. 237\u2013247. ACM Press, New York (1993)"},{"key":"17_CR10","first-page":"114","volume-title":"ISCA 2004","author":"S. Hangal","year":"2004","unstructured":"Hangal, S., Vahia, D., Manovit, C., Lu, J.-Y.J.: TSOtool: A program for verifying memory systems using the memory consistency model. In: ISCA 2004, p. 114. IEEE, Los Alamitos (2004)"},{"issue":"3","key":"17_CR11","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/503502.503505","volume":"23","author":"A. Igarashi","year":"2001","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Programming Languages and Systems\u00a023(3), 396\u2013450 (2001)","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"17_CR12","first-page":"15","volume-title":"SC","author":"A. Kamil","year":"2005","unstructured":"Kamil, A., Su, J., Yelick, K.A.: Making sequential consistency practical in Titanium. In: SC, p. 15. IEEE, Los Alamitos (2005)"},{"issue":"9","key":"17_CR13","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Trans. Comput.\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"17_CR14","unstructured":"Lea, D.: The JSR-133 cookbook for compiler writers (2008), http:\/\/gee.cs.oswego.edu\/dl\/jmm\/cookbook.html (Last modified: April 2008)"},{"key":"17_CR15","unstructured":"Luchangco, V.M.: Memory consistency models for high-performance distributed computing. PhD thesis, MIT (2001)"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1145\/1040305.1040336","volume-title":"POPL 2005","author":"J. Manson","year":"2005","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL 2005, pp. 378\u2013391. ACM Press, New York (2005)"},{"key":"17_CR17","unstructured":"Milner, R.: The polyadic pi-calculus: a tutorial. Technical report, Logic and Algebra of Specification (1991)"},{"key":"17_CR18","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-step Guide. Artima (2008)"},{"key":"17_CR19","unstructured":"Pugh, W.: Causality test cases (2004), http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/CausalityTestCases.html"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1007\/978-3-540-30502-6_36","volume-title":"Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making","author":"V.A. Saraswat","year":"2004","unstructured":"Saraswat, V.A.: Concurrent constraint-based memory machines: A framework for Java memory models. In: Maher, M.J. (ed.) ASIAN 2004. LNCS, vol.\u00a03321, pp. 494\u2013508. Springer, Heidelberg (2004)"},{"key":"17_CR21","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/1229428.1229469","volume-title":"PPOPP","author":"V.A. Saraswat","year":"2007","unstructured":"Saraswat, V.A., Jagadeesan, R., Michael, M.M., von Praun, C.: A theory of memory models. In: PPOPP, pp. 161\u2013172. ACM, New York (2007)"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: POPL, pp. 379\u2013391 (2009)","DOI":"10.1145\/1594834.1480929"},{"key":"17_CR23","unstructured":"Sevc\u00edk, J.: Program Transformations in Weak Memory Models. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh (2008)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-70592-5_3","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"J. Sevc\u00edk","year":"2008","unstructured":"Sevc\u00edk, J., Aspinall, D.: On validity of program transformations in the Java memory model. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 27\u201351. Springer, Heidelberg (2008)"},{"issue":"5","key":"17_CR25","doi-asserted-by":"publisher","first-page":"800","DOI":"10.1145\/1017460.1017464","volume":"51","author":"R.C. Steinke","year":"2004","unstructured":"Steinke, R.C., Nutt, G.J.: A unified theory of shared memory consistency. J. ACM\u00a051(5), 800\u2013849 (2004)","journal-title":"J. ACM"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Yelick, K., Bonachea, D., Wallace, C.: A proposal for a UPC memory consistency model, v1.1. Technical Report LBNL-54983, Lawrence Berkeley National Lab (2004)","DOI":"10.2172\/823757"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:42Z","timestamp":1606185942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}