Certifying Concurrent Programs Using Transactional Memory

Transactional memory (TM) is a new promising concurrency-controlmechanism that can avoid many of the pitfalls of the traditionallock-based techniques. TM systems handle data races between threadsautomatically so that programmers do not have to reason about theinteraction of threads manually. TM provides a programming modelthat may make the development of multi-threaded programseasier. Much work has been done to explore the variousimplementation strategies of TM systems and to achieve betterperformance, but little has been done on how to formally reasonabout programs using TM and how to make sure thatsuch reasoning is sound.In this paper, we focus on the semantics of transactional memory andpresent a proof-carrying code (PCC) system for reasoning aboutprograms using TM . We formalize our reasoning with respect to the TM semantics,prove its soundness, and use examples to demonstrate its effectiveness.