Advertisement

MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings

(Competition Contribution)
  • Ermenegildo TomascoEmail author
  • 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 CSeq module that implements improved algorithms for the verification of multi-threaded C programs with dynamic thread creation. It is based on sequentializing the programs according to a guessed sequence of write operations in the shared memory (memory unwinding, MU). The original algorithm (implemented in MU-CSeq 0.1) stores the values of all shared variables for each write (read-explicit fine-grained MU), which requires multiple copies of the shared variables. Our new algorithms store only the writes (read-implicit MU) or only a subset of the writes (coarse-grained MU), which reduces the memory footprint of the unwinding and so allows larger unwinding bounds.

References

  1. 1.
    Fischer, B., Inverso, O., Parlato, G.: CSeq: A Sequentialization Tool for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 616–618. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Fischer, B., Inverso, O., Parlato, G.: CSeq: A Concurrency Pre-Processor for Sequential C Verification Tools. In: ASE, pp. 710–713 (2013)Google Scholar
  3. 3.
    Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: A Lazy Sequentialization Tool for C. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 398–401. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  4. 4.
    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
  5. 5.
    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
  6. 6.
    Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 402–404. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  7. 7.
    Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Verifying Concurrent Programs by Memory Unwinding. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 551–565. Springer, Heidelberg (2015)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Ermenegildo Tomasco
    • 1
    Email author
  • 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.Dipartimento di InformaticaUniversità di SalernoFiscianoItaly

Personalised recommendations