Transactions in the Jungle

Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. However, the semantics of interactions between transactions managed by a TM and non-transactional operations, while widely studied, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a new correctness condition for TMs, \emph{parametrized opacity}, which captures the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional operations, and second, non-transactional operations conform to a given memory model. Parametrized opacity corresponds to the well-studied strong atomicity property, which lacks a formal definition and is, in fact, ambiguous. We use our formalization to theoretically investigate the inherent cost of implementing parametrized opacity. We first prove that parametrized opacity requires either instrumenting non-transactional operations (for most memory models) or writing to memory by transactions using potentially expensive read-modify-write instructions (such as compare-and-swap). Then, we show that for a class of relaxed memory models, parametrized opacity can indeed be implemented with constant-time instrumentation of non-transactional writes and no instrumentation of non-transactional reads. We show that, in practice, parametrizing the notion of correctness allows to develop more efficient TM implementations.