Non-interference and local correctness in transactional memory

We show that non-interference is, in a strict sense, not implementable with respect to the popular criterion of opacity that requires all transactions (be they committed, aborted or incomplete) to witness the same global serial execution. In contrast, when we only require local correctness, non-interference is implementable. Informally, a correctness criterion is local if it only requires that every transaction can be serialized along with (a subset of) the transactions committed before its last event (aborted or incomplete transactions ignored). We give a few examples of local correctness properties, including the recently proposed criterion of virtual world consistency, and present a simple though efficient implementation that satisfies non-interference and local opacity.