nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

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

verfasst von : Jürgen König, Heike Wehrheim

Erschienen in: Theoretical Aspects of Computing – ICTAC 2017

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Class-Diagrams for Abstract Data Types

Nächstes Kapitel Smaller-State Implementations of 2D FSSP Algorithms

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

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)

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)

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 CrossRef

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)

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 CrossRef

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

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

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 CrossRef

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 CrossRef

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 CrossRef

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

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

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 CrossRef

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 CrossRef

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

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)

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 CrossRef

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)

23.

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

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)

25.

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

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)

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)

Titel: Value-Based or Conflict-Based? Opacity Definitions for STMs
verfasst von: Jürgen König
Heike Wehrheim
Verlag: Springer International Publishing
Buch: Theoretical Aspects of Computing – ICTAC 2017
Print ISBN: 978-3-319-67728-6

Electronic ISBN: 978-3-319-67729-3

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-67729-3_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"