{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:58:43Z","timestamp":1781027923562,"version":"3.54.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","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,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"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>\n                  <jats:p>\n                    There are two major techniques for scaling up stateless model checking:\n                    <jats:italic>dynamic partial order reduction<\/jats:italic>\n                    (DPOR), which only explores executions that differ in the ordering of racy accesses, and\n                    <jats:italic>preemption bounding<\/jats:italic>\n                    , which only explores executions containing up to\n                    <jats:italic>k<\/jats:italic>\n                    preemptions (preemptive context-switches).\n                  <\/jats:p>\n                  <jats:p>Combining these two techniques is challenging because DPOR-equivalent executions often contain a different number of preemptions, making it incorrect to cut explorations that exceed the preemption bound. To restore completeness, prior work has weakened the DPOR algorithm, which often results in the exploration of many redundant executions.<\/jats:p>\n                  <jats:p>We propose an alternative approach. Starting from an optimal DPOR algorithm, we achieve completeness by allowing some slack on the preemption-bound of the explored executions. We prove that the required slack does not exceed the number of threads of the program (minus two), and that this upper limit is tight.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_5","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"85-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Reconciling Preemption Bounding with DPOR"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5077-5275","authenticated-orcid":false,"given":"Iason","family":"Marmanis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. \u201cStateless model checking for TSO and PSO\u201d. In: TACAS 2015. Vol. 9035. LNCS. Berlin, Heidelberg: Springer, 2015, pp. 353\u2013367. doi: https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28. url: http:\/\/dx.doi.org\/10.1007\/978-3-662-46681-0_28.","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. \u201cOptimal dynamic partial order reduction\u201d. In: POPL 2014. New York, NY, USA: ACM, 2014, pp. 373\u2013384. doi: https:\/\/doi.org\/10.1145\/2535838.2535845. url: http:\/\/doi.acm.org\/10.1145\/2535838.2535845.","DOI":"10.1145\/2535838.2535845"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. \u201cContext-Bounded Analysis for POWER\u201d. In: TACAS 2017. Ed. by Axel Legay and Tiziana Margaria. Berlin, Heidelberg: Springer Berlin Heidelberg, 2017, pp. 56\u201374. isbn: 978-3-662-54580-5. doi: https:\/\/doi.org\/10.1007\/978-3-662-54580-5_4.","DOI":"10.1007\/978-3-662-54580-5_4"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. \u201cStateless model checking for POWER\u201d. In: CAV 2016. Vol. 9780. LNCS. Berlin, Heidelberg: Springer, 2016, pp. 134\u2013156. doi: https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8.","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. \u201cOptimal stateless model checking under the release-acquire semantics\u201d. In: Proc. ACM Program. Lang. 2. OOPSLA (Oct. 2018), 135:1\u2013135:29. issn: 2475-1421. doi: https:\/\/doi.org\/10.1145\/3276505. url: http:\/\/doi.acm.org\/10.1145\/3276505.","DOI":"10.1145\/3276505"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. \u201cStateless Model Checking Under a Reads-Value-From Equivalence\u201d. In: CAV 2021. Ed. by Alexandra Silva and K. Rustan M. Leino. Cham: Springer International Publishing, July 2021, pp. 341\u2013366. isbn: 978-3-030-81685-8. doi: https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16.","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. \u201cContext-Bounded Analysis of TSO Systems\u201d. In: FPS 2014. Ed. by Saddek Bensalem, Yassine Lakhneck, and Axel Legay. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, pp. 21\u201338. isbn: 978-3-642-54848-2. doi: https:\/\/doi.org\/10.1007\/978-3-642-54848-2_2.","DOI":"10.1007\/978-3-642-54848-2_2"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. \u201cData-centric dynamic partial order reduction\u201d. In: Proc. ACM Program. Lang. 2.POPL (Dec. 2017), 31:1\u201331:30. issn: 2475-1421. doi: https:\/\/doi.org\/10.1145\/3158119. url: http:\/\/doi.acm.org\/10.1145\/3158119.","DOI":"10.1145\/3158119"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. \u201cValue-Centric Dynamic Partial Order Reduction\u201d. In: Proc. ACM Program. Lang. 3.OOPSLA (Oct. 2019). doi: https:\/\/doi.org\/10.1145\/3360550. url: https:\/\/doi.org\/10.1145\/3360550.","DOI":"10.1145\/3360550"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Katherine E. Coons, Madan Musuvathi, and Kathryn S. McKinley. \u201cBounded Partial-Order Reduction\u201d. In: OOPSLA 2013. Indianapolis, Indiana, USA: ACM, 2013, pp. 833\u2013848. isbn: 9781450323741. doi: https:\/\/doi.org\/10.1145\/2509136.2509556.","DOI":"10.1145\/2509136.2509556"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Cormac Flanagan and Patrice Godefroid. \u201cDynamic partial-order reduction for model checking software\u201d. In: POPL 2005. New York, NY, USA: ACM, 2005, pp. 110\u2013121. doi: https:\/\/doi.org\/10.1145\/1040305.1040315. url: http:\/\/doi.acm.org\/10.1145\/1040305.1040315.","DOI":"10.1145\/1040305.1040315"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Patrice Godefroid. \u201cModel checking for programming languages using VeriSoft\u201d. In: POPL 1997. Paris, France: ACM, 1997, pp. 174\u2013186. doi: https:\/\/doi.org\/10.1145\/263699.263717. url: http:\/\/doi.acm.org\/10.1145\/263699.263717.","DOI":"10.1145\/263699.263717"},{"key":"5_CR13","unstructured":"Maurice Herlihy and Nir Shavit. The art of multiprocessor programming. 2008."},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Jeff Huang. \u201cStateless model checking concurrent programs with maximal causality reduction\u201d. In: PLDI 2015. New York, NY, USA: ACM, 2015, pp. 165\u2013174. doi: https:\/\/doi.org\/10.1145\/2737924.2737975. url: http:\/\/doi.acm.org\/10.1145\/2737924.2737975.","DOI":"10.1145\/2737924.2737975"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. \u201cEffective stateless model checking for C\/C++ concurrency\u201d. In: Proc. ACM Program. Lang. 2.POPL (Dec. 2017), 17:1\u201317:32. issn: 2475-1421. doi: 10.1145\/3158105. url: http:\/\/doi.acm.org\/10.1145\/3158105.","DOI":"10.1145\/3158105"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. \u201cTruly stateless, optimal dynamic partial order reduction\u201d. In: Proc. ACM Program. Lang. 6.POPL (Jan. 2022). doi: https:\/\/doi.org\/10.1145\/3498711.","DOI":"10.1145\/3498711"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. \u201cModel checking for weakly consistent libraries\u201d. In: PLDI 2019. New York, NY, USA: ACM, 2019. doi: https:\/\/doi.org\/10.1145\/3314221.3314609.","DOI":"10.1145\/3314221.3314609"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Michalis Kokologiannakis and Viktor Vafeiadis. \u201cGenMC: A model checker for weak memory models\u201d. In: CAV 2021. Ed. by Alexandra Silva and K. Rustan M. Leino. Vol. 12759. LNCS. Springer, 2021, pp. 427\u2013440. doi: https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20.","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Michalis Kokologiannakis and Viktor Vafeiadis. \u201cHMC: Model checking for hardware memory models\u201d. In: ASPLOS 2020. ASPLOS \u201920. Lausanne, Switzerland: ACM, 2020, pp. 1157\u20131171. isbn: 9781450371025. doi: https:\/\/doi.org\/10.1145\/3373376.3378480.","DOI":"10.1145\/3373376.3378480"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. \u201cRepairing sequential consistency in C\/C++11\u201d. In: PLDI 2017. Barcelona, Spain: ACM, 2017, pp. 618\u2013632. isbn: 978-1-4503-4988-8. doi: https:\/\/doi.org\/10.1145\/3062341.3062352. url: http:\/\/doi.acm.org\/10.1145\/3062341.3062352.","DOI":"10.1145\/3062341.3062352"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis. \u201cReconciling Preemption Bounding with DPOR (artifact)\u201d. In: (Apr. 2023). doi: https:\/\/doi.org\/10.5281\/zenodo.7505917.","DOI":"10.5281\/zenodo.7505917"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis. \u201cReconciling Preemption Bounding with DPOR (supplementary material)\u201d. In: (Apr. 2023). url: https:\/\/plv.mpi-sws.org\/genmc.","DOI":"10.1007\/978-3-031-30823-9_5"},{"key":"5_CR23","unstructured":"Madalan Musuvathi and Shaz Qadeer. Partial-Order Reduction for Context-Bounded State Exploration. Tech. rep. MSR-TR-2007-12. Microsoft Research, 2007. url: https:\/\/www.microsoft.com\/en-us\/research\/wpcontent\/uploads\/2016\/02\/tr-2007-12.pdf."},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Madanlal Musuvathi and Shaz Qadeer. \u201cIterative Context Bounding for Systematic Testing of Multithreaded Programs\u201d. In: PLDI 2007. San Diego, California, USA: ACM, 2007, pp. 446\u2013455. isbn: 9781595936332. doi: https:\/\/doi.org\/10.1145\/1250734.1250785.","DOI":"10.1145\/1250734.1250785"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Shaz Qadeer and Jakob Rehof. \u201cContext-Bounded Model Checking of Concurrent Software\u201d. In: TACAS 2005. Ed. by Nicolas Halbwachs and Lenore D. Zuck. Vol. 3440. LNCS. Springer, 2005, pp. 93\u2013107. doi: https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7.","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"5_CR26","unstructured":"SV-COMP. Competition on Software Verification (SV-COMP). 2019. url: https:\/\/sv-comp.sosy-lab.org\/2019\/ (visited on 03\/27\/2019)."},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Paul Thomson, Alastair F. Donaldson, and Adam Betts. \u201cConcurrency testing using schedule bounding: an empirical study\u201d. In: PPoPP 2014. ACM, 2014, pp. 15\u201328. doi: https:\/\/doi.org\/10.1145\/2555243.2555260.","DOI":"10.1145\/2555243.2555260"},{"key":"5_CR28","unstructured":"R. Kent Treiber. Systems Programming: Coping with Parallelism. Tech. rep. Technical Report RJ5118, IBM, 1986. url: https:\/\/dominoweb.draco.res.ibm.com\/58319a2ed2b1078985257003004617ef.html."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:06:30Z","timestamp":1781024790000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_5","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":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","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":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}