{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T13:22:03Z","timestamp":1791206523894,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642237010","type":"print"},{"value":"9783642237027","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-23702-7_14","type":"book-chapter","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T17:31:31Z","timestamp":1315589491000},"page":"146-162","source":"Crossref","is-referenced-by-count":17,"title":["Verifying Fence Elimination Optimisations"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Vafeiadis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francesco","family":"Zappa Nardelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci., 253\u2013284 (1991)","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"14_CR2","unstructured":"Alglave, J.: A shared memory poetics. Ph.D. thesis, Universit\u00e9 Paris 7 (2010)"},{"key":"14_CR3","unstructured":"Becker, P.: Working draft, standard for programming language C++, n3090=10-0080 (March 2010)"},{"issue":"3","key":"14_CR4","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-11970-5_7","volume-title":"Compiler Construction","author":"S. Burckhardt","year":"2010","unstructured":"Burckhardt, S., Musuvathi, M., Singh, V.: Verifying local transformations on relaxed memory models. In: Gupta, R. (ed.) CC 2010. LNCS, vol.\u00a06011, pp. 104\u2013123. Springer, Heidelberg (2010)"},{"key":"14_CR7","unstructured":"Cao Minh, C., Chung, J., Kozyrakis, C., Olukotun, K.: STAMP: Stanford transactional applications for multi-processing. In: IISWC (2008)"},{"key":"14_CR8","unstructured":"The Compcert verified compiler, v.\u00a01.5 (August 2009), http:\/\/compcert.inria.fr\/release\/compcert-1.5.tgz"},{"key":"14_CR9","unstructured":"CompCertTSO (2011), http:\/\/www.cl.cam.ac.uk\/~pes20\/CompCertTSO"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/11864219_14","volume-title":"Distributed Computing","author":"D. Dice","year":"2006","unstructured":"Dice, D., Shalev, O., Shavit, N.N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol.\u00a04167, pp. 194\u2013208. Springer, Heidelberg (2006)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Eide, E., Regehr, J.: Volatiles are miscompiled, and what to do about it. In: EMSOFT (2008)","DOI":"10.1145\/1450058.1450093"},{"key":"14_CR12","unstructured":"Fraser, K.: Practical Lock Freedom. Ph.D. thesis, University of Cambridge, also available as Tech. Report UCAM-CL-TR-639 (2003)"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10703-007-0041-6","volume":"31","author":"T.Q. Huynh","year":"2007","unstructured":"Huynh, T.Q., Roychoudhury, A.: Memory model sensitive bytecode verification. Form. Methods Syst. Des.\u00a031, 281\u2013305 (2007)","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR14","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2010)"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1109\/12.947002","volume":"50","author":"J. Lee","year":"2001","unstructured":"Lee, J., Padua, D.A.: Hiding relaxed memory consistency with a compiler. IEEE Trans. Comput.\u00a050, 824\u2013833 (2001)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"14_CR16","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009), http:\/\/gallium.inria.fr\/~xleroy\/publi\/compcert-backend.pdf","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations I: untimed systems. Inf. Comput.\u00a0121, 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model. In: POPL (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1145\/359060.359069","volume":"22","author":"E. Morel","year":"1979","unstructured":"Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Commun. ACM\u00a022, 96\u2013103 (1979)","journal-title":"Commun. ACM"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: PLDI (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"14_CR22","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":"14_CR23","doi-asserted-by":"crossref","unstructured":"\u0160ev\u010dik, J.: Safe optimisations for shared-memory concurrent programs. In: PLDI (2011)","DOI":"10.1145\/1993498.1993534"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"\u0160ev\u010dik, J., Vafeiadis, V., Zappa\u00a0Nardelli, F., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL (2011)","DOI":"10.1145\/1926385.1926393"},{"issue":"7","key":"14_CR25","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., Zappa Nardelli, F., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM\u00a053(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"14_CR26","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D. Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst.\u00a010, 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Sura, Z., Fang, X., Wong, C.-L., Midkiff, S.P., Lee, J., Padua, D.: Compiler techniques for high performance sequentially consistent Java programs. In: PPoPP (2005)","DOI":"10.1145\/1065944.1065947"},{"key":"14_CR28","unstructured":"Terekhov, A.: Brief tentative example x86 implementation for C\/C++ memory model. cpp-threads mailing list (2008), http:\/\/www.decadent.org.uk\/pipermail\/cpp-threads\/2008-December\/001933.html"},{"key":"14_CR29","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism. Tech. rep. (1986)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23702-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T03:03:33Z","timestamp":1560567813000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23702-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237010","9783642237027"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23702-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}