Abstract
In this chapter we give a formal overview of liveness properties of transactional memory (TM) systems. Unlike safety properties, which require some ‘bad’ events not to occur, liveness properties require some ‘good’ events to eventually occur. Usually, liveness properties of shared memory systems require some operations to eventually return a response (terminate). However, in the context of TM systems operation termination is not enough to ensure meaningful progress. It is necessary to require some transactions to eventually commit. In this chapter we give precise definitions of liveness properties and what it means for a TM systems to satisfy a liveness property. Using the defined formal framework we give some impossibility results. We show that it is impossible to guarantee both local progress, the strongest TM liveness property that requires every correct transaction to eventually commit, and common TM safety properties such as strict serializability or opacity in a fault prone system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Birrell, A., Harris, T., Isard, M.: Semantics of transactional memory and automatic mutual exclusion. ACM Trans. Program. Lang. Syst. 33(1) (2011)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4) (1985)
Bushkov, V., Guerraoui, R., Kapałka, M.: On the liveness of transactional memory. In: Proceedings of ACM PODC 2012 (2012)
Dice, D., Shalev, O., Shavit, N.N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 194–208. Springer, Heidelberg (2006)
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Electron. Notes Theor. Comput. Sci. 259 (2009)
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects of Computing 25(5), 769–799 (2013)
Dragojević, A., Guerraoui, R., Kapalka, M.: Stretching transactional memory. SIGPLAN Not 44(6), 155–165 (2009)
Dziuma, D., Fatourou, P., Kanellou, E.: Survey on consistency conditions. Tech. Rep. 439, FORTH-ICS (2013)
Felber, P., Fetzer, C., Riegel, T.: Dynamic performance tuning of word-based software transactional memory. In: ACM PPoPP 2008, pp. 237–246 (2008)
Fraser, K.: Practical lock freedom. PhD thesis, Cambridge University Computer Laboratory (2003)
Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Proceedings of ACM PPoPP 2008 (2008)
Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. Morgan and Claypool (2010)
Harris, T., Larus, J.R., Rajwar, R.: Transactional Memory, 2nd edn. Morgan and Claypool (2010)
Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1) (1991)
Herlihy, M., Luchangco, V., Moir, M., Scherer III, W.N.: Software transactional memory for dynamic-sized data structures. In: Proceedings of ACM PODC 2003 (2003)
Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. SIGARCH Comput. Archit. News 21(2) (1993)
Herlihy, M., Shavit, N.: On the nature of progress. In: Fernàndez Anta, A., Lipari, G., Roy, M. (eds.) OPODIS 2011. LNCS, vol. 7109, pp. 313–328. Springer, Heidelberg (2011)
Imbs, D., de Mendivil, J.R., Raynal, M.: Brief announcement: Virtual world consistency: A new condition for stm systems. In: ACM PODC 2009, pp. 280–281 (2009)
Jagannathan, S., Vitek, J., Welc, A., Hosking, A.: A transactional object calculus. Sci. Comput. Program. 57(2) (2005)
Lesani, M., Palsberg, J.: Proving non-opacity. In: Afek, Y. (ed.) DISC 2013. LNCS, vol. 8205, pp. 106–120. Springer, Heidelberg (2013)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc. (1996)
Menon, V., Balensiefer, S., Shpeisman, T., Adl-Tabatabai, A.R., Hudson, R.L., Saha, B., Welc, A.: Practical weak-atomicity semantics for java stm. In: ACM SPAA 2008, pp. 314–325 (2008)
Moore, K.F., Grossman, D.: High-level small-step operational semantics for transactions. In: ACM POPL 2008, pp. 51–62 (2008)
Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4) (1979)
Segala, R., Gawlick, R., Søgaard-Andersen, J., Lynch, N.: Liveness in timed and untimed systems. Inf. Comput. 141(2) (1998)
Shavit, N., Touitou, D.: Software transactional memory. In: Proceedings of ACM PODC 1995 (1995)
Völzer, H., Varacca, D.: Defining fairness in reactive and concurrent systems. J. ACM 59(3) (2012)
Wamhoff, J.T., Fetzer, C.: The universal transactional memory construction. In: TRANSACT 2011. ACM, New York (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Bushkov, V., Guerraoui, R. (2015). Liveness in Transactional Memory. In: Guerraoui, R., Romano, P. (eds) Transactional Memory. Foundations, Algorithms, Tools, and Applications. Lecture Notes in Computer Science, vol 8913. Springer, Cham. https://doi.org/10.1007/978-3-319-14720-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-14720-8_2
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14719-2
Online ISBN: 978-3-319-14720-8
eBook Packages: Computer ScienceComputer Science (R0)