{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T02:21:24Z","timestamp":1769048484993,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119699","type":"print"},{"value":"9783642119705","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11970-5_7","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:23:33Z","timestamp":1267989813000},"page":"104-123","source":"Crossref","is-referenced-by-count":33,"title":["Verifying Local Transformations on Relaxed Memory Models"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Burckhardt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Madanlal","family":"Musuvathi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasu","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"7_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S. Adve","year":"1996","unstructured":"Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"issue":"6","key":"7_CR2","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1109\/71.242161","volume":"4","author":"S. Adve","year":"1993","unstructured":"Adve, S., Hill, M.: 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":"7_CR3","doi-asserted-by":"crossref","unstructured":"Arvind, Maessen, J.-W.: Memory model = instruction reordering + store atomicity. In: ISCA, pp. 29\u201340 (2006)","DOI":"10.1145\/1150019.1136489"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Programming Language Design and Implementation (PLDI), pp. 68\u201378 (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Principles of Programming Languages, POPL (2009)","DOI":"10.1145\/1480881.1480930"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Brookes, S.: Full abstraction for a shared variable parallel language. In: LICS, pp. 98\u2013109 (1993)","DOI":"10.1109\/LICS.1993.287596"},{"key":"7_CR7","unstructured":"Brumme, C.: cbrumme\u2019s weblog, http:\/\/blogs.gotdotnet.com\/cbrumme\/archive\/2003\/05\/17\/51445.aspx"},{"key":"7_CR8","unstructured":"Burckhardt, S., Musuvathi, M., Singh, V.: Verification of compiler transformations for concurrent programs. Technical Report MSR-TR-2008-171, Microsoft Research (2008)"},{"key":"7_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., 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":"7_CR10","unstructured":"Compaq Computer Corporation. Alpha Architecture Reference Manual, 4th edn. (January 2002)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"7_CR12","unstructured":"Duffy, J.: Joe Duffy\u2019s Weblog, http:\/\/www.bluebytesoftware.com\/blog\/2007\/11\/10\/CLR20MemoryModel.aspx"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Sarkar, S., et al.: The semantics of x86-CC multiprocessor machine code. In: Principles of Programming Languages, POPL (2009)","DOI":"10.1145\/1480881.1480929"},{"key":"7_CR14","unstructured":"Gharachorloo, K.: Memory Consistency Models for Shared-Memory Multiprocessors. PhD thesis, University of Utah (2005)"},{"key":"7_CR15","unstructured":"Intel Corporation. Intel 64 Architecture Memory Ordering White Paper (August 2007)"},{"key":"7_CR16","unstructured":"International Business Machines Corporation. z\/Architecture Principles of Operation, 1st edn. (December 2000)"},{"issue":"4","key":"7_CR17","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 Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Programming Language Design and Implementation (PLDI), pp. 220\u2013231 (2003)","DOI":"10.1145\/781131.781156"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Principles of programming languages (POPL), pp. 42\u201354 (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model. In: Principles of Programming Languages (POPL), pp. 378\u2013391 (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"7_CR21","unstructured":"Morrison, V.: Understand the impact of low-lock techniques in multithreaded apps. MSDN Magazine\u00a020(10) (October 2005)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO (extended version). Technical Report UCAM-CL-TR-745, Univ. of Cambridge (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: Symposium on Parallel Algorithms and Architectures (SPAA), pp. 34\u201341 (1995)","DOI":"10.1145\/215399.215413"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: PPoPP 2007: Principles and practice of parallel programming, pp. 161\u2013172 (2007)","DOI":"10.1145\/1229428.1229469"},{"key":"7_CR25","unstructured":"Sevcik, J.: Program Transformations in Weak Memory Models. PhD thesis, University of Edinburgh (2008)"},{"key":"7_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. Sevcik","year":"2008","unstructured":"Sevcik, 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)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Shen, X., Arvind, Rudolph, L.: Commit-reconcile & fences (crf): A new memory model for architects and compiler writers. In: ISCA, pp. 150\u2013161 (1999)","DOI":"10.1145\/307338.300992"},{"key":"7_CR28","volume-title":"The SPARC Architecture Manual Version 9","year":"1994","unstructured":"Weaver, D., Germond, T. (eds.): The SPARC Architecture Manual Version 9. PTR Prentice Hall, Englewood Cliffs (1994)"},{"issue":"4","key":"7_CR29","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"W.D. Young","year":"1989","unstructured":"Young, W.D.: A mechanically verified code generator. Journal of Automated Reasoning\u00a05(4), 493\u2013518 (1989)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11970-5_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:46:00Z","timestamp":1606167960000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11970-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119699","9783642119705"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11970-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}