Skip to main content
SpringerLink
Log in

Value-Based or Conflict-Based? Opacity Definitions for STMs

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2017 (ICTAC 2017)

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

Included in the following conference series:

Abstract

Software Transactional Memory (STM) algorithms provide programmers with a high-level synchronization technique for concurrent access to shared state. STMs typically guarantee some sort of serializability: the concurrent execution of transactions appears to occur in a sequential order. With Guerraoui and Kapalka’s 2008 paper, serializability of software transactions has been phrased as opacity. While opacity has been accepted as the standard correctness criterion for STMs, later verification approaches nevertheless adopt different formulations – claiming them to be opacity.

In this paper, we study the relationships between different versions of opacity, Guerraoui and Kapalka’s value-based version and the verification-friendly, value-less conflict-based version. We show that even under some reasonable restrictions on executions, conflict-based remains stronger than value-based opacity, rejecting some serializable executions. We provide an alternative definition of conflict-based opacity, still not tracking values and thus keeping its verification-friendly style. This version, which we call constraint-based, is proven to coincide with value-based opacity. Finally, we propose a technique for checking constraint-based opacity on executions, employing the SMT-solver Z3.

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

Access this chapter

Log in via an institution
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

References

  1. Armstrong, A., Dongol, B., Doherty, S.: Reducing opacity to linearizability: a sound and complete method. arXiv preprint arXiv:1610.01004 (2016)

  2. Attiya, H., Hans, S., Kuznetsov, P., Ravi, S.: Safety of deferred update in transactional memory. In: 2013 IEEE 33rd International Conference on Distributed Computing Systems (ICDCS), pp. 601–610. IEEE (2013)

    Google Scholar 

  3. Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: ACM SIGPLAN Notices, vol. 45, pp. 330–340. ACM (2010)

    Google Scholar 

  4. Dalessandro, L., Dice, D., Scott, M., Shavit, N., Spear, M.: Transactional mutex locks. In: D’Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 2–13. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15291-7_2

    Chapter  Google Scholar 

  5. Dalessandro, L., Spear, M.F., Scott, M.L.: NOrec: streamlining STM by abolishing ownership records. In: ACM Sigplan Notices, vol. 45, pp. 67–78. ACM (2010)

    Google Scholar 

  6. Derrick, J., Dongol, B., Schellhorn, G., Travkin, O., Wehrheim, H.: Verifying opacity of a transactional mutex lock. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 161–177. Springer, Cham (2015). doi:10.1007/978-3-319-19249-9_11

    Chapter  Google Scholar 

  7. Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Proving opacity of a pessimistic STM. In: Fatourou, P., Jiménez, E., Pedone, F. (eds.) 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 70, pp. 35:1–35:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017). http://drops.dagstuhl.de/opus/volltexte/2017/7104

  8. Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects Comput. 25(5), 769–799 (2013). http://dx.doi.org/10.1007/s00165-012-0225-8

  9. Dziuma, D., Fatourou, P., Kanellou, E.: Consistency for transactional memory computing. In: Guerraoui, R., Romano, P. (eds.) Transactional Memory. Foundations, Algorithms, Tools, and Applications. LNCS, vol. 8913, pp. 3–31. Springer, Cham (2015). doi:10.1007/978-3-319-14720-8_1

    Chapter  Google Scholar 

  10. Felber, P., Gramoli, V., Guerraoui, R.: Elastic transactions. In: Keidar, I. (ed.) DISC 2009. LNCS, vol. 5805, pp. 93–107. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04355-0_12

    Chapter  Google Scholar 

  11. Guerraoui, R., Henzinger, T.A., Singh, V.: Completeness and nondeterminism in model checking transactional memories. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 21–35. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85361-9_6

    Chapter  Google Scholar 

  12. Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distrib. Comput. 22(3), 129–145 (2010). http://dx.doi.org/10.1007/s00446-009-0092-6

  13. Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2008), pp. 175–184. ACM, New York (2008). http://doi.acm.org/10.1145/1345206.1345233

  14. Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: Proceedings of the 20th Annual International Symposium on Computer Architecture, San Diego, CA, May 1993, pp. 289–300 (1993). http://doi.acm.org/10.1145/165123.165164

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

    Article  Google Scholar 

  16. Imbs, D., Raynal, M.: Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations). Theoret. Comput. Sci. 444, 113–127 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  17. Lesani, M., Luchangco, V., Moir, M.: A framework for formally verifying software transactional memory algorithms. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 516–530. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32940-1_36

    Chapter  Google Scholar 

  18. Lesani, M., Palsberg, J.: Proving non-opacity. In: Afek, Y. (ed.) DISC 2013. LNCS, vol. 8205, pp. 106–120. Springer, Heidelberg (2013). doi:10.1007/978-3-642-41527-2_8

    Chapter  Google Scholar 

  19. Lesani, M., Palsberg, J.: Decomposing opacity. In: Kuhn, F. (ed.) DISC 2014. LNCS, vol. 8784, pp. 391–405. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45174-8_27

    Google Scholar 

  20. Manovit, C., Hangal, S., Chafi, H., McDonald, A., Kozyrakis, C., Olukotun, K.: Testing implementations of transactional memory. In: Proceedings of the 15th International Conference on Parallel Architectures and Compilation Techniques, pp. 134–143. ACM (2006)

    Google Scholar 

  21. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  22. O’Leary, J., Saha, B., Tuttle, M.R.: Model checking transactional memory with spin. In: 2009 29th IEEE International Conference on Distributed Computing Systems (ICDCS 2009), pp. 335–342. IEEE (2009)

    Google Scholar 

  23. Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM (JACM) 26(4), 631–653 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  24. Riegel, T., Fetzer, C., Felber, P.: Snapshot isolation for software transactional memory. In: First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT 2006), pp. 1–10. Association for Computing Machinery (ACM) (2006)

    Google Scholar 

  25. Shavit, N., Touitou, D.: Software transactional memory. Distrib. Comput. 10(2), 99–116 (1997)

    Article  Google Scholar 

  26. Siek, K., Wojciechowski, P.T.: Last-use opacity: a strong safety property for transactional memory with early release support. CoRR abs/1506.06275 (2015). http://arxiv.org/abs/1506.06275

  27. Sinha, A., Malik, S.: Runtime checking of serializability in software transactional memory. In: 2010 IEEE International Symposium on Parallel and Distributed Processing (IPDPS), pp. 1–12. IEEE (2010)

    Google Scholar 

  28. Spear, M.F., Michael, M.M., von Praun, C.: RingSTM: Scalable transactions with a single atomic instruction. In: Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, pp. 275–284. ACM (2008)

    Google Scholar 

Download references

Acknowledgements

Thanks to Jan Haltermann for help with Z3.

Author information

Authors and Affiliations

  1. Department of Computer Science, Paderborn University, Paderborn, Germany

    Jürgen König & Heike Wehrheim

Authors
  1. Jürgen König
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jürgen König .

Editor information

Editors and Affiliations

  1. Vietnam National University, Hanoi, Vietnam

    Dang Van Hung

  2. University of New Mexico, Albuquerque, New Mexico, USA

    Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

König, J., Wehrheim, H. (2017). Value-Based or Conflict-Based? Opacity Definitions for STMs. In: Hung, D., Kapur, D. (eds) Theoretical Aspects of Computing – ICTAC 2017. ICTAC 2017. Lecture Notes in Computer Science(), vol 10580. Springer, Cham. https://doi.org/10.1007/978-3-319-67729-3_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67729-3_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67728-6

  • Online ISBN: 978-3-319-67729-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation