On the Verification of Strong Atomicity of Programs Using STM
Authors
Yong Li
Yu Zhang
Yiyun Chen
Ming Fu
Abstract
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 consistency of states in our model and use a notion of ``local guarantee'' to check the shared memory consistency for verification. Our work provides a foundation for certifying realistic transactional program and makes an important advance toward generating proof-carrying code.
Published
- Paper Draft
- Coq implementation