## Model Checking Transactional Memories

*Rachid Guerraoui,
Thomas A. Henzinger,
Barbara Jobstmann, and Vasu Singh*

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 second step we use a model
checker to prove the requirement for the STM applied to a most general
program with two threads and two variables. In the safety case, the
model checker constructs a simulation relation between two carefully
constructed finite-state transition systems, one representing the
given STM applied to a most general program, and the other
representing a most liberal safe STM applied to the same program. In
the liveness case, the model checker analyzes fairness conditions on
the given STM transition system.

*Proceedings of the
International Conference on Programming Language Design and Implementation*
(PLDI),
ACM Press,
2008,
pp. 372-382.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2008 ACM.