Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient

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 ob-served 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 imple-mentation, yet strong enough to disallow undesirable TM behavior, which can lead to run-time errors in live transactions. The latter feature is formalized by ob-servational 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 cor-rectness condition, is equivalent to observational refinement for the common pro-gramming 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.