{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:12:26Z","timestamp":1784211146805,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Recurrence sets characterize non-termination in sequential programs. We present a generalization of recurrence sets to concurrent programs that run on weak memory models. Sequential programs have operational semantics in terms of states and transitions, and classical recurrence sets are defined as sets of states that are existentially closed under transitions. Concurrent programs have axiomatic semantics in terms of executions, and our new recurrence sets are defined as sets of executions that are existentially closed under extensions.<\/jats:p>\n                  <jats:p>The semantics of concurrent programs is not only affected by the memory model, but also by fairness assumptions about its environment, be it the scheduler or the memory subsystems. Our new recurrence sets are formulated relative to such fairness assumptions. We show that our recurrence sets are sound for proving fair non-termination on all practical memory models, and even complete on many.<\/jats:p>\n                  <jats:p>To turn our theory into practice, we develop a new automated technique for proving fair non-termination in concurrent programs on weak memory models. At the heart of this technique is a finite representation of recurrence sets in terms of execution-based lassos. We implemented a lasso-finding algorithm in Dartagnan, and evaluated it on a number of programs running under CPU and GPU memory models.<\/jats:p>","DOI":"10.1145\/3776687","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1296-1325","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-8552","authenticated-orcid":false,"given":"Thomas","family":"Haas","sequence":"first","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8830","authenticated-orcid":false,"given":"Hern\u00e1n","family":"Ponce de Le\u00f3n","sequence":"additional","affiliation":[{"name":"Huawei Dresden Research Center, Dresden, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8922-790X","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Lomel\u00ed Gardu\u00f1o","sequence":"additional","affiliation":[{"name":"Huawei Dresden Research Center, Dresden, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_10"},{"key":"e_1_3_2_3_2","unstructured":"Andy Adinets and Duane Merrill. 2022. Onesweep: A Faster Least Significant Digit Radix Sort for GPUs. arXiv:2206.01784 [cs.DC] https:\/\/arxiv.org\/abs\/2206.01784"},{"key":"e_1_3_2_4_2","volume-title":"A Shared Memory Poetics","author":"Alglave Jade","year":"2010","unstructured":"Jade Alglave. 2010. A Shared Memory Poetics. Th\u00e8se de doctorat. L\u2019universit\u00e9 Paris Denis Diderot."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Jade Alglave Patrick Cousot and Luc Maranget. 2016. Syntax and semantics of the weak consistency model specification language CAT. CoRR abs\/1608.07531 (2016). doi:10.48550\/arXiv.1608.07531","DOI":"10.48550\/arXiv.1608.07531"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Mark Batty Alastair F. Donaldson and John Wickerson. 2016. Overhauling SC atomics in C11 and OpenCL. In POPL. ACM 634\u2013648. doi:10.1145\/2837614.2837637","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Guy E. Blelloch. 2018. Prefix sums and their applications. (6 2018). doi:10.1184\/R1\/6608579.v1","DOI":"10.1184\/R1\/6608579.v1"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192405"},{"key":"e_1_3_2_14_2","volume-title":"Scanbox: A tunable and portable GPU prefix scan implementation in Vulkan and WebGPU. Bachelor\u2019s thesis","author":"Contini James V.","year":"2025","unstructured":"James V. Contini. 2025. Scanbox: A tunable and portable GPU prefix scan implementation in Vulkan and WebGPU. Bachelor\u2019s thesis. University of California Santa Cruz."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328459"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Thomas Haas Roland Meyer Ponce de Leon Hernan and Andr\u00e9s Lomeli. 2025. Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models (Artifact). doi:10.5281\/zenodo.17770530","DOI":"10.5281\/zenodo.17770530"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563292"},{"key":"e_1_3_2_19_2","unstructured":"Alastair Harrison. 2024. [libc++] Incorrect memory order in atomic wait. https:\/\/github.com\/llvm\/llvm-project\/issues\/109290"},{"key":"e_1_3_2_20_2","unstructured":"Mateusz Kielan. 2025. Do Subgroup Shuffle Intrinsics require a preceeding OpControlBarrier with scope at least Subgroup to avoid UB? https:\/\/github.com\/KhronosGroup\/Vulkan-Docs\/issues\/2548"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428294"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485475"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_16"},{"key":"e_1_3_2_25_2","unstructured":"Raph Levien. 2020. Prefix sum on Vulkan. https:\/\/raphlinus.github.io\/gpu\/2020\/04\/30\/prefix-sum.html."},{"key":"e_1_3_2_26_2","unstructured":"Raph Levien. 2021. An HLSL implementation of prefix-scan. https:\/\/github.com\/linebender\/vello\/blob\/custom-hal-archive-with-shaders\/tests\/shader\/prefix.comp."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598095"},{"key":"e_1_3_2_28_2","unstructured":"Reese Levine and James Contini. 2023. An OpenCL implementation of prefix-scan. https:\/\/github.com\/reeselevine\/vk-prefix-scan."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575750"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304043"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040336"},{"key":"e_1_3_2_33_2","unstructured":"Duane Merrill and Michael Garland. 2016. Single-pass Parallel Prefix Scan with Decoupled Look-back. https:\/\/research.nvidia.com\/publication\/2016-03_single-pass-parallel-prefix-scan-decoupled-look-back."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_27"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_15"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_24"},{"key":"e_1_3_2_40_2","unstructured":"S4C Safe and Scalable System Software Concurrency. 2024. libvsync. https:\/\/github.com\/open-s4c\/libvsync."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_42_2","unstructured":"Frank Sch\u00fcssele. 2022. New subcategory: Termination concurrent. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks\/-\/merge_requests\/1363"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.2312\/EGGH\/EGGH07\/097106"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Thomas Smith Raph Levien and John D. Owens. 2025. Decoupled Fallback: A Portable Single-Pass GPU Scan. In Proceedings of the 37th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA\u201925). doi:10.1145\/3694906.3743326","DOI":"10.1145\/3694906.3743326"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984032"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.23"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485508"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622781.3674174"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776687","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:42:34Z","timestamp":1784209354000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776687"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776687"],"URL":"https:\/\/doi.org\/10.1145\/3776687","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}