{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:28Z","timestamp":1776305308182,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377051","type":"print"},{"value":"9783031377068","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>\nExisting dynamic partial order reduction (DPOR) algorithms scale poorly on concurrent data structure benchmarks because they visit a huge number of blocked executions due to spinloops.<\/jats:p><jats:p>In response, we develop <jats:sc>Awamoche<\/jats:sc>, a sound, complete, and strongly optimal DPOR algorithm that avoids exploring any useless blocked executions in programs with await and confirmation-CAS loops. Consequently, it outperforms the state-of-the-art, often by an exponential factor.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_12","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"230-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Unblocking Dynamic Partial Order Reduction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5077-5275","authenticated-orcid":false,"given":"Iason","family":"Marmanis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-662-46681-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353\u2013367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL 2014, pp. 373\u2013384. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535845","DOI":"10.1145\/2535838.2535845"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., L\u00e5ang, M., Ngo, T.P., Sagonas, K.: Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3, 150:1\u2013150:29 (2019). https:\/\/doi.org\/10.1145\/3360576","DOI":"10.1145\/3360576"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-41540-6_8","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2(OOPSLA), 135:1\u2013135:29 (2018). https:\/\/doi.org\/10.1145\/3276505","DOI":"10.1145\/3276505"},{"key":"12_CR6","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_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-319-63387-9_26","volume-title":"Computer Aided Verification","author":"E Albert","year":"2017","unstructured":"Albert, E., Arenas, P., de la Banda, M.G., G\u00f3mez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 526\u2013543. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_26"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-319-96142-2_24","volume-title":"Computer Aided Verification","author":"E Albert","year":"2018","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Isabel, M., Rubio, A.: Constrained dynamic partial order reduction. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 392\u2013410. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_24"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-319-89963-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Aronis","year":"2018","unstructured":"Aronis, S., Jonsson, B., L\u00e5ng, M., Sagonas, K.: Optimal dynamic partial order reduction with observers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 229\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_14"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., Vaidya, K.: Datacentric dynamic partial order reduction. Proc. ACM Program. Lang. 2(POPL), 31:1\u201331:30 (2017). https:\/\/doi.org\/10.1145\/3158119","DOI":"10.1145\/3158119"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Pavlogiannis, A., Toman, V.: Value-centric dynamic partial order reduction. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360550","DOI":"10.1145\/3360550"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL 2005, pp. 110\u2013121. ACM, New York (2005). https:\/\/doi.org\/10.1145\/1040305.1040315","DOI":"10.1145\/1040305.1040315"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Jonsson, B., L\u00e5ng, M., Sagonas, K.: Awaiting for Godot: stateless model checking that avoids executions where nothing happens. In: FMCAD 2022, pp. 163\u2013172. TU Wien Academic Press (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_35","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_35"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Marmanis, I., Gladstein, V., Vafeiadis, V.: Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498711","DOI":"10.1145\/3498711"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Effective lock handling in stateless model checking. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360599","DOI":"10.1145\/3360599"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: PLDI 2019. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314609","DOI":"10.1145\/3314221.3314609"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Ren, X., Vafeiadis, V.: Dynamic partial order reductions for spinloops. In: FMCAD 2021, pp. 163\u2013172. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_25","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_25"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-030-81685-8_20","volume-title":"Computer Aided Verification","author":"M Kokologiannakis","year":"2021","unstructured":"Kokologiannakis, M., Vafeiadis, V.: GenMC: a model checker for weak memory models. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 427\u2013440. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Vafeiadis, V.: HMC: model checking for hardware memory models. In: ASPLOS 2020, pp. 1157\u20131171. ACM, Lausanne, Switzerland (2020). https:\/\/doi.org\/10.1145\/3373376.3378480","DOI":"10.1145\/3373376.3378480"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., Vafeiadis, V.: Making weak memory models fair. Proc. ACM Program. Lang. 5(OOPSLA) (2021). https:\/\/doi.org\/10.1145\/3485475","DOI":"10.1145\/3485475"},{"key":"12_CR22","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. ACM, Barcelona, Spain (2017). https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Norris, B., Demsky, B.: CDSChecker: checking concurrent data structures written with C\/C++ atomics. In: OOPSLA 2013, pp. 131\u2013150. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509514","DOI":"10.1145\/2509136.2509514"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Oberhauser, J., et al.: VSync: push-button verification and optimization for synchronization primitives on weak memory models. In: ASPLOS 2021 - Virtual, pp. 530\u2013545. ACM, USA (2021). https:\/\/doi.org\/10.1145\/3445814.3446748","DOI":"10.1145\/3445814.3446748"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:05:26Z","timestamp":1704452726000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}