{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:46:56Z","timestamp":1725670016457},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288685"},{"type":"electronic","value":"9783642288692"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_25","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"497-517","source":"Crossref","is-referenced-by-count":20,"title":["Java and the Java Memory Model \u2014 A Unified, Machine-Checked Formalisation"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"25_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S. Adve","year":"1996","unstructured":"Adve, S., Gharachaorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer\u00a029(12), 66\u201376 (1996)","journal-title":"IEEE Computer"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Adve, S., Hill, M.D.: Weak ordering - a new definition. In: ISCA 1990, pp. 2\u201314. ACM (1990)","DOI":"10.1145\/325096.325100"},{"key":"25_CR3","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/1787234.1787255","volume":"53","author":"S.V. Adve","year":"2010","unstructured":"Adve, S.V., Boehm, H.J.: Memory models: A case for rethinking parallel languages and hardware. Commun. ACM\u00a053, 90\u2013101 (2010)","journal-title":"Commun. ACM"},{"key":"25_CR4","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., \u0160ev\u010d\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":"25_CR5","doi-asserted-by":"crossref","unstructured":"Batty, M., Memarian, K., Owens, S., Sarkar, S., Sewell, P.: Clarifying and compiling C\/C++ concurrency: From C++11 to POWER. In: POPL 2012, pp. 509\u2013520. ACM (2012)","DOI":"10.1145\/2103621.2103717"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI 2008, pp. 68\u201378. ACM (2008)","DOI":"10.1145\/1375581.1375591"},{"issue":"4","key":"25_CR8","doi-asserted-by":"publisher","first-page":"33","DOI":"10.5381\/jot.2009.8.4.a2","volume":"8","author":"J. Boyland","year":"2009","unstructured":"Boyland, J.: An operational semantics including \u201cvolatile\u201d for safe concurrency. Journal of Object Technology\u00a08(4), 33\u201353 (2009); FTfJP 2008","journal-title":"Journal of Object Technology"},{"key":"25_CR9","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":"25_CR10","unstructured":"Gosling, J., Joy, B., Stelle, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley (2005)"},{"key":"25_CR11","unstructured":"Huisman, M., Petri, G.: The Java Memory Model: a formal explanation. In: VAMP 2007, pp. 81\u201396, Tech. Rep. ICIS-R07021, University of Nijmegen (2007)"},{"key":"25_CR12","unstructured":"International standard ISO\/IEC 14882:2011. programming languages \u2013 C++. International Organization for Standardization (2011)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-11957-6_17","volume-title":"Programming Languages and Systems","author":"R. Jagadeesan","year":"2010","unstructured":"Jagadeesan, R., Pitcher, C., Riely, J.: Generative Operational Semantics for Relaxed Memory Models. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 307\u2013326. Springer, Heidelberg (2010)"},{"issue":"4","key":"25_CR14","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"25_CR15","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 programs. IEEE Trans. Comput.\u00a028, 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"25_CR16","unstructured":"Lochbihler, A.: Type safe nondeterminism - a formal semantics of Java threads. In: Foundations of Object-Oriented Languages, FOOL 2008 (2008)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-11957-6_23","volume-title":"Programming Languages and Systems","author":"A. Lochbihler","year":"2010","unstructured":"Lochbihler, A.: Verifying a Compiler for Java Threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 427\u2013447. Springer, Heidelberg (2010)"},{"key":"25_CR18","unstructured":"Lochbihler, A.: Jinja with threads. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (2011), \n                  \n                    http:\/\/afp.sourceforge.net\/entries\/JinjaThreads.shtml\n                  \n                  \n                , formal proof development"},{"key":"25_CR19","unstructured":"Lochbihler, A.: A unified, machine-checked formalisation of Java and the Java Memory Model. Tech. Rep. 2011-34, Karlsruhe Reports in Informatics (2011)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-642-22863-6_17","volume-title":"Interactive Theorem Proving","author":"A. Lochbihler","year":"2011","unstructured":"Lochbihler, A., Bulwahn, L.: Animating the Formalised Semantics of a Java-Like Language. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 216\u2013232. Springer, Heidelberg (2011)"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model. In: POPL 2005, pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"25_CR23","unstructured":"Causality test cases for the Java memory model, \n                  \n                    http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/CausalityTestCases.html"},{"key":"25_CR24","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1002\/1096-9128(200005)12:6<445::AID-CPE484>3.0.CO;2-A","volume":"12","author":"W. Pugh","year":"2000","unstructured":"Pugh, W.: The Java memory model is fatally flawed. Concurrency: Practice and Experience\u00a012, 445\u2013455 (2000)","journal-title":"Concurrency: Practice and Experience"},{"key":"25_CR25","unstructured":"Quis custodiet, \n                  \n                    http:\/\/pp.info.uni-karlsruhe.de\/project.php?id=31"},{"key":"25_CR26","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. \u0160ev\u010d\u00edk","year":"2008","unstructured":"\u0160ev\u010d\u00edk, J., Aspinall, D.: On Validity of Program Transformations in the Java Memory Model. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 27\u201351. Springer, Heidelberg (2008)"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Nardelli, F., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL 2011. pp. 43\u201354. ACM (2011)","DOI":"10.1145\/1925844.1926393"},{"key":"25_CR28","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM\u00a053, 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Torlak, E., Vaziri, M., Dolby, J.: MemSAT: checking axiomatic specifications of memory models. In: PLDI 2010. pp. 341\u2013350. ACM (2010)","DOI":"10.1145\/1806596.1806635"}],"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-28869-2_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:13:42Z","timestamp":1620126822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}