Abstract
Software transactional memory (STMs) is a software-enabled form of transactional memory, typically implemented as a language library, that provides fine-grained concurrency control on behalf of a programmer STM algorithms have been recently adapted to cope with non-volatile memory (NVM), aka persistent memory, which is a new paradigm for memory that preserves its contents even after power loss. This paper presents a model checking approach to validating correctness of STM algorithms using FDR (a model checker for CS P specifications). Our proofs are based on operational transactional memory specifications that allow proofs of (durable) opacity, the main safety property for STMs under volatile and persistent memory, to be verified by refinement. Since FDR enables automatic proofs of refinement, we obtain an automatic technique for checking both opacity and durable opacity of bounded models of STM algorithms.