{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:26:13Z","timestamp":1784183173194,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>\n                    Clients reason about the behavior of concurrent data structure libraries such as sets, queues, or stacks using specifications that capture well-understood correctness conditions, such as linearizability. The implementation of these libraries, however, focused as they are on performance, may additionally exploit relaxed memory behavior allowed by the language or underlying hardware that weaken the strong ordering and visibility constraints on shared-memory accesses that would otherwise be imposed by a sequentially consistent (SC) memory model. As an alternative to developing new specification and verification mechanisms for reasoning about libraries under relaxed memory model, we instead consider the orthogonal problem of\n                    <jats:italic toggle=\"yes\">library robustness<\/jats:italic>\n                    , a property that holds when all possible behaviors of a library implementation under relaxed memory model are also possible under SC. In this paper, we develop a new\n                    <jats:italic toggle=\"yes\">automated<\/jats:italic>\n                    technique for verifying robustness of library implementations in the context of a C11-style memory model. This task is challenging because a most-general client may invoke an unbounded number of concurrently executing library operations that can manipulate an unbounded number of shared locations. We establish a novel inductive technique for verifying library robustness that leverages prior work on the robustness problem for the C11 memory model based on the search for a non-robustness witness under SC executions. We crucially rely on the fact that this search is carried out over SC executions, and use high-level SC specifications (including linearizability) of the library to verify the absence of a non-robustness witness. Our technique is compositional - we show how we can safely preserve robustness of multiple interacting library implementations and clients using additional SC fences to guarantee robustness of entire executions. Experimental results on a number of complex realistic library implementations demonstrate the feasibility of our approach.\n                  <\/jats:p>","DOI":"10.1145\/3689802","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2578-2605","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0679-226X","authenticated-orcid":false,"given":"Kartik","family":"Nagar","sequence":"first","affiliation":[{"name":"IIT Madras, Chennai, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2490-6478","authenticated-orcid":false,"given":"Anmol","family":"Sahoo","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-4097-8115","authenticated-orcid":false,"given":"Romit Roy","family":"Chowdhury","sequence":"additional","affiliation":[{"name":"Chennai Mathematical Institute, Chennai, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2424","authenticated-orcid":false,"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_2_2_2","article-title":"An Integrated Specification and Verification Technique for Highly Concurrent Data Structures","author":"Abdulla Parosh Aziz","year":"2013","unstructured":"Parosh Aziz Abdulla, Fr\u00e9d\u00e9ric Haziza, Luk\u00e1s Hol\u00edk, Bengt Jonsson, and Ahmed Rezine. 2013. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In TACAS.","journal-title":"TACAS"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/325096.325100"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2994593"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_6"},{"key":"e_1_3_2_6_2","unstructured":"Helge Bahmann and Tim Blechmann. 2012. https:\/\/www.boost.org\/doc\/libs\/1_85_0\/libs\/atomic\/doc\/html\/atomic\/usage_examples.html#boost_atomic.usage_examples.singleton. Accessed 31-07-2024."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_8_2","first-page":"509","article-title":"Clarifying and Compiling C\/C++ Concurrency: from C++11 to POWER","author":"Batty Mark","year":"2012","unstructured":"Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. 2012. Clarifying and Compiling C\/C++ Concurrency: from C++11 to POWER. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2012), Philadelphia, Pennsylvania, USA, January 22-28, 2012. 509\u2013520. https:\/\/doi.org\/10.1145\/2103656.2103717 10.1145\/2103656.2103717","journal-title":"Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2012), Philadelphia, Pennsylvania, USA, January 22-28, 2012"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2247684.2247688"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","unstructured":"Sebastian Burckhardt Alexey Gotsman Hongseok Yang and Marek Zawirski. 2014. Replicated data types: specification verification optimality. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL \u201914 San Diego CA USA January 20-21 2014. 271\u2013284. https:\/\/doi.org\/10.1145\/2535838.2535848 10.1145\/2535838.2535848","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_3_2_16_2","unstructured":"C11 Last Accessed Nov 9 2022. C11 Memory Model (std::memory_order). https:\/\/en.cppreference.com\/w\/cpp\/atomic\/memory_order."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_28"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_9"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158113"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290373"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737983"},{"key":"e_1_3_2_27_2","unstructured":"Folly Last Accessed Nov 9 2022. Meta Folly MPMC Queue. https:\/\/github.com\/facebook\/folly\/blob\/main\/folly\/MPMCQueue.h."},{"key":"e_1_3_2_28_2","first-page":"6:1","volume-title":"27th International Conference on Concurrency Theory (CONCUR 2016) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 59)","author":"Haas Andreas","year":"2016","unstructured":"Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. 2016. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory (CONCUR 2016) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 59), Jos\u00e9e Desharnais and Radha Jagadeesan (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1\u20136:15. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.6 10.4230\/LIPIcs.CONCUR.2016.6"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_25"},{"key":"e_1_3_2_30_2","volume-title":"Revised Reprint","author":"Herlihy Maurice","year":"2012","unstructured":"Maurice Herlihy and Nir Shavit. 2012. The Art of Multiprocessor Programming, Revised Reprint (1st ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.","edition":"1"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_27"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_19"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473571"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_47_2","unstructured":"Kartik Nagar Anmol Sahoo Romit Roy Chowdhury and Suresh Jagannathan. 2024. Artifact - Automated Robustness Verification of Concurrent Data Structure Libraries Against Relaxed Memory Models. https:\/\/doi.org\/10.5281\/zenodo.13626195 10.5281\/zenodo.13626195"},{"key":"e_1_3_2_48_2","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 European Conference on Object-Oriented Programming. https:\/\/api.semanticscholar.org\/CorpusID:28735505","journal-title":"European Conference on Object-Oriented Programming"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"e_1_3_2_50_2","first-page":"68:1","article-title":"On Library Correctness Under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries Under Declarative Consistency Models","volume":"3","author":"Raad Azalea","year":"2019","unstructured":"Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, and Viktor Vafeiadis. 2019. On Library Correctness Under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries Under Declarative Consistency Models. PACMPL 3, POPL (2019), 68:1\u201368:31. https:\/\/doi.org\/10.1145\/3290381 10.1145\/3290381","journal-title":"PACMPL"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.5555\/2049814"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571246"},{"key":"e_1_3_2_54_2","unstructured":"R.K. Treiber. 1986. Systems programming: Coping with Parallelism. Technical Report RJ-5118. Technical Report. IBM Almaden Research Center."},{"key":"e_1_3_2_55_2","unstructured":"Anthony Williams. Last Accessed Nov 9 2022. Implementing Dekker\u2019s algorithm with fences. https:\/\/www.justsoftwaresolutions.co.uk\/threading\/implementing_dekkers_algorithm_with_fences.html."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689802","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689802","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:02:52Z","timestamp":1770195772000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":54,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689802"],"URL":"https:\/\/doi.org\/10.1145\/3689802","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}