Skip to main content
SpringerLink
Log in

Extracting Safe Thread Schedules from Incomplete Model Checking Results

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11636))

Included in the following conference series:

Abstract

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 towards 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—somewhat surprisingly—even leads to faster executions.

P. Metzler—Supported by the German Academic Exchange Service (DAAD).

N. Suri—Research supported in part by H2020-SU-ICT-2018-2 CONCORDIA GA 830927 and BMBF-Hessen TUD CRISP.

G. Weissenbacher—Supported by the Vienna Science and Technology Fund (WWTF) through grant VRG11-005 and the Austrian Science Fund (FWF) via the Austrian National Research Network S11403-N23 (RiSE).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    E.g., Pthread mutexes, some uses of the address-of operator, and reuse of the same function by several threads are not supported. We solve these issues by rewriting our benchmark programs so that Impara handles them correctly and their intuitive semantics is not changed. We will publish our modifications to Impara, including two bug fixes.

  2. 2.

    As enforcing an IVR is redundant to synchronization over existing mutexes and barriers, omitting them is safe.

  3. 3.

    Opt2 follows a general algorithm, however we do not automate our implementation of Opt2, as it would be a large effort to implement compiler optimizations. Our implementation of Opt1 is automated.

  4. 4.

    As Impara cannot handle several features used by pfscan (such as condition variables, structs, and standard output), we manually generate initial IVRs.

References

  1. Benchmark suite of the competition on software verification (SV-COMP). https://github.com/sosy-lab/sv-benchmarks

  2. Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 204–219. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_15

    Chapter  Google Scholar 

  3. Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 530–536. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_37

    Chapter  Google Scholar 

  4. Aviram, A., Weng, S., Hu, S., Ford, B.: Efficient system-enforced deterministic parallelism. In: OSDI. USENIX Association (2010)

    Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  6. Bergan, T., Anderson, O., Devietti, J., Ceze, L., Grossman, D.: CoreDet: a compiler and runtime system for deterministic multithreaded execution. In: ASPLOS. ACM (2010)

    Google Scholar 

  7. Bergan, T., Ceze, L., Grossman, D.: Input-covering schedules for multithreaded programs. In: OOPSLA (2013)

    Article  Google Scholar 

  8. Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: FSE. ACM (2012)

    Google Scholar 

  9. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  10. Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2(3), 279–287 (1999)

    Article  Google Scholar 

  11. Cui, H., et al.: Parrot: a practical runtime for deterministic, stable, and reliable threads. In: SOSP. ACM (2013)

    Google Scholar 

  12. Cui, H., Wu, J., Gallagher, J., Guo, H., Yang, J.: Efficient deterministic multithreading through schedule relaxation. In: SOSP. ACM (2011)

    Google Scholar 

  13. Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: ICS. ACM (2003)

    Google Scholar 

  14. Fischer, B., Inverso, O., Parlato, G.: CSeq: a concurrency pre-processor for sequential C verification tools. In: ASE. IEEE (2013)

    Google Scholar 

  15. Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45927-8_19

    Chapter  Google Scholar 

  16. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL. ACM (2005)

    Article  Google Scholar 

  17. Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60761-7

    Book  MATH  Google Scholar 

  18. Günther, H., Laarman, A., Sokolova, A., Weissenbacher, G.: Dynamic reductions for model checking concurrent software. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 246–265. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_14

    Chapter  MATH  Google Scholar 

  19. Gupta, A., Henzinger, T.A., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL. ACM (2015)

    Google Scholar 

  20. Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI. ACM (2004)

    Google Scholar 

  21. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70. ACM (2002)

    Google Scholar 

  22. Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585–602. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_39

    Chapter  Google Scholar 

  23. Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 573–578. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_45

    Chapter  Google Scholar 

  24. Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: FMCAD. IEEE (2010)

    Google Scholar 

  25. Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73–97 (2009)

    Article  Google Scholar 

  26. Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 339–353. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_24

    Chapter  MATH  Google Scholar 

  27. Liu, T., Curtsinger, C., Berger, E.D.: DTHREADS: efficient deterministic multithreading. In: SOSP. ACM (2011)

    Google Scholar 

  28. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_14

    Chapter  Google Scholar 

  29. Metzler, P., Saissi, H., Bokor, P., Suri, N.: Quick verification of concurrent programs by iteratively relaxed scheduling. In: ASE. IEEE Computer Society (2017)

    Google Scholar 

  30. 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)

    Google Scholar 

  31. Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI. ACM (2007)

    Google Scholar 

  32. Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy sequentialization for the safety verification of unbounded concurrent programs. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 174–191. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_12

    Chapter  Google Scholar 

  33. 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)

    Google Scholar 

  34. Olszewski, M., Ansel, J., Amarasinghe, S.P.: Kendo: efficient deterministic multithreading in software. In: ASPLOS (2009)

    Article  Google Scholar 

  35. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_7

    Chapter  MATH  Google Scholar 

  36. Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI. ACM (2004)

    Google Scholar 

  37. Raychev, V., Vechev, M., Yahav, E.: Automatic synthesis of deterministic concurrency. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 283–303. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_16

    Chapter  Google Scholar 

  38. Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-65306-6_21

    Chapter  Google Scholar 

  39. Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: FMCAD. IEEE (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Darmstadt, Darmstadt, Germany

    Patrick Metzler & Neeraj Suri

  2. TU Wien, Vienna, Austria

    Georg Weissenbacher

Authors
  1. Patrick Metzler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Neeraj Suri
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Georg Weissenbacher
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Patrick Metzler .

Editor information

Editors and Affiliations

  1. Avast Software, Prague, Czech Republic

    Fabrizio Biondi

  2. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Thomas Given-Wilson

  3. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Axel Legay

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Metzler, P., Suri, N., Weissenbacher, G. (2019). Extracting Safe Thread Schedules from Incomplete Model Checking Results. In: Biondi, F., Given-Wilson, T., Legay, A. (eds) Model Checking Software. SPIN 2019. Lecture Notes in Computer Science(), vol 11636. Springer, Cham. https://doi.org/10.1007/978-3-030-30923-7_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30923-7_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30922-0

  • Online ISBN: 978-3-030-30923-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation