Li L,Zhang Y,Chen YY et al.Certifying concurrent programs using transactional memory.JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 24(1):110-121 Jan.2009 Certifying Concurrent Programs Using Transactional Memory Long Li(李隆)，Yu Zhang(张昱)，Yi-Yun Chen(陈意云)，and Yong Li(李勇) Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230027,China Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China Suzhou 215123,China E-mail:fliwis,liyong}@mail.ustc.edu.cn:fyuzhang,yiyun@ustc.edu.cn Received December 19,2007;revised June 23,2008 Abstract Transactional memory (TM)is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques.TM systems handle data races between threads automatically so that programmers do not have to reason about the interaction of threads manually.TM provides a programming model that may make the development of multi-threaded programs easier.Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance,but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound.In this paper,we focus on the semantics of transactional memory and present a proof-carrying code (PCC)system for reasoning about programs using TM.We formalize our reasoning with respect to the TM semantics,prove its soundness,and use examples to demonstrate its effectiveness. Keywords program verification,transactional memory,proof-carrying code,concurrent program safety 1 Introduction performance issues of these implementations have also been discussed.And there has also been some work The multicore architectures.which provide infras- that explores the formalization of the semantics of tructures of better performance,have become popu- TM[6.11-151.But little has been done on how to for- lar.To benefit from this growth in performance,pro- mally reason about programs using TM and how to grammers are required and forced to develop multi- make sure that such reasoning is sound.Easy reason- threaded programs.However,it is of great challenges ing,one of the primary reasons to introduce transac- for programmers to deal with subtle concurrent access tional memory,is rarely referred to. to shared memory by multiple threads.Traditionally. programmers use locks to achieve mutual exclusion on Proof-carrying code(PCC)16]is a Hoare-style rea- concurrent access to shared memory.But lock-based soning framework and has been well studied to rea- programming is difficult to reason about and may lead son about various properties of programs in recent to problems such as deadlock.Transactional memory years[17-201.And there are also extensions for reason- (TM)is proposed as an alternate concurrency-control ing about multi-threaded programs using locks(21.221 mechanism to avoid many of the pitfalls of the lock- However,the appearance of programs using TM claims based one.TM systems provide transactions as a pro for to be a brand-new system. gramming structure for programmers and handle data In this paper,we present a system to certify con- races between threads automatically so that program- current programs using transactional memory.We de- mers do not have to reason about the interaction of fine an abstract machine with built-in TM at assembly- threads manually.TM provides a programming model level and present a program logic based on this ma- that may make the development of multi-threaded pro- chine to support the verification of different properties. grams easier. We prove the soundness of our program logic with re- Much work has been done to explore the var- spect to the semantics of transactional memory and use ious implementation strategies of TM systems in examples to demonstrate its effectiveness.Our paper hardwarel1-4,in softwarel5-8],and in hybridl9,10.The makes the following contributions. Regular Paper Supported by the National Natural Science Foundation of China under Grant Nos.60673126 and 90718026,and Intel China Research Center.Li L, Zhang Y, Chen YY et al. Certifying concurrent programs using transactional memory. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 24(1): 110–121 Jan. 2009 Certifying Concurrent Programs Using Transactional Memory Long Li (李 隆), Yu Zhang (张 昱), Yi-Yun Chen (陈意云), and Yong Li (李 勇) Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China Suzhou 215123, China E-mail: {liwis, liyong}@mail.ustc.edu.cn; {yuzhang, yiyun}@ustc.edu.cn Received December 19, 2007; revised June 23, 2008. Abstract Transactional memory (TM) is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound. In this paper, we focus on the semantics of transactional memory and present a proof-carrying code (PCC) system for reasoning about programs using TM . We formalize our reasoning with respect to the TM semantics, prove its soundness, and use examples to demonstrate its effectiveness. Keywords program verification, transactional memory, proof-carrying code, concurrent program safety 1 Introduction The multicore architectures, which provide infras￾tructures of better performance, have become popu￾lar. To benefit from this growth in performance, pro￾grammers are required and forced to develop multi￾threaded programs. However, it is of great challenges for programmers to deal with subtle concurrent access to shared memory by multiple threads. Traditionally, programmers use locks to achieve mutual exclusion on concurrent access to shared memory. But lock-based programming is difficult to reason about and may lead to problems such as deadlock. Transactional memory (TM) is proposed as an alternate concurrency-control mechanism to avoid many of the pitfalls of the lock￾based one. TM systems provide transactions as a pro￾gramming structure for programmers and handle data races between threads automatically so that program￾mers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded pro￾grams easier. Much work has been done to explore the var￾ious implementation strategies of TM systems in hardware[1−4], in software[5−8], and in hybrid[9,10]. The performance issues of these implementations have also been discussed. And there has also been some work that explores the formalization of the semantics of TM[6,11−15]. But little has been done on how to for￾mally reason about programs using TM and how to make sure that such reasoning is sound. Easy reason￾ing, one of the primary reasons to introduce transac￾tional memory, is rarely referred to. Proof-carrying code (PCC)[16] is a Hoare-style rea￾soning framework and has been well studied to rea￾son about various properties of programs in recent years[17−20]. And there are also extensions for reason￾ing about multi-threaded programs using locks[21,22] . However, the appearance of programs using TM claims for to be a brand-new system. In this paper, we present a system to certify con￾current programs using transactional memory. We de- fine an abstract machine with built-in TM at assembly￾level and present a program logic based on this ma￾chine to support the verification of different properties. We prove the soundness of our program logic with re￾spect to the semantics of transactional memory and use examples to demonstrate its effectiveness. Our paper makes the following contributions. Regular Paper Supported by the National Natural Science Foundation of China under Grant Nos. 60673126 and 90718026, and Intel China Research Center