Abstract
One of the main challenges in stating the correctness of transactional memory (TM) systems is the need to provide guarantees on the system state observed by live transactions, i.e., those that have not yet committed or aborted. A TM correctness condition should be weak enough to allow flexibility in implementation, yet strong enough to disallow undesirable TM behavior, which can lead to run-time errors in live transactions. The latter feature is formalized by observational refinement between TM implementations, stating that properties of a program using a concrete TM implementation can be established by analyzing its behavior with an abstract TM, serving as a specification of the concrete one.
We show that a variant of transactional memory specification (TMS), a TM correctness condition, is equivalent to observational refinement for the common programming model in which local variables are rolled back upon a transaction abort and, hence, is the weakest acceptable condition for this case. This is challenging due to the nontrivial formulation of TMS, which allows different aborted and live transactions to have different views of the system state. Our proof reveals some natural, but subtle, assumptions on the TM required for the equivalence result.
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
Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26, 631–653 (1979)
Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: PPOPP, pp. 175–184 (2008)
Imbs, D., Raynal, M.: Virtual world consistency: A condition for STM systems (with a versatile protocol with invisible read operations). Theor. Comput. Sci. 444, 113–127 (2012)
Attiya, H., Hans, S., Kuznetsov, P., Ravi, S.: Safety of deferred update in transactional memory. In: ICDCS (2013)
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects of Computing 25, 769–799 (2013)
He, J., Hoare, C., Sanders, J.: Prespecification in data refinement. Information Processing Letters 25, 71–76 (1987)
He, J., Hoare, C., Sanders, J.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Attiya, H., Gotsman, A., Hans, S., Rinetzky, N.: A programming language perspective on transactional memory consistency. In: PODC, pp. 309–318 (2013)
Scala STM Expert Group: Scala STM quick start guide (2012), http://nbronson.github.io/scala-stm/quick_start.html
Lesani, M., Luchangco, V., Moir, M.: Putting opacity in its place. In: WTTM (2012)
Attiya, H., Gotsman, A., Hans, S., Rinetzky, N.: Safety of live transactions in transactional memory: Tms is necessary and sufficient. Technical Report CS-2014-02, Technion (2014)
Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems 12, 463–492 (1990)
Gotsman, A., Yang, H.: Liveness-preserving atomicity abstraction. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 453–465. Springer, Heidelberg (2011)
Filipović, I., O’Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 252–266. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Attiya, H., Gotsman, A., Hans, S., Rinetzky, N. (2014). Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient. In: Kuhn, F. (eds) Distributed Computing. DISC 2014. Lecture Notes in Computer Science, vol 8784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45174-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-662-45174-8_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45173-1
Online ISBN: 978-3-662-45174-8
eBook Packages: Computer ScienceComputer Science (R0)