Moverness for Locks and Transactions

Locks are pervasive in multithreaded code. For software transactional memory (STM) to be widely adopted there must be a consensus on a semantics for programs that entail both locks and transactions, particularly for weakly isolated STMs. For instance, in a weakly isolated STM, use of both locks and transactions to access the same data may introduce data races. In response we present a simple and intuitive semantics that guarantees ordered linearisation points for conflicting locks and transactions. Our approach allows us to classify the moverness of locks and transactions, making reasoning about parallel compositions trivial. Under our semantics we show locks to be left movers and transactions right movers, and the serialisability of conflicting locks and transactions.