Model CheckingTransactional Memories.pptVIP

Liveness properties Utopia: Every thread commits infinitely often (wait-freedom) Wait-freedom cannot be guaranteed in TM in an asynchronous system Two weaker notions: Lock freedom: commits occur infinitely often (no matter which thread commits) Obstruction freedom: if a thread takes an infinite number of steps in isolation, it commits infinitely often Wait freedom = Lock freedom = Obstruction freedom * Alpine Verification Meeting 2008 A similar recipe for liveness Model (n,k) TM as a finite state transition system Check automatically liveness of (n,k) TM Appeal to symmetry of TM * Alpine Verification Meeting 2008 What we prove about liveness We formally prove the following results: DSTM is obstruction free for any number of threads and variables TL2, Two phase locking, Optimistic concurrency control are not obstruction free None of these TMs are lock free or wait free * Alpine Verification Meeting 2008 FURTHER WORK Alpine Verification Meeting 2008 * Making the procedure complete Incompleteness due to nondeterministic references: Simple and intuitive. Explore all possible serialization points of transactions Lot of redundancy. Many equivalent behaviors. We build smaller deterministic references: Speed up model checking by ten times Give a sound and complete procedure Correctness not so intuitive: proved using an antichain based tool * Alpine Verification Meeting 2008 Handling Contention Managers Build a universal contention manager (UCM) which chooses one of the possible decisions nondeterministically Plug the TM with UCM and prove correctness Correctness of TM with UCM = correctness of TM with any contention manager DSTM, TL2 plugged with UCM satisfy symmetry properties * Alpine Verification Meeting 2008 Conclusion Modeling transactional memories and verifying safety and liveness First automatically prove the property for a restricted case, then exploit inherent symmetry in TM to generalize the result Works for most of the published TMs: we prove that DSTM