Sequential Specification of Transactional Memory Semantics

Abstract

Transactional memory (TM) provides a general-purpose mechanism withwhich to construct concurrent objects. Transactional memory can alsobe thought of as a concurrent object, but its semantics are lessclear than those of the objects typically constructed on top of it.In particular, commit operations in a transactional memory may failwhen transactions conflict. Under what circumstances, exactly, issuch behavior permissible? We offer candidate sequential specificationsto capture the semantics of transactional memory. In all cases, werequire that reads return consistent values in any transaction thatsucceeds. Each specification embodies a conflict function, whichspecifies when two transactions cannot both succeed. Optionally,a specification may also embody an arbitration function, which specifieswhich of two conflicting transactions must fail. In the terminologyof the STM literature, arbitration functions correspond to the conceptof contention management. We identify TM implementations from theliterature corresponding to several specific conflict and arbitrationfunctions. We note that the specifications facilitate not only correctness(i.e., linearizability) proofs for nonblocking TM implementations,but also formal comparisons of the degree to which different implementationsadmit inter-transaction concurrency. In at least one case— eagerdetection of write-write conflicts and lazy detection of readwriteconflicts—the formalization exercise has led us to semantics thatare arguably desirable, but not, to the best of our knowledge, providedby any current TM system.