{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:24Z","timestamp":1775790684204,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,10,24]]},"abstract":"<jats:p>We present a framework for the efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C\/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which specify how reads obtain their values from writes. This is in contrast to previous approaches, which also explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially significant source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.<\/jats:p>","DOI":"10.1145\/3276505","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":58,"title":["Optimal stateless model checking under the release-acquire semantics"],"prefix":"10.1145","volume":"2","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Tuan Phong","family":"Ngo","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_2_3_1","volume-title":"CONCUR","author":"Abdulla Parosh Aziz","year":"2016"},{"key":"e_1_2_2_4_1","volume-title":"Context-Bounded Analysis for POWER. In TACAS","author":"Abdulla Parosh Aziz","year":"2017"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Bengt Jonsson and Carl Leonardsson. 2016b. Stateless Model Checking for POWER. In Computer Aided Verification (CAV) (LNCS) Vol. 9780. Springer Toronto ON Canada 134\u2013156.  Parosh Aziz Abdulla Mohamed Faouzi Atig Bengt Jonsson and Carl Leonardsson. 2016b. Stateless Model Checking for POWER. In Computer Aided Verification (CAV) (LNCS) Vol. 9780. Springer Toronto ON Canada 134\u2013156.","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"e_1_2_2_8_1","volume-title":"Computer Aided Verification, (CAV) (LNCS)","author":"Alglave Jade"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001436"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.50"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_2_17_1","unstructured":"Thomas H. Cormen Charles E. Leiserson Ronald L. Rivest and Clifford Stein. 2009. Introduction to Algorithms. The MIT Press.   Thomas H. Cormen Charles E. Leiserson Ronald L. Rivest and Clifford Stein. 2009. Introduction to Algorithms. The MIT Press."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"P.\n       \n      Godefroid\n    . 1996.\n      \n  \n   \n  Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem\n   . Ph.D. Dissertation. University of Li\u00e8ge. Also volume \n  1032\n   of \n  LNCS Springer\n  .  P. Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem . Ph.D. Dissertation. University of Li\u00e8ge. Also volume 1032 of LNCS Springer.","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271800"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_2_2_26_1","unstructured":"ISO. 2012. C++ Specification Standard. International Organization for Standardization. 1338 (est.) pages.  ISO. 2012. C++ Specification Standard. International Organization for Standardization. 1338 (est.) pages."},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the 31st European Conference on Object-Oriented Programming, ECOOP 2017 . 17:1\u201317:29","author":"Kaiser Jan-Oliver","year":"2017"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092287"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993521"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/645604.662740"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"A. Mazurkiewicz. 1986. Trace Theory. In Advances in Petri Nets.   A. Mazurkiewicz. 1986. Trace Theory. In Advances in Petri Nets.","DOI":"10.1007\/3-540-17906-2_30"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_2_36_1","unstructured":"M. Musuvathi S. Qadeer T. Ball G. Basler P.A. Nainar and I. Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI. USENIX Association 267\u2013280.   M. Musuvathi S. Qadeer T. Ball G. Basler P.A. Nainar and I. Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI. USENIX Association 267\u2013280."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2806886"},{"key":"e_1_2_2_38_1","volume-title":"Computer Aided Verification, (CAV) (LNCS)","author":"Peled Doron A."},{"key":"e_1_2_2_39_1","unstructured":"Personal-com. 2018. Personal communication with authors of RCMC.  Personal-com. 2018. Personal communication with authors of RCMC."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851141.2851171"},{"key":"e_1_2_2_41_1","unstructured":"Pedro Ramalhete and Andreia Correia. 2018. https:\/\/github.com\/pramalhe\/ConcurrencyFreaks. {Online; accessed 2018-07-10}.  Pedro Ramalhete and Andreia Correia. 2018. https:\/\/github.com\/pramalhe\/ConcurrencyFreaks. {Online; accessed 2018-07-10}."},{"key":"e_1_2_2_42_1","volume-title":"Unfolding-based Partial Order Reduction. In CONCUR 2015 . 456\u2013469","author":"Rodr\u00edguez C\u00e9sar","year":"2015"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2012.18"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_2_45_1","volume-title":"Haifa Verification Conference . 166\u2013182","author":"Sen K."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_2_47_1","unstructured":"Abraham Silberschatz Peter B. Galvin and Greg Gagne. 2012. Operating System Concepts (9th ed.). Wiley Publishing.   Abraham Silberschatz Peter B. Galvin and Greg Gagne. 2012. Operating System Concepts (9th ed.). Wiley Publishing."},{"key":"e_1_2_2_48_1","unstructured":"SPSC-bug. 2008. https:\/\/groups.google.com\/forum\/#!msg\/comp.programming.threads\/nSSFT9vKEe0\/7eD3ioDg6nEJ. {Online; accessed 2018-04-11}.  SPSC-bug. 2008. https:\/\/groups.google.com\/forum\/#!msg\/comp.programming.threads\/nSSFT9vKEe0\/7eD3ioDg6nEJ. {Online; accessed 2018-04-11}."},{"key":"e_1_2_2_49_1","unstructured":"SV-COMP. 2018. Competition on Software Verification. https:\/\/sv-comp.sosy-lab.org\/2018 . {Online; accessed 2017-11-10}.  SV-COMP. 2018. Competition on Software Verification. https:\/\/sv-comp.sosy-lab.org\/2018 . {Online; accessed 2017-11-10}."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_2_2_51_1","first-page":"491","article-title":"Stubborn Sets for Reduced State Space Generation","volume":"483","author":"Valmari A.","year":"1990","journal-title":"Advances in Petri Nets (LNCS)"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276505","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":52,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276505"],"URL":"https:\/\/doi.org\/10.1145\/3276505","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}