On the Verification of Strong Atomicity in Programs Using STM

Transactional memory(TM) provides an easy-using and high-performance parallel programming model for multicore systems. It simplifies parallel programming by supporting that transactions appear to execute atomically and in isolation. Despite the large amount of recent works on various TM implementations, very little has been devoted to precisely guarantee that these implementations have implemented the atomicity and isolation properties. In previous work we have proposed a framework on the correctness of STM programs by formally certifying the shared memory invariant at assembly level. Now the framework is extended and we certify the strong atomicity property of programs using STM in this paper. In particular, we formalize the strong atomicity as the shared memory consistence of states in our model and use a notion of "local guarantee" to check the shared memory consistence for verification. Our work provides a foundation for certifying realistic transactional programs and makes an important advance toward generating proof-carrying code.