Proving isolation properties for software transactional memory

Abstract

An algorithm for Software Transactional Memory (STM) is correct if it guarantees a proclaimed degree of isolation between concurrently executing transactions. A correctness proof requires explicit modeling of the effects of transaction bodies and the non-deterministic scheduling of their operations. We provide a formalization of an STM algorithm that is explicit about all aspects required for a correctness proof: effects of operations, non-determinism, and modeling rollback. We prove that this algorithm is correct by showing that it implements opacity. © 2011 Springer-Verlag.