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

Moving Around: Lipton’s Reduction for TSO

(Regular Submission)

  • Conference paper
Verified Software: Theories, Tools, and Experiments (VSTTE 2015)

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

Included in the following conference series:

  • 583 Accesses

Abstract

We generalize Lipton’s reduction theory, hitherto limited to SC, for TSO programs. We demonstrate the use of our theory by specifying the conditions under which a particular write is SC-like (i.e. placing a fence immediately after the write does not constrain the behavior of the overall program) and a library implementation can be safely used (i.e. compositionality). Our theory is complete: a program has only SC behaviors iff there is a proof that establishes that every write in the program is SC-like. We adapt the notion of program abstraction to TSO analysis via our theory. We define precisely what is meant by abstraction, and propose a methodology by which one can obtain via abstraction SC summaries of a program which may have non-SC behaviors. Finally, we show how checking whether a write instruction is SC-like can be mechanized. We describe a transformation in which the execution of each thread of the original program (under TSO) is simulated by the execution of two tightly coupled threads in the new program (under SC).

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

References

  1. Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don’t sit on the fence. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508–524. Springer, Heidelberg (2014)

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

    Chapter  Google Scholar 

  4. Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50–66. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Batty, M., Dodds, M., Gotsman, A.: Library abstraction for c/c++ concurrency. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 235–248. ACM (2013)

    Google Scholar 

  6. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing c++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 55–66. ACM (2011)

    Google Scholar 

  7. Boehm, H.J. and Adve, S.V.: Foundations of the c++ concurrency memory model. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 68–78. ACM (2008)

    Google Scholar 

  8. Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Burckhardt, S., Alur, R., Martin, M.M.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007, pp. 12–21. ACM (2007)

    Google Scholar 

  10. Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107–120. Springer, Heidelberg (2008)

    Chapter  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. Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 2–15. ACM (2009)

    Google Scholar 

  13. Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267–286. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31–45. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Jagannathan, S., Laporte, V., Petri, G., Pichardie, D., Vitek, J.: Atomicity refinement for verified compilation. ACM Trans. Program. Lang. Syst. 36(2), 6 (2014)

    Article  Google Scholar 

  16. Koskinen, E., Parkinson, M., Herlihy, M.: Coarse-grained transactions. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 19–30. ACM (2010)

    Google Scholar 

  17. Lipton, R.J.: Reduction: a method of proving properties of parallel programs. ACM Commun. 18(12), 717–721 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  18. Mador-Haim, S., et al.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495–512. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Norris, B., Demsky, B.: CDSchecker: Checking concurrent data structures written with c/c++ atomics. In: Proceedings of the ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 131–150. ACM (2013)

    Google Scholar 

  20. Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478–503. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55–70. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Rinard, M.C., Diniz, P.C.: Commutativity analysis: A new analysis technique for parallelizing compilers. ACM Trans. Program. Lang. Syst. 19(6), 942–991 (1997)

    Article  Google Scholar 

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

    Article  Google Scholar 

  24. Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282–312 (1988)

    Article  Google Scholar 

  25. Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for c11 concurrency. In: Proceedings of the ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 867–884. ACM (2013)

    Google Scholar 

Download references

Acknowledgment

This work is supported by EPSRC grants EP/H005633/1, EP/ K008528/1 and TUBITAK grant 111E135.

Author information

Authors and Affiliations

  1. University of Cambridge, Cambridge, UK

    Ali Sezgin

  2. Koc University, Istanbul, Turkey

    Serdar Tasiran

Authors
  1. Ali Sezgin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Serdar Tasiran
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ali Sezgin .

Editor information

Editors and Affiliations

  1. Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, USA

    Arie Gurfinkel

  2. Department of Electrical Engineering and Computer Science, University of California, Berkeley, USA

    Sanjit A. Seshia

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Sezgin, A., Tasiran, S. (2016). Moving Around: Lipton’s Reduction for TSO. In: Gurfinkel, A., Seshia, S.A. (eds) Verified Software: Theories, Tools, and Experiments. VSTTE 2015. Lecture Notes in Computer Science(), vol 9593. Springer, Cham. https://doi.org/10.1007/978-3-319-29613-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29613-5_10

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29612-8

  • Online ISBN: 978-3-319-29613-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation