{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T15:54:32Z","timestamp":1781020472416,"version":"3.54.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>Symmetry reduction (SR) and partial order reduction (POR) aim to scale up model checking by exploiting the underlying program structure: SR avoids exploring executions equivalent up to some permutation of symmetric threads, while POR avoids exploring executions equivalent up to reordering of independent instructions. While both SR and POR have been well studied individually, their combination in the context of stateless model checking has remained an open problem.<\/jats:p>\n          <jats:p>\n            In this paper, we present Spore, the first stateless model checker that combines SR and POR in a sound, complete and optimal manner. Spore can leverage both symmetries in the client program itself, but also\n            <jats:italic toggle=\"yes\">internal symmetries<\/jats:italic>\n            in the underlying implementation (i.e., idempotent operations), a novel symmetry notion we introduce in this paper. Our experiments confirm that Spore explores drastically fewer executions than tools that solely employ SR\/POR, thereby greatly advancing the state-of-the-art.\n          <\/jats:p>\n          <jats:p>\n            CCS Concepts: \u2022\n            <jats:bold>Theory of computation \u2192 Concurrency; Verification by model checking<\/jats:bold>\n            .\n          <\/jats:p>","DOI":"10.1145\/3656449","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1781-1803","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["SPORE: Combining Symmetry and Partial Order Reduction"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5077-5275","authenticated-orcid":false,"given":"Iason","family":"Marmanis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_1_3_1","first-page":"373","article-title":"\u201cOptimal dynamic partial order reduction","author":"Abdulla Parosh Aziz","year":"2014","unstructured":"Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. \u201cOptimal dynamic partial order reduction. \u201d In: POPL 2014. ACM, NewYork, NY, USA, 373-384. https:\/\/doi.org\/10.1145\/2535838.2535845.","journal-title":"\u201d In: POPL 2014. ACM, NewYork, NY, USA,"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3073408"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Bengt Jonsson and Tuan Phong Ngo. Oct. 2018.\u201cOptimal stateless model checking under the release-acquire semantics\u201d Proc. ACM Program. Lang. 2 OOPSLA (Oct. 2018) 135:1-135:29. https:\/\/doi.org\/10.1145\/3276505 10.1145\/3276505.","DOI":"10.1145\/3276505"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_24"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"e_1_3_1_10_1","unstructured":"Samy Al Bahra. N.d. Concurrency Kit. (). https:\/\/github.com\/concurrencykit\/ck."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360550"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625969"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29400-7_24"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30232-2\\_7"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_25"},{"key":"e_1_3_1_19_1","unstructured":"Facebook. N.d. Folly: Facebook Open-source Library. (). https:\/\/github.com\/facebook\/folly."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.47"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_1_23_1","article-title":"Optimised Lock-Free FIFO Queue","author":"Fober Dominique","year":"2001","unstructured":"Dominique Fober, Yann Orlarey, and Stephane Letz. 2001. Optimised Lock-Free FIFO Queue. Technical Report. GRAME.https:\/\/hal.archives-ouvertes.fr\/hal-02158792.","journal-title":"Technical Report. GRAME"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_3_1_25_1","unstructured":"Michalis Kokologiannakis. N.d. GenMC: Generic model checking for C programs. (). https:\/\/github.com\/MPI-SWS\/genmc."},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36108-1\\_18"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_3_1_29_1","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming."},{"key":"e_1_3_1_30_1","author":"N.d Max Khizhinsky.","unstructured":"Max Khizhinsky. N.d. CDS C++ library. (). https:\/\/github.com\/khizmax\/libcds.","journal-title":"CDS C++ library. ()"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"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.5281\/zenodo.10798179"},{"key":"e_1_3_1_34_1","doi-asserted-by":"crossref","unstructured":"Michalis Kokologiannakis Iason Marmanis and Viktor Vafeiadis. June 2024b. \u201cSpore: Combining Symmetry and Partial Order Reduction (supplementary material) \u201d (June 2024). https:\/\/plv.mpi-sws.org\/genmc.","DOI":"10.1145\/3656449"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8\\_12"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360599"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4\\_25"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_1_40_1","first-page":"618","article-title":"\u201cRepairing sequential consistency in C\/C++11.\u201d","author":"Lahav Ori","year":"2017","unstructured":"Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. \u201cRepairing sequential consistency in C\/C++11.\u201d In: PLDI2017. ACM, Barcelona, Spain, 618-632. ISBN: 978-1-4503-4988-8. https:\/\/doi.org\/10.1145\/3062341.3062352.","journal-title":"In: PLDI2017. ACM, Barcelona, Spain,"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_1_42_1","first-page":"1","article-title":"\u201cNonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors.\u201d","author":"Michael Maged M.","year":"1998","unstructured":"Maged M. Michael and Michael L. Scott. 1998. \u201cNonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors.\u201d J. Parallel Distrib. Comput., 51, 1, 1-26.","journal-title":"J. Parallel Distrib. Comput., 51, 1,"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_22"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.456"},{"key":"e_1_3_1_46_1","unstructured":"SPARC International Inc. 1994. The SPARC architecture manual (version 9). Prentice-Hall."},{"key":"e_1_3_1_47_1","article-title":"Systems Programming: Coping with Parallelism","author":"Treiber R. Kent","year":"1986","unstructured":"R. Kent Treiber. 1986. Systems Programming: Coping with Parallelism. Tech. rep. Technical Report RJ5118, IBM. https:\/\/dominoweb.draco.res.ibm.com\/58319a2ed2b1078985257003004617ef.html.","journal-title":"Tech. rep. Technical Report RJ5118, IBM"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Thomas Wahl and Alastair Donaldson. 2010. \u201cReplication and Abstraction: Symmetry in Automated Formal Verification.\u201d 2 2 799-847. https:\/\/doi.org\/10.3390\/sym2020799 10.3390\/sym2020799.","DOI":"10.3390\/sym2020799"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656449","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656449","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:40:29Z","timestamp":1751661629000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656449"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":47,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656449"],"URL":"https:\/\/doi.org\/10.1145\/3656449","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}