{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,13]],"date-time":"2026-11-13T10:16:40Z","timestamp":1794565000559,"version":"4.9.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_36","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"1027-1055","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Compositional Verification of Compiler Optimisations on Relaxed Memory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4439-0130","authenticated-orcid":false,"given":"Mike","family":"Dodds","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Batty","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexey","family":"Gotsman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"2","key":"36_CR1","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, J.H., Moir, M.: Universal constructions for multi-object operations. In: Symposium on Principles of Distributed Computing (PODC), pp. 184\u2013193 (1995)","DOI":"10.1145\/224964.224985"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C\/C++ concurrency. In: Symposium on Principles of Programming Languages (POPL), pp. 235\u2013248 (2013)","DOI":"10.1145\/2429069.2429099"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-662-46669-8_12","volume-title":"Programming Languages and Systems","author":"M Batty","year":"2015","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283\u2013307. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Symposium on Principles of Programming Languages (POPL), pp. 55\u201366 (2011)","DOI":"10.1145\/1926385.1926394"},{"issue":"2","key":"36_CR6","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"S Brookes","year":"1996","unstructured":"Brookes, S.: Full abstraction for a shared-variable parallel language. Inf. Comput. 127(2), 145\u2013163 (1996)","journal-title":"Inf. Comput."},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Musuvathi, M., Singh, V.: Verifying local transformations on relaxed memory models. In: International Conference on Compiler Construction (CC), pp. 104\u2013123 (2010)","DOI":"10.1007\/978-3-642-11970-5_7"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Vafeiadis, V.: Validating optimizations of concurrent C\/C++ programs. In: International Symposium on Code Generation and Optimization (CGO), pp. 216\u2013226 (2016)","DOI":"10.1145\/2854038.2854051"},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_19"},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"Dodds, M., Batty, M., Gotsman, A.: Compositional verification of compiler optimisations on relaxed memory (extended version). CoRR, arXiv:1802.05918 (2018)","DOI":"10.1007\/978-3-319-89884-1_36"},{"issue":"3","key":"36_CR11","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"36_CR12","volume-title":"Software Abstractions - Logic Language and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions - Logic Language and Analysis, Revised edn. MIT Press, Cambridge (2012)","edition":"Revised"},{"key":"36_CR13","doi-asserted-by":"crossref","unstructured":"Jagadeesan, R., Petri, G., Riely, J.: Brookes is relaxed, almost! In: International Conference on Foundations of Software Science and Computational Structures (FOSSACS), pp. 180\u2013194 (2012)","DOI":"10.1007\/978-3-642-28729-9_12"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Jeffrey, A., Riely, J.: On thin air reads towards an event structures model of relaxed memory. In: Symposium on Logic in Computer Science (LICS), pp. 759\u2013767 (2016)","DOI":"10.1145\/2933575.2934536"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C.-K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: Symposium on Principles of Programming Languages (POPL), pp. 175\u2013189 (2017)","DOI":"10.1145\/3009837.3009850"},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Symposium on Principles of Programming Languages (POPL), pp. 649\u2013662 (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"36_CR17","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.-K., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: Conference on Programming Language Design and Implementation (PLDI), pp. 618\u2013632 (2017)","DOI":"10.1145\/3062341.3062352"},{"key":"36_CR18","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering (ICSE), pp. 609\u2013619 (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"Morisset, R., Pawan, P., Zappa Nardelli, F.: Compiler testing via a theory of sound optimisations in the C11\/C++11 memory model. In: Conference on Programming Language Design and Implementation (PLDI), pp. 187\u2013196 (2013)","DOI":"10.1145\/2491956.2491967"},{"key":"36_CR20","doi-asserted-by":"crossref","unstructured":"Pichon-Pharabod, J., Sewell, P.: A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In: Symposium on Principles of Programming Languages (POPL), pp. 622\u2013633 (2016)","DOI":"10.1145\/2837614.2837616"},{"key":"36_CR21","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-662-49674-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Daniel Poetzl","year":"2016","unstructured":"Poetzl, D., Kroening, D.: Formalizing and checking thread refinement for data-race-free execution models. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 515\u2013530 (2016)"},{"key":"36_CR22","unstructured":"The C++ Standards Committee: Programming Languages \u2013 C++ (2011). ISO\/IEC JTC1 SC22 WG21"},{"key":"36_CR23","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Zappa Nardelli, F.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: Symposium on Principles of Programming Languages (POPL), pp. 209\u2013220 (2015)","DOI":"10.1145\/2676726.2676995"},{"key":"36_CR24","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-23702-7_14","volume-title":"Static Analysis","author":"Viktor Vafeiadis","year":"2011","unstructured":"Vafeiadis, V., Zappa Nardelli, F.: Verifying fence elimination optimisations. In: International Conference on Static Analysis (SAS), pp. 146\u2013162 (2011)"},{"key":"36_CR25","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: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 27\u201351. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70592-5_3"},{"key":"36_CR26","doi-asserted-by":"crossref","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S.: Sewell, P.: Relaxed-memory concurrency and verified compilation. In: Symposium on Principles of Programming Languages (POPL), pp. 43\u201354 (2011)","DOI":"10.1145\/1925844.1926393"},{"issue":"3","key":"36_CR27","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1\u201322:50 (2013)","journal-title":"J. ACM"},{"key":"36_CR28","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: Symposium on Principles of Programming Languages (POPL), pp. 190\u2013204 (2017)","DOI":"10.1145\/3009837.3009838"}],"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-319-89884-1_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:33:24Z","timestamp":1571157204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_36","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}