{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:03:37Z","timestamp":1750309417459,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:00Z","timestamp":1725494400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62032024"],"award-info":[{"award-number":["62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cDigital Silk Road\u201d Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]},{"name":"Shanghai Trusted Industry Internet Software Collaborative Innovation Center"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>The C and C++ languages introduced the relaxed-memory concurrency into the language specification for efficiency purposes in 2011. Trace semantics can provide the mathematical foundation for the proposed C++11 memory model, and there is a lack of investigation of trace semantics for C++11.<\/jats:p>\n          <jats:p>The Promising Semantics (PS) of Kang et\u00a0al. provides the standard SC-style operational semantics for the C++11 concurrency model, where \u201cSC\u201d refers to \u201cSequential Consistency\u201d. Inspired by PS, in this article we first investigate the trace semantics for the relaxed read and write accesses under C++11, acting in the denotational semantics style. In our semantic model, a trace is in the form of a sequence of snapshots, and the snapshots record the modification in the relevant global or local variables, and the thread view. Moreover, the trace semantics for the release\/acquire accesses under C++11 is also explored, based on the separated thread views and newly added message views. When considering this trace model, different accesses bring in their unique snapshots, and make distinguished effects on the production of the sequences.<\/jats:p>\n          <jats:p>For any given program, the proposed trace semantics in this article produces all the valid traces directly. Furthermore, our trace semantics, together with that for TSO and MCA ARMv8, has the possibility to be the foundation of the meta model of the trace semantics for weak memory models.<\/jats:p>","DOI":"10.1145\/3670696","type":"journal-article","created":{"date-parts":[[2024,6,5]],"date-time":"2024-06-05T11:17:23Z","timestamp":1717586243000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Trace Semantics for C++11 Memory Model"],"prefix":"10.1145","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9006-6219","authenticated-orcid":false,"given":"Lili","family":"Xiao","sequence":"first","affiliation":[{"name":"School of Computer Science and Technology, Donghua University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3923-7972","authenticated-orcid":false,"given":"Sini","family":"Chen","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1303-2760","authenticated-orcid":false,"given":"Mengda","family":"He","sequence":"additional","affiliation":[{"name":"Teesside University, Middlesbrough, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3028-8191","authenticated-orcid":false,"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[{"name":"Xidian University, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,9,5]]},"reference":[{"key":"e_1_3_3_2_2","first-page":"55","volume-title":"Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011.","author":"Batty Mark","year":"2011","unstructured":"Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011.Thomas Ball and Mooly Sagiv (Eds.), ACM, 55\u201366."},{"key":"e_1_3_3_3_2","volume-title":"The C11 and C++11 Concurrency Model","author":"Batty Mark John","year":"2015","unstructured":"Mark John Batty. 2015. The C11 and C++11 Concurrency Model. Ph.D. Dissertation. University of Cambridge, UK."},{"doi-asserted-by":"publisher","key":"e_1_3_3_4_2","DOI":"10.1006\/inco.1996.0056"},{"doi-asserted-by":"publisher","key":"e_1_3_3_5_2","DOI":"10.1007\/s00165-012-0253-4"},{"key":"e_1_3_3_6_2","first-page":"11:1\u201311:26","volume-title":"Proceedings of the 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15\u201317, 2020, Berlin, Germany (Virtual Conference).","volume":"166","author":"Dalvandi Sadegh","year":"2020","unstructured":"Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. 2020. Owicki-gries reasoning for C11 RAR. In Proceedings of the 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15\u201317, 2020, Berlin, Germany (Virtual Conference).Robert Hirschfeld and Tobias Pape (Eds.), Vol. 166, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11:1\u201311:26."},{"doi-asserted-by":"publisher","key":"e_1_3_3_7_2","DOI":"10.1007\/s10817-021-09610-2"},{"key":"e_1_3_3_8_2","first-page":"608","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016","author":"Flur Shaked","year":"2016","unstructured":"Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016. Rastislav Bod\u00edk and Rupak Majumdar (Eds.), ACM, 608\u2013621."},{"key":"e_1_3_3_9_2","volume-title":"Unifying Theories of Programming","author":"Hoare Charles Antony Richard","year":"1998","unstructured":"Charles Antony Richard Hoare and He Jifeng. 1998. Unifying Theories of Programming. Prentice Hall Englewood Cliffs."},{"doi-asserted-by":"publisher","key":"e_1_3_3_10_2","DOI":"10.1007\/s10817-020-09579-4"},{"key":"e_1_3_3_11_2","first-page":"175","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017.","author":"Kang Jeehoon","year":"2017","unstructured":"Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017.Giuseppe Castagna and Andrew D. Gordon (Eds.), ACM, 175\u2013189."},{"unstructured":"Ryan Kavanagh and Stephen Brookes. 2018. A denotational account of C11-style memory. arXiv:1804.04214. Retrieved from https:\/\/arxiv.org\/abs\/1804.04214","key":"e_1_3_3_12_2"},{"issue":"2","key":"e_1_3_3_13_2","article-title":"A denotational semantics for SPARC TSO","volume":"15","author":"Kavanagh Ryan","year":"2019","unstructured":"Ryan Kavanagh and Stephen Brookes. 2019. A denotational semantics for SPARC TSO. Logical Methods in Computer Science 15, 2 (2019), 1\u201323.","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_14_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-319-48989-6_29","volume-title":"Proceedings of the FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9\u201311, 2016.","volume":"9995","author":"Lahav Ori","year":"2016","unstructured":"Ori Lahav and Viktor Vafeiadis. 2016. Explaining relaxed memory models with program transformations. In Proceedings of the FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9\u201311, 2016.John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.), Lecture Notes in Computer Science, Vol. 9995, 479\u2013495."},{"doi-asserted-by":"publisher","key":"e_1_3_3_15_2","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_3_16_2","first-page":"197","volume-title":"Proceedings of the Concurrency: The Works of Leslie Lamport.","author":"Lamport Leslie","year":"2019","unstructured":"Leslie Lamport. 2019. How to make a multiprocessor computer that correctly executes multiprocess programs. In Proceedings of the Concurrency: The Works of Leslie Lamport.Dahlia Malkhi (Ed.), ACM, 197\u2013201."},{"key":"e_1_3_3_17_2","first-page":"362","volume-title":"Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15\u201320, 2020","author":"Lee Sung-Hwan","year":"2020","unstructured":"Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis. 2020. Promising 2.0: Global optimizations in relaxed memory concurrency. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15\u201320, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 362\u2013376."},{"key":"e_1_3_3_18_2","first-page":"123","volume-title":"Proceedings of the 26th International Conference on Engineering of Complex Computer Systems. Hiroshima, Japan, March 26\u201330, 2022","author":"Li Ran","year":"2022","unstructured":"Ran Li, Huibiao Zhu, and Richard Banach. 2022. Denotational and algebraic semantics for cyber-physical systems. In Proceedings of the 26th International Conference on Engineering of Complex Computer Systems. Hiroshima, Japan, March 26\u201330, 2022. IEEE, 123\u2013132."},{"key":"e_1_3_3_19_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/978-3-642-31424-7_36","volume-title":"Proceedings of the Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7\u201313.","volume":"7358","author":"Mador-Haim Sela","year":"2012","unstructured":"Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An axiomatic memory model for POWER multiprocessors. In Proceedings of the Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7\u201313.P. Madhusudan and Sanjit A. Seshia (Eds.), Lecture Notes in Computer Science, Vol. 7358, Springer, 495\u2013512."},{"key":"e_1_3_3_20_2","first-page":"378","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12\u201314, 2005.","author":"Manson Jeremy","year":"2005","unstructured":"Jeremy Manson, William W. Pugh, and Sarita V. Adve. 2005. The Java memory model. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12\u201314, 2005.Jens Palsberg and Mart\u00edn Abadi (Eds.), ACM, 378\u2013391."},{"key":"e_1_3_3_21_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference. Munich, Germany, August 17\u201320, 2009.","volume":"5674","author":"Owens Scott","year":"2009","unstructured":"Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A better x86 memory model: x86-TSO. In Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference. Munich, Germany, August 17\u201320, 2009.Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Lecture Notes in Computer Science, Vol. 5674, Springer, 391\u2013407."},{"key":"e_1_3_3_22_2","volume-title":"A Structural Approach to Operational Semantics","author":"Plotkin Gordon D.","year":"1981","unstructured":"Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. Aarhus university."},{"key":"e_1_3_3_23_2","first-page":"19:1\u201319:29","article-title":"Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8","volume":"2","author":"Pulte Christopher","year":"2018","unstructured":"Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2018. Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2, POPL (2018), 19:1\u201319:29.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_3_24_2","first-page":"175","volume-title":"Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4\u20138, 2011.","author":"Sarkar Susmit","year":"2011","unstructured":"Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding POWER multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4\u20138, 2011.Mary W. Hall and David A. Padua (Eds.), ACM, 175\u2013186."},{"doi-asserted-by":"publisher","key":"e_1_3_3_25_2","DOI":"10.1145\/1785414.1785443"},{"doi-asserted-by":"publisher","key":"e_1_3_3_26_2","DOI":"10.5555\/2028905"},{"key":"e_1_3_3_27_2","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"Stoy Joseph E.","year":"1981","unstructured":"Joseph E. Stoy. 1981. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT press."},{"doi-asserted-by":"publisher","key":"e_1_3_3_28_2","DOI":"10.5555\/524724"},{"key":"e_1_3_3_29_2","first-page":"237","volume-title":"Proceedings of the Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20\u201326, 2021.","volume":"13047","author":"Wright Daniel","year":"2021","unstructured":"Daniel Wright, Mark Batty, and Brijesh Dongol. 2021. Owicki-gries reasoning for C11 programs with relaxed dependencies. In Proceedings of the Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20\u201326, 2021.Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan (Eds.), Lecture Notes in Computer Science, Vol. 13047, Springer, 237\u2013254."},{"doi-asserted-by":"publisher","key":"e_1_3_3_30_2","DOI":"10.1016\/j.sysarc.2022.102438"},{"key":"e_1_3_3_31_2","first-page":"1","volume-title":"Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conference. Los Alamitos, CA, USA, June 27\u2013July 1, 2022","author":"Xiao Lili","year":"2022","unstructured":"Lili Xiao, Huibiao Zhu, Mengda He, and Shengchao Qin. 2022. Algebraic semantics for C++11 memory model. In Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conference. Los Alamitos, CA, USA, June 27\u2013July 1, 2022. Hong Va Leong, Sahra Sedigh Sarvestani, Yuuichi Teranishi, Alfredo Cuzzocrea, Hiroki Kashiwazaki, Dave Towey, Ji-Jiang Yang, and Hossain Shahriar (Eds.), IEEE, 1\u20136."},{"doi-asserted-by":"publisher","key":"e_1_3_3_32_2","DOI":"10.1007\/s11390-021-1616-1"},{"doi-asserted-by":"publisher","key":"e_1_3_3_33_2","DOI":"10.1007\/s00165-021-00530-x"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670696","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3670696","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:58:21Z","timestamp":1750294701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670696"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,5]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3670696"],"URL":"https:\/\/doi.org\/10.1145\/3670696","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2024,9,5]]},"assertion":[{"value":"2023-07-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-20","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}