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.
transactional memory strong atomicity proof- carrying code
Yong Li Yu Zhang Yiyun Chen Ming Fu
Department of Computer Science & Technology University of Science & Technology of China Hefei, 23002 Department of Computer Science & Technology University of Science & Technology of China Hefei, 23002 Department of Computer Science & Technology University of Science & Technology of China Hefei, 23002
国际会议
上海
英文
123-131
2009-07-08（万方平台首次上网日期，不代表论文的发表时间）