Skip to main content
SpringerLink
Log in

Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models

  • Conference paper
  • First Online:
Book cover Software Engineering and Formal Methods (SEFM 2017)

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

Included in the following conference series:

Abstract

Sequentialization translates concurrent programs into equivalent nondeterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. However, existing sequentializations assume sequential consistency, which modern hardware architectures no longer guarantee. Here we describe a new approach to embed weak memory models within eager sequentializations. Our approach is based on the separation of intra-thread computations from inter-thread communications by means of a shared memory abstraction (SMA). We give details of SMA implementations for the SC, TSO, and PSO memory models that are based on the idea of individual memory unwindings. We use our approach to implement a new, efficient BMC-based bug finding tool for multi-threaded C programs under SC, TSO, or PSO based on these SMAs, and show experimentally that it is competitive to existing tools.

Partially supported by EPSRC EP/M008991/1, and MIUR-FARB 2014-2016 grants.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    http://users.ecs.soton.ac.uk/gp4/cseq/files/IMU-2017.zip.

  2. 2.

    Note that the SV-COMP16 version of MU-CSeq is a hybrid tool that already uses IMU for the shown sub-categories. We thus use the SV-COMP15 version here.

References

  1. Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353–367. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_28

    Chapter  MATH  Google Scholar 

  2. Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 56–74. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54580-5_4

    Chapter  Google Scholar 

  3. Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. In: IEEE PDP, pp. 332–341 (2014)

    Google Scholar 

  4. Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512–532. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37036-6_28

    Chapter  Google Scholar 

  5. Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: CAV, pp. 141–157 (2013)

    Chapter  Google Scholar 

  6. Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1–7:74 (2014)

    Article  Google Scholar 

  7. 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). doi:10.1007/978-3-642-22110-1_9

    Chapter  Google Scholar 

  8. Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (Report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_55

    Chapter  Google Scholar 

  9. Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 267–282. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46675-9_18

    Chapter  Google Scholar 

  10. Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: ICSE, pp. 589–592 (2016)

    Google Scholar 

  11. Chen, G., Jin, H., Zou, D., Zhou, B.B., Liang, Z., Zheng, W., Shi, X.: Safestack: automatically patching stack-based buffer overflow vulnerabilities. IEEE Trans. Dependable Sec. Comput. 10(6), 368–379 (2013)

    Article  Google Scholar 

  12. Horn, A., Kroening, D.: On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 19–34. Springer, Cham (2015). doi:10.1007/978-3-319-19195-9_2

    Chapter  MATH  Google Scholar 

  13. Inverso, O., Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy-cseq: a context-bounded model checking tool for multi-threaded c-programs. In: ASE, pp. 807–812 (2015)

    Google Scholar 

  14. 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). doi:10.1007/978-3-319-08867-9_39

    Chapter  Google Scholar 

  15. La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: CAV, pp. 629–644 (2010)

    Google Scholar 

  16. La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing Parameterized Programs. In: FIT, pp. 34–47 (2012)

    Google Scholar 

  17. 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 

  18. Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_27

    Chapter  Google Scholar 

  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). doi:10.1007/978-3-540-31980-1_7

    Chapter  MATH  Google Scholar 

  20. Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: PPopp, pp. 15–28 (2014)

    Google Scholar 

  21. 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). doi:10.1007/978-3-662-46681-0_52

    Chapter  Google Scholar 

  22. Tomasco, E., Nguyen, T.L., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Lazy sequentialization for TSO and PSO via shared memory abstractions. In: FMCAD, pp. 193–200 (2016)

    Google Scholar 

  23. Tomasco, E., Nguyen, T.L., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq 0.4: individual memory location unwindings. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 938–941. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_65

    Chapter  Google Scholar 

  24. Wehrheim, H., Travkin, O.: TSO to SC via symbolic execution. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 104–119. Springer, Cham (2015). doi:10.1007/978-3-319-26287-1_7

    Chapter  Google Scholar 

  25. Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: PLDI, pp. 250–259 (2015)

    Article  Google Scholar 

  26. Zheng, M., Rogers, M.S., Luo, Z., Dwyer, M.B., Siegel, S.F.: CIVL: formal verification of parallel programs. In: ASE, pp. 830–835 (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Electronics and Computer Science, University of Southampton, Southampton, UK

    Ermenegildo Tomasco, Truc Lam Nguyen & Gennaro Parlato

  2. Division of Computer Science, Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  3. Dipartimento di Informatica, Università di Salerno, Fisciano, Italy

    Salvatore La Torre

Authors
  1. Ermenegildo Tomasco
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Truc Lam Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bernd Fischer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Salvatore La Torre
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Gennaro Parlato
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Truc Lam Nguyen .

Editor information

Editors and Affiliations

  1. University of Trento, Trento, Italy

    Alessandro Cimatti

  2. Mälardalen University, Västerås, Sweden

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Tomasco, E., Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G. (2017). Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models. In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66197-1_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66196-4

  • Online ISBN: 978-3-319-66197-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation