Advertisement

Combining sequentialization-based verification of multi-threaded C programs with symbolic Partial Order Reduction

  • Vladimir HerdtEmail author
  • Hoang M. Le
  • Daniel Große
  • Rolf Drechsler
Regular Paper

Abstract

Sequentialization has been shown to be an effective symbolic verification technique for safety properties in multi-threaded C programs using POSIX threads. The tool Lazy-CSeq, which applies a lazy sequentialization scheme, demonstrated its efficiency by ranking top places within the concurrency division of the Competitions on Software Verification in recent years. This lazy sequentialization scheme encodes all thread schedules up to a given exploration bound into a single non-deterministic sequential C program. Another particularly effective technique to tackle the state explosion of multi-threaded programs is Partial Order Reduction (POR). It works by limiting the exploration of redundant thread execution orders (i.e., schedules) by exploiting independence. Integrating POR into lazy sequentialization can further significantly improve its scalability. However, a combination of both techniques can lead to unsoundness, i.e., reachability of states is not preserved within the exploration bound. The reason is that POR is not aware of the exploration bound; therefore, POR can prune a schedule which will reach a bug within the exploration bound and instead keep another (functionally) equivalent schedule which requires a larger exploration bound to reach the bug. This paper presents a novel implementation of lazy sequentialization, which integrates symbolic POR into the encoding to prune redundant schedules. An efficient pruning check is employed to make the POR technique aware of the exploration bound and thus avoid unsoundness, while still providing significant state space reductions. On the other hand, the integration of POR entails some additional encoding overhead that can also result in a performance slowdown. Such a case is avoided by a practical heuristic that only employs POR if the encoding overhead of POR is reasonable (i.e., less than 50%). Experimental evaluation shows that our proposed approach can provide considerable speed-ups.

Keywords

Verification Multi-threading Partial order reduction Sequentialization Context bounded analysis Bounded model checking 

Notes

References

  1. 1.
    Alglave, J., Kroening, D., Tautschnig, M.: Partial Orders for Efficient Bounded Model Checking of Concurrent Software, pp. 141–157. Springer, Berlin (2013)Google Scholar
  2. 2.
    Andersen, L.O.: Program analysis and specialization for the C programming language. Dissertation, University of Copenhagen (1994)Google Scholar
  3. 3.
    Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004-Concurrency Theory, pp. 1–15. Springer, Berlin (2004)Google Scholar
  4. 4.
    Beyer, D.: Software Verification with Validation of Results, pp. 331–349. Springer, Berlin (2017)Google Scholar
  5. 5.
    Beyer, D., Friedberger, K.: A light-weight approach for verifying multi-threaded programs with CPAchecker. Electron. Proc. Theor. Comput. Sci. 233, 61–71 (2016)CrossRefGoogle Scholar
  6. 6.
    Beyer, D., Keremoglu, M .E.: CPAchecker: A Tool for Configurable Software Verification, pp. 184–190. Springer, Berlin (2011)Google Scholar
  7. 7.
    Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking system C. TCAD 32(5), 774–787 (2013)zbMATHGoogle Scholar
  8. 8.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Lecture Notes in Computer Science, vol. 2988 , pp. 168–176. Springer, Berlin (2004)Google Scholar
  9. 9.
    Coons, K.E., Musuvathi, M., McKinley, K.S.: Bounded partial-order reduction. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA’13, pp. 833–848. ACM, New York (2013)Google Scholar
  10. 10.
    Cordeiro, L., Fischer, B.: Verifying multi-threaded software using smt-based context-bounded model checking. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, pp. 331–340. ACM, New York (2011)Google Scholar
  11. 11.
    Cordeiro, L., Morse, J., Nicole, D., Fischer, B.: Context-Bounded Model Checking with ESBMC 1.17, pp. 534–537. Springer, Berlin (2012)Google Scholar
  12. 12.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’05, pp. 110–121. ACM, New York (2005)Google Scholar
  13. 13.
    Ghafari, N., Hu, A.J., Rakamarić, Z.: Context-bounded translations for concurrent software: an empirical evaluation. In: Proceedings of the 17th International SPIN Conference on Model Checking Software, SPIN’10, pp. 227–244. Springer, Berlin (2010)Google Scholar
  14. 14.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Secaucus (1996)CrossRefzbMATHGoogle Scholar
  15. 15.
    Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, pp. 290–299. ACM, New York (2007)Google Scholar
  16. 16.
    Herdt, V., Le, H., Große, D., Drechsler, R.: Lazy-cseq-sp: boosting sequentialization-based verification of multi-threaded c programs via symbolic pruning of redundant schedules. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 9364, pp. 228–233. Springer, Berlin (2015)Google Scholar
  17. 17.
    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.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 8559, pp. 585–602. Springer, Berlin (2014)Google Scholar
  18. 18.
    Inverso, O., Tomasco, E., Fischer, B., Torre, S.L., Parlat, G.: Lazy-CSeq 0.6c: An Improved Lazy Sequentialization Tool for C. University of Southampton, Southampton (2014)Google Scholar
  19. 19.
    Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In: Proceedings of the 21st International Conference on Computer Aided Verification, CAV ’09, pp. 398–413. Springer, Berlin (2009)Google Scholar
  20. 20.
    La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643, pp. 477–492. Springer, Berlin (2009)Google Scholar
  21. 21.
    Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35(1), 73–97 (2009)CrossRefzbMATHGoogle Scholar
  22. 22.
    Le, H.M., Große, D., Herdt, V., Drechsler, R.: Verifying SystemC using an intermediate verification language and symbolic simulation. In: DAC, pp. 116:1–116:6 (2013)Google Scholar
  23. 23.
    Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Mazurkiewicz. A.: Trace theory. In: Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency, pp. 279–324. Springer, New York (1987)Google Scholar
  25. 25.
    Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, pp. 446–455. ACM, New York (2007)Google Scholar
  26. 26.
    Musuvathi, M., Qadeer, S.: Partial-order reduction for context-bounded state exploration. Technical Report MSR-TR-2007-12. Microsoft Research, Jan 2007Google Scholar
  27. 27.
    Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3440, pp. 93–107. Springer, Berlin (2005)Google Scholar
  28. 28.
    Qadeer, S., Wu, D.: Kiss: Keep it simple and sequential. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI ’04, pp. 14–24. ACM, New York (2004)Google Scholar
  29. 29.
    Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 489–504. Springer, Berlin (2003)Google Scholar
  30. 30.
    Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Groce, A., Musuvathi, M. (eds.) Model Checking Software. Lecture Notes in Computer Science, vol. 6823, pp. 57–74. Springer, Berlin (2011)Google Scholar
  31. 31.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990, pp. 491–515. Springer, Berlin (1991)CrossRefGoogle Scholar
  32. 32.
    Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pp. 382–396. Springer, Berlin (2008)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Vladimir Herdt
    • 1
    Email author
  • Hoang M. Le
    • 1
  • Daniel Große
    • 1
    • 2
  • Rolf Drechsler
    • 1
    • 2
  1. 1.Group of Computer ArchitectureUniversity of BremenBremenGermany
  2. 2.Cyber-Physical Systems, DFKI GmbHBremenGermany

Personalised recommendations