Model Checking Transactional Memories

Опубликовано 6 сентября 2016, 17:39

With the inherent problems in writing correct and efficient concurrent code, a recent concurrent programming paradigm called 'software transactional memory' has gained popularity. 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 reduce this verification problem to a finite state problem in two steps. First, 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. Second, 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. 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 talk presents work published in PLDI'08 and CONCUR'08.