{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T03:41:47Z","timestamp":1790480507509,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540745907","type":"print"},{"value":"9783540745914","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_4","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T10:49:52Z","timestamp":1187779792000},"page":"22-37","source":"Crossref","is-referenced-by-count":22,"title":["Formalising Java\u2019s Data Race Free Guarantee"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jaroslav","family":"\u0160ev\u010d\u00edk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","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. Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 378\u2013391. ACM Press, New York (2005)"},{"key":"4_CR2","series-title":"Java Series","first-page":"557","volume-title":"Java(TM) Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: Memory Model. In: Java(TM) Language Specification, 3rd edn. Java Series, pp. 557\u2013573. Addison-Wesley Professional, Reading (2005)","edition":"3"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: Operationally, denotationally, axiomatically. In: 16th ESOP (2007)","DOI":"10.1007\/978-3-540-71316-6_23"},{"issue":"12","key":"4_CR4","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"},{"issue":"6","key":"4_CR5","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(6), 445\u2013455 (2000)","journal-title":"Concurrency - Practice and Experience"},{"key":"4_CR6","volume-title":"Java Concurrency in Practice","author":"T. Peierls","year":"2005","unstructured":"Peierls, T., Goetz, B., Bloch, J., Bowbeer, J., Lea, D., Holmes, D.: Java Concurrency in Practice. Addison-Wesley Professional, Reading (2005)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Pugh, W., Manson, J.: Java memory model causality test cases (2004), http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/CausalityTestCases.html","DOI":"10.1145\/1040305.1040336"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. Special POPL Issue (submitted)","DOI":"10.1145\/1040305.1040336"},{"issue":"7","key":"4_CR9","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\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"4_CR10","unstructured":"Adve, S.: The SC- memory model for Java (2004), http:\/\/www.cs.uiuc.edu\/~sadve\/jmm"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual (2005), http:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf","DOI":"10.1007\/11542384_8"},{"issue":"6","key":"4_CR12","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1109\/71.242161","volume":"4","author":"S.V. Adve","year":"1993","unstructured":"Adve, S.V., Aggarwal, J.K.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst.\u00a04(6), 613\u2013624 (1993)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"4_CR13","unstructured":"Kawash, J.: Limitations and Capabilities of Weak Memory Consistency Systems. PhD thesis, The University of Calgary (2000)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-36103-0_44","volume-title":"Formal Methods and Software Engineering","author":"A. Roychoudhury","year":"2002","unstructured":"Roychoudhury, A.: Formal reasoning about hardware and software memory models. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol.\u00a02495, pp. 423\u2013434. Springer, Heidelberg (2002)"},{"key":"4_CR15","unstructured":"Bacon, D., et al.: The \u201cdouble-checked locking is broken\u201d declaration (2001), http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/DoubleCheckedLocking.html"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/353171.353172","volume-title":"OOPSLA","author":"J.W. Maessen","year":"2000","unstructured":"Maessen, J.W., Shen, X.: Improving the Java memory model using CRF. In: OOPSLA, pp. 1\u201312. ACM Press, New York (2000)"},{"key":"4_CR17","volume-title":"ACM 2007 SIGPLAN Conference on Principles and Practice of Parallel Computing","author":"V. Saraswat","year":"2007","unstructured":"Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: ACM 2007 SIGPLAN Conference on Principles and Practice of Parallel Computing, ACM, New York (2007)"},{"key":"4_CR18","unstructured":"Manson, J.: The Java memory model. PhD thesis, University of Maryland, College Park (2004)"},{"issue":"2-3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.tcs.2004.09.019","volume":"331","author":"E. \u00c1brah\u00e1m","year":"2005","unstructured":"\u00c1brah\u00e1m, E., de Boer, F.S., de Roever, W.P., Steffen, M.: An assertion-based proof system for multithreaded Java. TCS\u00a0331(2-3), 251\u2013290 (2005)","journal-title":"TCS"},{"issue":"1-3","key":"4_CR20","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci.\u00a0338(1-3), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/514188.514189","volume":"24","author":"J.S. Moore","year":"2002","unstructured":"Moore, J.S., Porter, G.: The apprentice challenge. ACM Trans. Program. Lang. Syst.\u00a024(3), 193\u2013216 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1145\/349299.349328","volume-title":"PLDI","author":"C. Flanagan","year":"2000","unstructured":"Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: PLDI, pp. 219\u2013232. ACM Press, New York (2000)"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/504282.504287","volume-title":"OOPSLA","author":"C. Boyapati","year":"2001","unstructured":"Boyapati, C., Rinard, M.: A parameterized type system for race-free Java programs. In: OOPSLA, pp. 56\u201369. ACM Press, New York (2001)"},{"key":"4_CR24","unstructured":"Huisman, M., Grigore, R., Haack, C., Hurlin, C., Kiniry, J., Petri, G., Poll, E.: Report on thread-modular verification. Mobius project deliverable D3.3 (2007), available from http:\/\/mobius.inria.fr"},{"key":"4_CR25","unstructured":"Microsoft: Standard ECMA-335 Common Language Infrastructure (CLI) (2005)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11817963_45","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2006","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded model checking of concurrent data types on relaxed memory models: A case study. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 489\u2013502. Springer, Heidelberg (2006)"},{"key":"4_CR27","volume-title":"PLDI","author":"S. Burckhardt","year":"2007","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI, San Diego, California, USA, ACM Press, New York (2007)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W.: Semantics of multithreaded Java. Technical Report CS-TR-4215, Dept. of Computer Science, University of Maryland, College Park (2001)","DOI":"10.1145\/376656.376806"},{"issue":"5-6","key":"4_CR29","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1002\/cpe.837","volume":"17","author":"Y. Yang","year":"2005","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability: Research articles. Concurr. Comput.: Pract. Exper.\u00a017(5-6), 465\u2013487 (2005)","journal-title":"Concurr. Comput.: Pract. Exper."},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/978-3-540-30482-1_11","volume-title":"Formal Methods and Software Engineering","author":"Y. Yang","year":"2004","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 30\u201345. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T17:38:23Z","timestamp":1683999503000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}