{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:56:10Z","timestamp":1780116970433,"version":"3.54.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,6,26]],"date-time":"2020-06-26T00:00:00Z","timestamp":1593129600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,6,26]],"date-time":"2020-06-26T00:00:00Z","timestamp":1593129600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Austrian Science Fund"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort toward verifying the program is wasted. We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach\u2014somewhat surprisingly\u2014even leads to faster executions.\n<\/jats:p>","DOI":"10.1007\/s10009-020-00575-y","type":"journal-article","created":{"date-parts":[[2020,6,26]],"date-time":"2020-06-26T15:45:34Z","timestamp":1593186334000},"page":"565-581","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Extracting safe thread schedules from incomplete model checking results"],"prefix":"10.1007","volume":"22","author":[{"given":"Patrick","family":"Metzler","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neeraj","family":"Suri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,26]]},"reference":[{"key":"575_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: TACAS. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_15"},{"key":"575_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: TACAS, LNCS. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_37"},{"key":"575_CR3","unstructured":"Aviram, A., Weng, S., Hu, S., Ford, B.: Efficient system-enforced deterministic parallelism. In: OSDI. USENIX Association (2010)"},{"key":"575_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"575_CR5","unstructured":"Benchmark suite of the competition on software verification (SV-COMP). https:\/\/github.com\/sosy-lab\/sv-benchmarks. Accessed 23 June 2020"},{"key":"575_CR6","doi-asserted-by":"crossref","unstructured":"Bergan, T., Anderson, O., Devietti, J., Ceze, L., Grossman, D.: Coredet: a compiler and runtime system for deterministic multithreaded execution. In: ASPLOS. ACM (2010)","DOI":"10.1145\/1736020.1736029"},{"key":"575_CR7","doi-asserted-by":"crossref","unstructured":"Bergan, T., Ceze, L., Grossman, D.: Input-covering schedules for multithreaded programs. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509508"},{"key":"575_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: FSE. ACM (2012)","DOI":"10.1145\/2393596.2393664"},{"key":"575_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.E.: Cpachecker: a tool for configurable software verification. In: CAV, LNCS, vol. 6806, pp. 184\u2013190. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"issue":"3","key":"575_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2(3), 279\u2013287 (1999)","journal-title":"STTT"},{"key":"575_CR11","doi-asserted-by":"crossref","unstructured":"Cui, H., Simsa, J., Lin, Y., Li, H., Blum, B., Xu, X., Yang, J., Gibson, G.A., Bryant, R.E.: Parrot: a practical runtime for deterministic, stable, and reliable threads. In: SOSP. ACM (2013)","DOI":"10.1145\/2517349.2522735"},{"key":"575_CR12","doi-asserted-by":"crossref","unstructured":"Cui, H., Wu, J., Gallagher, J., Guo, H., Yang, J.: Efficient deterministic multithreading through schedule relaxation. In: SOSP. ACM (2011)","DOI":"10.1145\/2043556.2043588"},{"key":"575_CR13","doi-asserted-by":"crossref","unstructured":"Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: ICS. ACM (2003)","DOI":"10.1145\/782814.782854"},{"key":"575_CR14","doi-asserted-by":"crossref","unstructured":"Fischer, B., Inverso, O., Parlato, G.: Cseq: A concurrency pre-processor for sequential C verification tools. In: ASE. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693139"},{"key":"575_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: ESOP, LNCS. Springer (2002)","DOI":"10.1007\/3-540-45927-8_19"},{"key":"575_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL. ACM (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"575_CR17","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem, LNCS","author":"P Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem, LNCS, vol. 1032. Springer, Berlin (1996)"},{"key":"575_CR18","doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Laarman, A., Sokolova, A., Weissenbacher, G.: Dynamic reductions for model checking concurrent software. In: VMCAI, LNCS. Springer (2017)","DOI":"10.1007\/978-3-319-52234-0_14"},{"key":"575_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL. ACM (2015)","DOI":"10.1145\/2676726.2677008"},{"key":"575_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI. ACM (2004)","DOI":"10.1145\/996841.996844"},{"key":"575_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"575_CR22","doi-asserted-by":"crossref","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: CAV. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"575_CR23","doi-asserted-by":"crossref","unstructured":"Kroening, D., Weissenbacher, G.: Interpolation-based software verification with wolverine. In: CAV, LNCS, vol. 6806, pp. 573\u2013578. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_45"},{"key":"575_CR24","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: FMCAD. IEEE (2010)"},{"issue":"1","key":"575_CR25","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35(1), 73\u201397 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"575_CR26","doi-asserted-by":"crossref","unstructured":"Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: TACAS, LNCS. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_24"},{"key":"575_CR27","doi-asserted-by":"crossref","unstructured":"Liu, T., Curtsinger, C., Berger, E.D.: Dthreads: efficient deterministic multithreading. In: SOSP. ACM (2011)","DOI":"10.1145\/2043556.2043587"},{"key":"575_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV, LNCS. Springer (2006)","DOI":"10.1007\/11817963_14"},{"key":"575_CR29","doi-asserted-by":"crossref","unstructured":"Metzler, P., Saissi, H., Bokor, P., Suri, N.: Quick verification of concurrent programs by iteratively relaxed scheduling. In: ASE. IEEE Computer Society (2017)","DOI":"10.1109\/ASE.2017.8115688"},{"key":"575_CR30","unstructured":"Metzler, P., Saissi, H., Bokor, P., Suri, N.: Safe execution of concurrent programs by enforcement of scheduling constraints. CoRR (2018). http:\/\/arxiv.org\/abs\/1809.01955"},{"key":"575_CR31","doi-asserted-by":"crossref","unstructured":"Metzler, P., Suri, N., Weissenbacher, G.: Extracting safe thread schedules from incomplete model checking results. In: SPIN, LNCS. Springer (2019)","DOI":"10.1007\/978-3-030-30923-7_9"},{"key":"575_CR32","doi-asserted-by":"publisher","unstructured":"Metzler, P., Suri, N., Weissenbacher, G.: Extracting Safe Thread Schedules from Incomplete Model Checking Results (2020). https:\/\/doi.org\/10.5281\/zenodo.3752957","DOI":"10.5281\/zenodo.3752957"},{"key":"575_CR33","doi-asserted-by":"crossref","unstructured":"Mushtaq, H., Al-Ars, Z., Bertels, K.: Detlock: portable and efficient deterministic execution for shared memory multicore systems. In: High Performance Computing, Networking Storage and Analysis. IEEE (2012)","DOI":"10.1109\/SC.Companion.2012.98"},{"key":"575_CR34","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI. ACM (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"575_CR35","doi-asserted-by":"crossref","unstructured":"Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy sequentialization for the safety verification of unbounded concurrent programs. In: ATVA, LNCS (2016)","DOI":"10.1007\/978-3-319-46520-3_12"},{"key":"575_CR36","doi-asserted-by":"crossref","unstructured":"Nguyen, T.L., Schrammel, P., Fischer, B., La Torre, S., Parlato, G.: Parallel bug-finding in concurrent programs via reduced interleaving instances. In: ASE. IEEE Computer Society (2017)","DOI":"10.1109\/ASE.2017.8115686"},{"key":"575_CR37","doi-asserted-by":"crossref","unstructured":"Olszewski, M., Ansel, J., Amarasinghe, S.P.: Kendo: efficient deterministic multithreading in software. In: ASPLOS (2009)","DOI":"10.1145\/1508244.1508256"},{"key":"575_CR38","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS, LNCS. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"575_CR39","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI. ACM (2004)","DOI":"10.1145\/996841.996845"},{"key":"575_CR40","doi-asserted-by":"crossref","unstructured":"Raychev, V., Vechev, M.T., Yahav, E.: Automatic synthesis of deterministic concurrency. In: SAS. Springer (2013)","DOI":"10.1007\/978-3-642-38856-9_16"},{"key":"575_CR41","volume-title":"Lectures on Petri Nets I: Basic Models, Advances in Petri Nets","author":"A Valmari","year":"1996","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models, Advances in Petri Nets. Springer, Berlin (1996)"},{"key":"575_CR42","doi-asserted-by":"crossref","unstructured":"Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: FMCAD. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679412"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00575-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00575-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00575-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,25]],"date-time":"2021-06-25T23:45:43Z","timestamp":1624664743000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00575-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,26]]},"references-count":42,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["575"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00575-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,26]]},"assertion":[{"value":"26 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}