{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T06:49:28Z","timestamp":1768891768939,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T00:00:00Z","timestamp":1687478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"VeTSS"},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/V000470\/1, EP\/R032971\/1, EP\/R032556\/1 and EP\/V038915\/1, EP\/R025134\/2"],"award-info":[{"award-number":["EP\/V000470\/1, EP\/R032971\/1, EP\/R032556\/1 and EP\/V038915\/1, EP\/R025134\/2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000287","name":"Royal Academy of Engineering","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ARC Discovery Grant","award":["DP190102142"],"award-info":[{"award-number":["DP190102142"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,6,30]]},"abstract":"<jats:p>\n            Verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly large fragments of C11. However, these semantics and logics have been developed in a restricted setting to avoid the\n            <jats:italic>thin-air-read<\/jats:italic>\n            problem. In this article, we propose an operational semantics that leverages an intra-thread partial order (called\n            <jats:italic>semantic dependencies<\/jats:italic>\n            ) induced by a recently developed denotational event-structure-based semantics. We prove that our operational semantics is sound and complete with respect to the denotational semantics. We present an associated logic that generalises a recent Owicki\u2013Gries framework for RC11 RAR (repaired C11) with relaxed and release-acquire accesses. We describe the mechanisation of the logic in the Isabelle\/HOL theorem prover, which we use to prove correctness of a number of examples.\n          <\/jats:p>","DOI":"10.1145\/3580285","type":"journal-article","created":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T02:46:06Z","timestamp":1673664366000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7404-2367","authenticated-orcid":false,"given":"Daniel","family":"Wright","sequence":"first","affiliation":[{"name":"University of Kent, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8813-780X","authenticated-orcid":false,"given":"Sadegh","family":"Dalvandi","sequence":"additional","affiliation":[{"name":"University of Surrey, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7053-4364","authenticated-orcid":false,"given":"Mark","family":"Batty","sequence":"additional","affiliation":[{"name":"University of Kent, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[{"name":"University of Surrey, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2023,6,23]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"issue":"2","key":"e_1_3_2_3_2","doi-asserted-by":"crossref","first-page":"7:1\u20137:74","DOI":"10.1145\/2627752","article-title":"Herding cats: Modelling, simulation, testing, and data mining for weak memory","volume":"36","author":"Alglave J.","year":"2014","unstructured":"J. Alglave, L. Maranget, and M. Tautschnig. 2014. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36, 2 (2014), 7:1\u20137:74.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_3_2_4_2","first-page":"235","volume-title":"POPL\u201914","author":"Batty M.","year":"2013","unstructured":"M. Batty, M. Dodds, and A. Gotsman. 2013. Library abstraction for C\/C++ concurrency. In POPL\u201914, R. Giacobazzi and R. Cousot (Eds.). ACM, 235\u2013248."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_2_6_2","first-page":"55","volume-title":"POPL\u201911","author":"Batty M.","year":"2011","unstructured":"M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. 2011. Mathematizing C++ concurrency. In POPL\u201911, T. Ball and M. Sagiv (Eds.). ACM, 55\u201366."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_16"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3574137"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09610-2"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3545117"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295702"},{"key":"e_1_3_2_15_2","first-page":"448","volume-title":"ESOP\u201917","author":"Doko M.","year":"2017","unstructured":"M. Doko and V. Vafeiadis. 2017. Tackling real-life relaxed concurrency with FSL++. In ESOP\u201917. 448\u2013475."},{"key":"e_1_3_2_16_2","unstructured":"O. Giroux. 2019. ISO WG21 SG1 Concurrency Subgroup Vote. (2019). https:\/\/github.com\/cplusplus\/papers\/issues\/554."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:33)2019"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498716"},{"key":"e_1_3_2_20_2","first-page":"17:1\u201317:29","volume-title":"ECOOP\u201917","author":"Kaiser J.-O.","year":"2017","unstructured":"J.-O. Kaiser, H.-H. Dang, D. Dreyer, O. Lahav, and V. Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP\u201917. 17:1\u201317:29."},{"key":"e_1_3_2_21_2","first-page":"175","volume-title":"POPL\u201917","author":"Kang J.","year":"2017","unstructured":"J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In POPL\u201917, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 175\u2013189. http:\/\/dl.acm.org\/citation.cfm?id=3009850."},{"key":"e_1_3_2_22_2","first-page":"311","volume-title":"ICALP\u201915 (LNCS)","author":"Lahav O.","year":"2015","unstructured":"O. Lahav and V. Vafeiadis. 2015. Owicki-gries reasoning for weak memory models. In ICALP\u201915 (LNCS), Vol. 9135. Springer, 311\u2013323."},{"key":"e_1_3_2_23_2","first-page":"618","volume-title":"PLDI\u201917","author":"Lahav O.","year":"2017","unstructured":"O. Lahav, V. Vafeiadis, J. Kang, C.-K. Hur, and D. Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI\u201917, A. Cohen and M. T. Vechev (Eds.). ACM, 618\u2013632."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58768-0_11"},{"key":"e_1_3_2_26_2","first-page":"111","volume-title":"OOPSLA\u201916","author":"Nienhuis K.","year":"2016","unstructured":"K. Nienhuis, K. Memarian, and P. Sewell. 2016. An operational semantics for C\/C++11 concurrency. In OOPSLA\u201916. ACM, 111\u2013128."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_31"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_13"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.6084\/m9.figshare.21507636"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3580285","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3580285","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:19Z","timestamp":1750182559000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3580285"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,23]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6,30]]}},"alternative-id":["10.1145\/3580285"],"URL":"https:\/\/doi.org\/10.1145\/3580285","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,23]]},"assertion":[{"value":"2022-03-31","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-05","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}