Model checking transactional memories

11 years 10 months ago
Model checking transactional memories
Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom. Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the secon...
Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2010
Where DC
Authors Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh
Comments (0)