{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:12Z","timestamp":1780994652672,"version":"3.54.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is\n            <jats:italic toggle=\"yes\">consistency testing<\/jats:italic>\n            : is the observed execution of a concurrent program in alignment with the specification of the underlying system? The problem has been studied extensively across Sequential Consistency (SC) and weak memory, and proven to be\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mi>N<\/mml:mi>\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -complete when some aspect of the input (e.g., number of threads\/memory locations) is unbounded. This unboundedness has left a natural question open: are there efficient\n            <jats:italic toggle=\"yes\">parameterized<\/jats:italic>\n            algorithms for testing?\n          <\/jats:p>\n          <jats:p>\n            The main contribution of this paper is a deep hardness result for consistency testing under many popular weak-memory models: the problem remains\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mi>N<\/mml:mi>\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -complete even in its\n            <jats:italic toggle=\"yes\">bounded<\/jats:italic>\n            setting, where candidate executions contain a bounded number of threads, memory locations, and values. This hardness spreads across several Release-Acquire variants of C11, a popular variant of its Relaxed fragment, popular Causal Consistency models, and the POWER architecture. To our knowledge, this is the first result that fully exposes the hardness of weak-memory testing and proves that the problem\n            <jats:italic toggle=\"yes\">admits no parameterization<\/jats:italic>\n            under standard input parameters. It also yields a computational separation of these models from SC, x86-TSO, PSO, and Relaxed, for which bounded consistency testing is either known (for SC), or shown here (for the rest), to be in polynomial time.\n          <\/jats:p>","DOI":"10.1145\/3632908","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1978-2009","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["How Hard Is Weak-Memory Testing?"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4454-2050","authenticated-orcid":false,"given":"Soham","family":"Chakraborty","sequence":"first","affiliation":[{"name":"TU Delft, Delft, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0925-398X","authenticated-orcid":false,"given":"Shankara Narayanan","family":"Krishna","sequence":"additional","affiliation":[{"name":"IIT Bombay, Mumbai, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"},{"name":"IIT Bombay, Mumbai, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_6"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-19835-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alglave Jade","year":"2011","unstructured":"Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011. Litmus: Running Tests against Hardware. In Tools and Algorithms for the Construction and Analysis of Systems, Parosh Aziz Abdulla and K. Rustan M. Leino (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 41\u201344."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485541"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000011"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2005.86"},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","unstructured":"Soham Chakraborty Shankaranarayanan Krishna Umang Mathur and Andreas Pavlogiannis. 2023. How Hard is Weak-Memory Testing? arXiv:2311.04302 [cs.PL]","DOI":"10.1145\/3632908"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360550"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2009.4798276"},{"issue":"1","key":"e_1_3_1_20_1","first-page":"56","article-title":"Timestamps in message-passing systems that preserve the partial ordering","volume":"10","author":"Fidge C. J.","year":"1988","unstructured":"C. J. Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. Proceedings of the 11th Australian Computer Science Conference 10, 1 (1988), 56\u201366.","journal-title":"Proceedings of the 11th Australian Computer Science Conference"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2753761"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/574848"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/181014.181328"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626403001628"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.1990.89297"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276516"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571212"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505273"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591297"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446711"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2006.1598123"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_1_45_1","first-page":"478","article-title":"Reasoning about the Implementation of Concurrency Abstractions on x86-TSO","author":"Owens Scott","year":"2010","unstructured":"Scott Owens. 2010. Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In ECOOP. 478\u2013503.","journal-title":"ECOOP."},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851141.2851170"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1225053"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_1_50_1","volume-title":"The SPARC Architecture Manual (Version 9)","author":"CORPORATE SPARC International, Inc","year":"1994","unstructured":"CORPORATE SPARC International, Inc. 1994. The SPARC Architecture Manual (Version 9). Prentice-Hall, Inc., USA."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591251"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1812"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632908","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632908","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:54Z","timestamp":1751659674000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":52,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632908"],"URL":"https:\/\/doi.org\/10.1145\/3632908","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}