{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T08:57:45Z","timestamp":1783587465516,"version":"3.55.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"Abstract<\/jats:title>\n \n In a seminal work, Gibbons and Korach\u00a0[9] studied the complexity of deciding whether an observed sequence of reads and writes of a multi-threaded program admits a sequentially consistent interleaving. They showed the problem to be\n \n \n $$\\textsf{NP}$$<\/jats:tex-math>\n \n NP<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -hard even under strong syntactic restrictions. More recently, Chakraborty\n et al.<\/jats:italic>\n \u00a0[6] considered the problem for weak memory models and proved that\n \n \n $$\\textsf{NP}$$<\/jats:tex-math>\n \n NP<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -hardness remains even when the number of threads, the number of memory locations, and the value domain are all bounded.\n <\/jats:p>\n \n In this paper we revisit the problem for the release-acquire variants of the C11 memory model. Our main positive result is that consistency testing can be done in polynomial-time when each memory location is written by at most one thread (multiple readers are allowed). Notably, this restriction is already\n \n \n $$\\textsf{NP}$$<\/jats:tex-math>\n \n NP<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -hard for the model of sequential consistency. We complement our upper bound with tight hardness results: we show the problem to be\n \n \n $$\\textsf{NP}$$<\/jats:tex-math>\n \n NP<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -hard when two threads may write to the same location; furthermore, allowing three writers per location rules out\n \n \n $$2^{o(k)}\\cdot n^{\\mathcal {O}(1)}$$<\/jats:tex-math>\n \n \n \n 2<\/mml:mn>\n \n o<\/mml:mi>\n (<\/mml:mo>\n k<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msup>\n \u00b7<\/mml:mo>\n \n n<\/mml:mi>\n \n O<\/mml:mi>\n (<\/mml:mo>\n 1<\/mml:mn>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n algorithms under the Exponential Time Hypothesis, where\n k<\/jats:italic>\n denotes the number of threads, and\n n<\/jats:italic>\n the number of memory operations.\n <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_12","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:53Z","timestamp":1779024113000},"page":"234-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Complexity of\u00a0Consistency Testing for\u00a0the\u00a0Release-Acquire Semantics"],"prefix":"10.1007","author":[{"given":"R.","family":"Govind","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Krishna","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanchari","family":"Sil","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"B.","family":"Srivathsan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-030-81685-8_16","volume-title":"Computer Aided Verification","author":"P Agarwal","year":"2021","unstructured":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., Toman, V.: Stateless model checking under a reads-value-from equivalence. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 341\u2013366. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, pp. 55\u201366. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926394","DOI":"10.1145\/1926385.1926394"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: POPL, pp. 626\u2013638. ACM (2017)","DOI":"10.1145\/3009837.3009888"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bui, T.L., Chatterjee, K., Gautam, T., Pavlogiannis, A., Toman, V.: The reads-from equivalence for the TSO and PSO memory models. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201330 (2021)","DOI":"10.1145\/3485541"},{"issue":"1\u20132","key":"12_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2500000011","volume":"1","author":"S Burckhardt","year":"2014","unstructured":"Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1\u20132), 1\u2013150 (2014). https:\/\/doi.org\/10.1561\/2500000011","journal-title":"Found. Trends Program. Lang."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Krishna, S.N., Mathur, U., Pavlogiannis, A.: How hard is weak-memory testing? Proc. ACM Program. Lang. 8(POPL), 1978\u20132009 (2024)","DOI":"10.1145\/3632908"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Chen, Y., et al.: Fast complete memory consistency verification. In: HPCA, pp. 381\u2013392. IEEE Computer Society (2009)","DOI":"10.1109\/HPCA.2009.4798276"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Chini, P., Saivasan, P.: A framework for consistency algorithms. In: Saxena, N., Simon, S. (eds.) 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, 14\u201318 December 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference). LIPIcs, vol.\u00a0182, pp. 42:1\u201342:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2020.42","DOI":"10.4230\/LIPICS.FSTTCS.2020.42"},{"issue":"4","key":"12_CR9","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Govind, R., Krishna, S., Sil, S., Srivathsan, B.: Complexity of consistency testing for the release-acquire semantics (2026). https:\/\/hal.science\/hal-05534072, hAL preprint, hal-05534072","DOI":"10.1007\/978-3-032-26220-2_12"},{"issue":"4","key":"12_CR11","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1006\/jcss.2001.1774","volume":"63","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity? J. Comput. Syst. Sci. 63(4), 512\u2013530 (2001)","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR12","unstructured":"J\u00e1J\u00e1, J.: An Introduction to Parallel Algorithms. Addison\u2013Wesley (1992)"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158105, https:\/\/doi.org\/10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Vafeiadis, V.: Kater: automating weak memory model metatheory and consistency checking. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571212","DOI":"10.1145\/3571212"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2) (2022). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: PLDI 2017, pp. 618\u2013632 (2017). https:\/\/doi.org\/10.1145\/3062341.3062352, technical Appendix Available at https:\/\/plv.mpi-sws.org\/scfix\/full.pdf","DOI":"10.1145\/3062341.3062352"},{"issue":"7","key":"12_CR17","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"12_CR18","unstructured":"Lokshtanov, D., Marx, D., Saurabh, S.: Lower bounds based on the exponential time hypothesis. Bull. EATCS 105, 41\u201372 (2011). http:\/\/eatcs.org\/beatcs\/index.php\/beatcs\/article\/view\/92"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Luo, W., Demsky, B.: C11Tester: A Race Detector for C\/C++ Atomics, pp. 630\u2013646. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3445814.3446711","DOI":"10.1145\/3445814.3446711"},{"key":"12_CR20","unstructured":"Manovit, C., Hangal, S.: Completely verifying memory consistency of test program executions. In: HPCA, pp. 166\u2013175. IEEE Computer Society (2006)"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Margalit, R., Lahav, O.: Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434285","DOI":"10.1145\/3434285"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Mathur, U., Pavlogiannis, A., Viswanathan, M.: The complexity of dynamic data race prediction. In: LICS, pp. 713\u2013727. ACM (2020)","DOI":"10.1145\/3373718.3394783"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Norris, B., Demsky, B.: Cdschecker: checking concurrent data structures written with C\/C++ atomics. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 131\u2013150. Association for Computing Machinery, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2509136.2509514","DOI":"10.1145\/2509136.2509514"},{"issue":"8","key":"12_CR24","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1109\/TPDS.2003.1225053","volume":"14","author":"S Qadeer","year":"2003","unstructured":"Qadeer, S.: Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans. Parallel Distrib. Syst. 14(8), 730\u2013741 (2003)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Tun\u00e7, H.C., Abdulla, P.A., Chakraborty, S., Krishna, S., Mathur, U., Pavlogiannis, A.: Optimal reads-from consistency checking for c11-style memory models. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591251","DOI":"10.1145\/3591251"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Vassilevska Williams, V., Williams, R.R.: Subcubic equivalences between path, matrix, and triangle problems. J. ACM 65(5), 27:1\u201327:38 (2018)","DOI":"10.1145\/3186893"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:06Z","timestamp":1783542546000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}