Advertisement

Verifying Concurrent Programs by Memory Unwinding

  • Ermenegildo Tomasco
  • Omar Inverso
  • Bernd Fischer
  • Salvatore La Torre
  • Gennaro Parlato
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)

Abstract

We describe a new sequentialization-based approach to the symbolic verification of multithreaded programs with shared memory and dynamic thread creation. Its main novelty is the idea of memory unwinding (MU), i.e., a sequence of write operations into the shared memory. For the verification, we nondeterministically guess an MU and then simulate the behavior of the program according to any scheduling that respects it. This approach is complementary to other sequentializations and explores an orthogonal dimension, i.e., the number of write operations. It also simplifies the implementation of several important optimizations, in particular the targeted exposure of individual writes. We implemented this approach as a code-to-code transformation from multithreaded into nondeterministic sequential programs, which allows the reuse of sequential verification tools. Experiments show that our approach is effective: it found all errors in the concurrency category of SV-COMP15.

References

  1. 1.
    Alglave, J., Kroening, D., Tautschnig, M.: Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99–115. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  3. 3.
    Beyer, D.: SV-COMP home page, http://sv-comp.sosy-lab.org/
  4. 4.
    Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 451–465. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  5. 5.
    Bouajjani, A., Emmi, M., Parlato, G.: On Sequentializing Concurrent Programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 129–145. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Chaki, S., Gurfinkel, A., Strichman, O.: Time-bounded analysis of real-time systems. In: FMCAD, pp. 72–80 (2011)Google Scholar
  7. 7.
    Clarke, E.M., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. POPL, 411–422 (2011)Google Scholar
  9. 9.
    Fischer, B., Inverso, O., Parlato, G.: CSeq: A Concurrency Pre-Processor for Sequential C Verification Tools. In: ASE, pp. 710-713 (2013)Google Scholar
  10. 10.
    Fischer, B., Inverso, O., Parlato, G.: CSeq: A Sequentialization Tool for C (Competition Contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 616–618. Springer, Heidelberg (2013)Google Scholar
  11. 11.
    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, Heidelberg (2014)CrossRefGoogle Scholar
  12. 12.
    Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 398–401. Springer, Heidelberg (2014)Google Scholar
  13. 13.
    La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477–492. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Lahiri, S.K., Qadeer, S., Rakamaric, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 509–524. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  16. 16.
    Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design 35(1), 73–97 (2009)CrossRefzbMATHGoogle Scholar
  17. 17.
    Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. SIGOPS Oper. Syst. Rev. 42(2), 329–339 (2008)CrossRefGoogle Scholar
  18. 18.
    Qadeer, S.: Poirot - a concurrency sleuth. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, p. 15. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI, pp. 14–24 (2004)Google Scholar
  21. 21.
    Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 402–404. Springer, Heidelberg (2014)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Ermenegildo Tomasco
    • 1
  • Omar Inverso
    • 1
  • Bernd Fischer
    • 2
  • Salvatore La Torre
    • 3
  • Gennaro Parlato
    • 1
  1. 1.Electronics and Computer ScienceUniversity of SouthamptonSouthamptonUK
  2. 2.Division of Computer ScienceStellenbosch UniversityStellenboschSouth Africa
  3. 3.Università degli Studi di SalernoSalernoItaly

Personalised recommendations