Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

TSO to SC via Symbolic Execution

  • Conference paper
  • First Online:
Hardware and Software: Verification and Testing (HVC 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9434))

Included in the following conference series:

Abstract

Modern multi-core processors equipped with weak memory models like TSO exhibit executions which – due to store buffers – seemingly reorder program operations. Thus, they deviate from the commonly assumed sequential consistency (SC) semantics. Analysis techniques for concurrent programs consequently need to take reorderings into account. For TSO, this is often accomplished by explicitly modelling store buffers.

In this paper, we present an approach for reducing TSO-verification of concurrent programs (with fenced or write-free loops) to SC-verification, thereby being able to reuse standard verification tools. To this end, we transform a given program P into a new program \(P'\) whose SC-semantics is (bisimulation-) equivalent to the TSO-semantics of P. The transformation proceeds via a symbolic execution of P, however, only with respect to store buffer contents. Out of the thus obtained abstraction of P, we generate the SC program \(P'\) which can then be the target of standard analysis tools.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

Notes

  1. 1.

    See e.g. T. Lane. Yes, waitlatch is vulnerable to weak-memory-ordering bugs, http://www.postgresql.org/message-id/24241.1312739269@sss.pgh.pa.us, 2011.

  2. 2.

    http://www.llvm.org.

  3. 3.

    https://github.com/oleg82upb.

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)

    Google Scholar 

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

    Chapter  Google Scholar 

  3. Arora, N.S., Blumofe, R.D., Plaxton, C.G.: Thread scheduling for multiprogrammed multiprocessors. Theor. Comput. Syst. 34(2), 115–144 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  4. Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL 2010, pp. 7–18. ACM (2010)

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

  7. Bouajjani, A., Meyer, R., Möhlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 428–440. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Burns, J., Lynch, N.A.: Mutual exclusion using indivisible reads and writes. In: 18th Allerton Conference on Communication, Control, and Computing, pp. 833–842 (1980)

    Google Scholar 

  9. Cohen, E., Schirmer, B.: From total store order to sequential consistency: a practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 403–418. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)

    Article  Google Scholar 

  11. Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 84–104. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)

    Article  Google Scholar 

  13. Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)

    Google Scholar 

  14. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)

    Article  MATH  Google Scholar 

  15. Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Milner, R. (ed.): A Calculus of Communicating Systems. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  17. Pasareanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. STTT 11(4), 339–353 (2009)

    Article  Google Scholar 

  18. Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)

    Article  Google Scholar 

  19. Travkin, O., Mütze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311–326. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132–147. Springer, Heidelberg (2014)

    Google Scholar 

  21. Treiber, R.K.: Systems programming: coping with parallelism. Technical report RJ 5118, IBM Almaden Res. Ctr. (1986)

    Google Scholar 

  22. Wonisch, D., Schremmer, A., Wehrheim, H.: Programs from proofs – a PCC alternative. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 912–927. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurrency Comput. Pract. Experience 17(5–6), 465–487 (2005)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Paderborn, 33098, Paderborn, Germany

    Heike Wehrheim & Oleg Travkin

Authors
  1. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oleg Travkin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Oleg Travkin .

Editor information

Editors and Affiliations

  1. University of Leicester, Leicester, United Kingdom

    Nir Piterman

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Wehrheim, H., Travkin, O. (2015). TSO to SC via Symbolic Execution. In: Piterman, N. (eds) Hardware and Software: Verification and Testing. HVC 2015. Lecture Notes in Computer Science(), vol 9434. Springer, Cham. https://doi.org/10.1007/978-3-319-26287-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26287-1_7

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation