{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T23:08:19Z","timestamp":1721862499711},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,8,17]],"date-time":"2017-08-17T00:00:00Z","timestamp":1502928000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Linnaeus centre of excellence UPMARC"},{"name":"EU FP7 STREP project RELEASE","award":["287510"]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2017,8,31]]},"abstract":"\n Stateless model checking is a powerful method for program verification that, however, suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, we present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called\n source sets<\/jats:italic>\n , that replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple-to-implement algorithm, called\n source-DPOR<\/jats:italic>\n . Subsequently, we enhance this algorithm with a novel mechanism, called\n wakeup trees<\/jats:italic>\n , that allows the resulting algorithm, called\n optimal-DPOR<\/jats:italic>\n , to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, for example, via locks. Finally, we discuss tradeoffs of the source- and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs, while the source-DPOR algorithm is at the core of a publicly available stateless model checking tool for C\/pthread programs running on machines with relaxed memory models. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.\n <\/jats:p>","DOI":"10.1145\/3073408","type":"journal-article","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T11:49:04Z","timestamp":1503575344000},"page":"1-49","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Source Sets"],"prefix":"10.1145","volume":"64","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"given":"Stavros","family":"Aronis","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"given":"Konstantinos","family":"Sagonas","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2017,8,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810891.1810910"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40447-4_19"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.50"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and Patrice Godefroid. 2005a. Addendum to Dynamic Partial-order Reduction for Model Checking Software. Retrieved from http:\/\/research.microsoft.com\/en-us\/um\/people\/pg\/ Cormac Flanagan and Patrice Godefroid. 2005a. Addendum to Dynamic Partial-order Reduction for Model Checking Software. Retrieved from http:\/\/research.microsoft.com\/en-us\/um\/people\/pg\/","DOI":"10.1145\/1047659.1040315"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Patrice 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. Patrice 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.","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384077"},{"key":"e_1_2_1_15_1","volume-title":"LCNS","volume":"697","author":"Godefroid Patrice","year":"1993"},{"key":"e_1_2_1_16_1","volume-title":"LCNS","volume":"575","author":"Godefroid Patrice","year":"1991"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351698"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_21"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90054-J"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092287"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_22"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.56"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Workshop on Parallel and Distributed Algorithms, M. Cosnard et al. (Ed.). North-Holland\/Elsevier, 215--226","author":"Mattern Friedemann","year":"1989"},{"key":"e_1_2_1_28_1","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"Mazurkiewicz Antoni"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)","author":"Musuvathi Madanlal","year":"2008"},{"key":"e_1_2_1_32_1","volume-title":"LNCS","volume":"697","author":"Peled Doron","year":"1993"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 26th International Conference on Concurrency Theory (CONCUR\u201915)","volume":"42","author":"Sousa Marcelo","year":"2015"},{"key":"e_1_2_1_35_1","volume-title":"Artificial Intelligence: A Modern Approach","author":"Russell Stuart","year":"2009","edition":"3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2012.18"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_25"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763218.1763234"},{"key":"e_1_2_1_39_1","volume-title":"Third International Conference, RV","volume":"7687","author":"Serbanuta Traian-Florin","year":"2012"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_14"},{"key":"e_1_2_1_41_1","volume-title":"Advances in Petri Nets","author":"Valmari Antti","year":"1990"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3073408","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T07:14:24Z","timestamp":1672470864000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3073408"}},"subtitle":["A Foundation for Optimal Dynamic Partial Order Reduction"],"short-title":[],"issued":{"date-parts":[[2017,8,17]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,8,31]]}},"alternative-id":["10.1145\/3073408"],"URL":"https:\/\/doi.org\/10.1145\/3073408","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,17]]},"assertion":[{"value":"2016-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-08-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}