{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:23Z","timestamp":1774025783957,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030449131","type":"print"},{"value":"9783030449148","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a denotational semantics for weak memory concurrency that avoids <jats:italic>thin-air reads<\/jats:italic>, provides data-race free programs with sequentially consistent semantics (DRF-SC), and supports a compositional refinement relation for validating optimisations. Our semantics identifies false program dependencies that might be removed by compiler optimisation, and leaves in place just the dependencies necessary to rule out thin-air reads. We show that our dependency calculation can be used to rule out thin-air reads in any axiomatic concurrency model, in particular C++. We present a tool that automatically evaluates litmus tests, show that we can augment C++ to fix the thin-air problem, and we prove that our augmentation is compatible with the previously used compilation mappings over key processor architectures. We argue that our dependency calculation offers a practical route to fixing the longstanding problem of thin-air reads in the C++ specification.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_22","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"599-625","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Modular Relaxed Dependencies in Weak Memory Concurrency"],"prefix":"10.1007","author":[{"given":"Marco","family":"Paviotti","sequence":"first","affiliation":[]},{"given":"Simon","family":"Cooksey","sequence":"additional","affiliation":[]},{"given":"Anouk","family":"Paradis","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Wright","sequence":"additional","affiliation":[]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Batty","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering \u2014 a new definition. In: ISCA (1990)","DOI":"10.1145\/325164.325100"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.: Frightening small children and disconcerting grown-ups: Concurrency in the linux kernel. In: ASPLOS (2018)","DOI":"10.1145\/3173162.3177156"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data-mining for weak memory. In: PLDI (2014)","DOI":"10.1145\/2594291.2594347"},{"key":"22_CR4","unstructured":"Batty, M.: The C11 and C++11 Concurrency Model. Ph.D. thesis, University of Cambridge, UK (2015)"},{"key":"22_CR5","unstructured":"Batty, M., Cooksey, S., Owens, S., Paradis, A., Paviotti, M., Wright, D.: Modular Relaxed Dependencies: A new approach to the Out-Of-Thin-Air Problem (2019), http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2019\/p1780r0.html"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Batty, M., Donaldson, A.F., Wickerson, J.: Overhauling SC atomics in C11 and opencl. In: POPL (2016)","DOI":"10.1145\/2837614.2837637"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: ESOP (2015)","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"22_CR9","unstructured":"Benton, N., Hur, C.: Step-indexing: The good, the bad and the ugly. In: Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010 (2010)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency model. In: PLDI (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Vafeiadis, V.: Grounding thin-air reads with event structures. In: POPL (2019)","DOI":"10.1145\/3290383"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Dodds, M., Batty, M., Gotsman, A.: Compositional verification of compiler optimisations on relaxed memory. In: ESOP (2018)","DOI":"10.1007\/978-3-319-89884-1_36"},{"key":"22_CR13","unstructured":"ISO\/IEC JTC 1\/SC 22 Programming languages, their environments and system software interfaces: ISO\/IEC 14882:2017 Programming languages \u2014 C++ (2017)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Jeffrey, A., Riely, J.: On thin air reads towards an event structures model of relaxed memory. In: LICS (2016)","DOI":"10.1145\/2933575.2934536"},{"key":"22_CR15","unstructured":"Jeffrey, A., Riely, J.: On thin air reads: Towards an event structures model of relaxed memory. Logical Methods in Computer Science 15(1) (2019)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL (2017)","DOI":"10.1145\/3009837.3009850"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Kavanagh, R., Brookes, S.: A denotational semantics for SPARC TSO. MFPS (2018)","DOI":"10.1016\/j.entcs.2018.03.025"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: PLDI (2017)","DOI":"10.1145\/3062341.3062352"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. (2009)","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: Making the java memory model safe. ACM Trans. Program. Lang. Syst. 35(4), 12:1\u201312:65 (2013). https:\/\/doi.org\/10.1145\/2518191","DOI":"10.1145\/2518191"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java Memory Model. In: POPL (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"22_CR22","unstructured":"McKenney, P.E., Jeffrey, A., Sezgin, A., Tye, T.: Out-of-Thin-Air Execution is Vacuous (2016), http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2016\/p0422r0.html"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Michalis\u00a0Kokologiannakis, Azalea\u00a0Raad, V.V.: Model checking for weakly consistent libraries. In: PLDI (2019)","DOI":"10.1145\/3314221.3314609"},{"key":"22_CR24","unstructured":"Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (2016)"},{"key":"22_CR25","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: POPL (2016)","DOI":"10.1145\/2837614.2837616"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Podkopaev, A., Lahav, O., Vafeiadis, V.: Bridging the gap between programming languages and hardware weak memory models. PACMPL (POPL) (2019)","DOI":"10.1145\/3290382"},{"key":"22_CR27","unstructured":"Pugh, W.: Java causality tests. http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/CausalityTestCases.html (2004), accessed: 2018-11-17"},{"key":"22_CR28","unstructured":"Riely, J., Jagadeesan, R., Jeffery, A.: private correspondence (2020)"},{"key":"22_CR29","unstructured":"\u0160ev\u010d\u00edk, J.: Program transformations in weak memory models. Ph.D. thesis, University of Edinburgh, UK (2009)"},{"key":"22_CR30","unstructured":"\u0160ev\u010d\u00edk, J., Aspinall, D.: On validity of program transformations in the java memory model. In: ECOOP (2008)"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Streicher, T.: Domain-theoretic foundations of functional programming (01 2006)","DOI":"10.1142\/6284"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: POPL (2017)","DOI":"10.1145\/3009837.3009838"},{"key":"22_CR33","unstructured":"Winskel, G.: Event structures. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986 (1986)"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Winskel, G.: An introduction to event structures (1989)","DOI":"10.7146\/dpb.v18i278.6655"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:12:21Z","timestamp":1656609141000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11-12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}