{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:07Z","timestamp":1784675047774,"version":"3.55.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["62372290,62002217"],"award-info":[{"award-number":["62372290,62002217"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    It is a long-standing open problem to support verified compilation of multi-threaded programs\n                    <jats:italic toggle=\"yes\">compositionally<\/jats:italic>\n                    when sharing of stack data between threads is allowed. Although certain solutions exist on paper, none of them is completely formalized because of the difficulty in simultaneously enabling sharing and forbidding modification of stack memory in presence of arbitrary memory operations (e.g., pointer arithmetic). We present a compiler verification framework that solves this open problem in the setting of\n                    <jats:italic toggle=\"yes\">cooperative multi-threading.<\/jats:italic>\n                    To address the challenges of sharing stack data, we introduce\n                    <jats:italic toggle=\"yes\">threaded Kripke memory relations<\/jats:italic>\n                    (TKMR) to support both protection and sharing of stacks in a multi-stack memory model. We further introduce\n                    <jats:italic toggle=\"yes\">threaded forward simulations<\/jats:italic>\n                    parameterized by TKMR to capture semantics preservation for compiling program modules in multi-threaded contexts. We show that threaded forward simulations are both\n                    <jats:italic toggle=\"yes\">horizontally composable\u2014<\/jats:italic>\n                    thereby enabling the compositional verification of open threads and heterogeneous modules\u2014and\n                    <jats:italic toggle=\"yes\">vertically composable\u2014<\/jats:italic>\n                    thereby enabling composition of compiler correctness for multiple compiler passes. Furthermore, threaded forward simulations can be converted into backward simulations. We apply this framework to 18 passes of CompCert to get CompCertOC, the first optimizing verified compiler that supports compositional verification of cooperative multi-threaded programs with shared stacks.\n                  <\/jats:p>","DOI":"10.1145\/3729276","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"651-674","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7190-6983","authenticated-orcid":false,"given":"Ling","family":"Zhang","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3990-2418","authenticated-orcid":false,"given":"Yuting","family":"Wang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1943-8662","authenticated-orcid":false,"given":"Yalun","family":"Liang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523718"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_4_1","first-page":"653","volume-title":"Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201916). USENIX Association, GA, 653\u2013669."},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_3_2_9_1","doi-asserted-by":"crossref","unstructured":"Hanru Jiang Hongjin Liang Siyang Xiao Junpeng Zha and Xinyu Feng. 2019b. Towards Certified Separate Compilation for Concurrent Programs. https:\/\/plax-lab.github.io\/publications\/ccc\/ccc-tr.pdf","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454097"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_2_13_1","unstructured":"Xavier Leroy. 2005\u20132023. The CompCert Verified Compiler. https:\/\/compcert.org\/"},{"key":"e_1_3_2_14_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2..Research Report RR-7987. INRIA.26 https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103711"},{"key":"e_1_3_2_16_1","unstructured":"Rust Standard Library. 2024.std::thread::scope. https:\/\/doc.rust-lang.org\/std\/thread\/fn.scope.html"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893594"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498686"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523734"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Ling Zhang Yuting Wang Yalun Liang and Zhong Shao. 2025. CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks (Artifact). https:\/\/doi.org\/10.5281\/zenodo.15201756 10.5281\/zenodo.15201756","DOI":"10.5281\/zenodo.15201756"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632914"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729276","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:08:03Z","timestamp":1784196483000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":27,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729276"],"URL":"https:\/\/doi.org\/10.1145\/3729276","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}