Parameterized Verification of Transactional Memories

We describe an automatic verification method to check whether transactional memories ensure strict serializability--a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized systems. The technique merges ideas from parameterized hardware and protocol verification--verification by invisible invariants and symmetry reduction--with ideas from software verification--template-based invariant generation and satisfiability checking for quantified formul

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Michael Emmi, Rupak Majumdar, Roman Manevich
• Keywords: PLDI 2010, Programming Languages, Software Transactional Memory, State Explosion, Transactional Locking Ii