nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

verfasst von : Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

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

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability.

In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). Software transactional memory algorithms allow for concurrent access to shared state. Like linearizability for concurrent data structures, opacity is the established notion of correctness for STMs. First, we provide a novel definition of durable opacity extending opacity to handle crashes and recovery in the context of NVM. Second, we develop a durably opaque version of an existing STM algorithm, namely the Transactional Mutex Lock (TML). Third, we design a proof technique for durable opacity based on refinement between TML and an operational characterisation of durable opacity by adapting the TMS2 specification. Finally, we apply this proof technique to show that the durable version of TML is indeed durably opaque. The correctness proof is mechanized within Isabelle.

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 Towards Bridging Time and Causal Reversibility

Nächstes Kapitel Conformance-Based Doping Detection for Cyber-Physical Systems

This is in contrast to lazy implementations that defer transactional writes until the commit operation is executed (e.g., [9, 13]).

All Isabelle theory files related to this proof may be downloaded from [5].

Armstrong, A., Dongol, B.: Modularising opacity verification for hybrid transactional memory. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 33–49. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60225-7_3CrossRef

Armstrong, A., Dongol, B., Doherty, S.: Proving opacity via linearizability: a sound and complete method. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 50–66. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60225-7_4CrossRef

Attiya, H., Gotsman, A., Hans, S., Rinetzky, N.: Safety of live transactions in transactional memory: TMS is necessary and sufficient. In: Kuhn, F. (ed.) DISC 2014. LNCS, vol. 8784, pp. 376–390. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45174-8_26CrossRef

Ben-David, N., Blelloch, G.E., Friedman, M., Wei, Y.: Delay-free concurrency on faulty persistent memory. In: The 31st ACM Symposium on Parallelism in Algorithms and Architectures, pp. 253–264 (2019)

Bila, E., Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Defining and verifying durable opacity: correctness for persistent software transactional memory (2020). https://arxiv.org/abs/2004.08200

Chakrabarti, D.R., Boehm, H.J., Bhandari, K.: Atlas: leveraging locks for non-volatile memory consistency. ACM SIGPLAN Not. 49(10), 433–452 (2014)CrossRef

Coburn, J., et al.: Nv-heaps: making persistent objects fast and safe with next-generation, non-volatile memories. ACM SIGARCH Comput. Archit. News 39(1), 105–118 (2011)CrossRef

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). https://doi.org/10.1007/978-3-642-15291-7_2CrossRef

Dalessandro, L., Spear, M.F., Scott, M.L.: NORec: streamlining STM by abolishing ownership records. In: Govindarajan, R., Padua, D.A., Hall, M.W. (eds.) PPoPP, pp. 67–78. ACM (2010)

10.

Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Travkin, O., Wehrheim, H.: Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30(5), 597–625 (2017). https://doi.org/10.1007/s00165-017-0433-3MathSciNetCrossRefMATH

11.

Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verifying correctness of persistent concurrent data structures. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 179–195. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_12CrossRef

12.

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). https://doi.org/10.1007/978-3-319-19249-9_11CrossRef

13.

Dice, D., Shalev, O., Shavit, N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 194–208. Springer, Heidelberg (2006). https://doi.org/10.1007/11864219_14CrossRef

14.

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.) OPODIS. LIPIcs, vol. 70, pp. 35:1–35:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

15.

Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Asp. Comput. 25(5), 769–799 (2013)MathSciNetCrossRef

16.

Dongol, B., Jagadeesan, R., Riely, J.: Transactions in relaxed memory architectures. PACMPL 2(POPL), 18:1–18:29 (2018)

17.

Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19:1–19:43 (2015)CrossRef

18.

Felber, P., Fetzer, C., Riegel, T.: Dynamic performance tuning of word-based software transactional memory. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 237–246 (2008)

19.

Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Chatterjee, S., Scott, M.L. (eds.) PPOPP, pp. 175–184. ACM (2008)

20.

Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2010)

21.

Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463–492 (1990)CrossRef

22.

Izraelevitz, J., Mendes, H., Scott, M.L.: Linearizability of persistent memory objects under a full-system-crash failure model. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 313–327. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53426-7_23CrossRef

23.

Izraelevitz, J., Kelly, T., Kolli, A.: Failure-atomic persistent memory updates via justdo logging. ACM SIGARCH Comput. Archit. News 44(2), 427–442 (2016)CrossRef

24.

Joshi, A., Nagarajan, V., Cintra, M., Viglas, S.: DHTM: durable hardware transactional memory. In: 2018 ACM/IEEE 45th Annual International Symposium on Computer Architecture (ISCA), pp. 452–465. IEEE (2018)

25.

Joshi, A., Nagarajan, V., Viglas, S., Cintra, M.: Atom: atomic durability in non-volatile memory through hardware logging. In: 2017 IEEE International Symposium on High Performance Computer Architecture (HPCA), pp. 361–372. IEEE (2017)

26.

Lesani, M., Luchangco, V., Moir, M.: Putting opacity in its place. In: Workshop on the Theory of Transactional Memory (2012)

27.

Lu, Y., Shu, J., Sun, L., Mutlu, O.: Loose-ordering consistency for persistent memory. In: 2014 IEEE 32nd International Conference on Computer Design (ICCD), pp. 216–223. IEEE (2014)

28.

Lynch, N., Vaandrager, F.: Forward and backward simulations. Inf. Comput. 121(2), 214–233 (1995)MathSciNetCrossRef

29.

Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137–151. ACM, New York (1987)

30.

Müller, O.: I/O Automata and beyond: temporal logic and abstraction in Isabelle. In: Grundy, J., Newey, M. (eds.) TPHOLs, pp. 331–348. Springer, Heidelberg (1998)

31.

Nalli, S., Haria, S., Hill, M.D., Swift, M.M., Volos, H., Keeton, K.: An analysis of persistent memory use with whisper. ACM SIGPLAN Not. 52(4), 135–148 (2017)CrossRef

32.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

33.

Olson, M.A., Bostic, K., Seltzer, M.I.: Berkeley DB. In: USENIX Annual Technical Conference, FREENIX Track, pp. 183–191 (1999)

34.

Raad, A., Wickerson, J., Vafeiadis, V.: Weak persistency semantics from the ground up: formalising the persistency semantics of ARMV8 and transactional models. PACMPL 3(OOPSLA), 135:1–135:27 (2019)

35.

Raad, A., Vafeiadis, V.: Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. PACMPL 2(OOPSLA), 137:1–137:27 (2018)

36.

Sears, R., Brewer, E., Brewer, E., Brewer, E.: Stasis: flexible transactional storage. In: Proceedings of the 7th symposium on Operating Systems Design and Implementation, pp. 29–44. USENIX Association (2006)

37.

Volos, H., Tack, A.J., Swift, M.M.: Mnemosyne: lightweight persistent memory. ACM SIGARCH Comput. Archit. News 39(1), 91–104 (2011)CrossRef

38.

Zuriel, Y., Friedman, M., Sheffi, G., Cohen, N., Petrank, E.: Efficient lock-free durable sets. PACMPL 3(OOPSLA), 1281–12826 (2019)

Titel: Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
verfasst von: Eleni Bila
Simon Doherty
Brijesh Dongol
John Derrick
Gerhard Schellhorn
Heike Wehrheim
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-50085-6

Electronic ISBN: 978-3-030-50086-3

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-50086-3_3

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"