Long Li et al.:Certifying Concurrent Programs Using TM 119 storage while consumers keep consuming goods.The of interaction.And we formalize our reasoning into a storage is modeled as a finite First In First Out queue in PCC[16]system. the program.Threads(producers and consumers)oper- Recent years,Shao et al.have developed CCAP211 ate on the queue concurrently while keeping the queue CMAP[22]and SAGL[36]as extensions to the PCC consistent:the queue will not overflow and will not framework to verify properties of concurrent programs be full and empty simultaneously.This invariant is ex- using locks.And we present an extension to enable pressed as！(Full A Empty）A(0≤In,Out<BFSIZE), verification of concurrent programs using TM. where Full and Empty indicate the queue is full or Also,much work has started to explore the seman- empty respectively,In points to the location where pro- tics of transactional memory.Moore and Grossman[13] ducers are about to put goods and Out points to the have presented type systems to study the behaviors of location where consumers are about to consume goods. spawning threads in transactional programs and showed The assembly code for producers and the corre- the relation of strong and weak atomicity in TM sys- sponding invariant for the program are presented in tem's implementations.They presented the semantics Fig.11.The specifications are also shown of where a of transactions in a A-calculus.In a later version of their producer thread is about to start a transaction (labeled work4l,they expanded to study the semantics of the L-start,to increase goods (labeled L_addin),to sig- rollback operation for eager versioning in details.They nal the non-emptiness of the storage(labeled L-setemp) used different type systems to study different issues. and to commit the transaction(labeled L_commit).And Abadi et al.15]developed semantics and type sys- the code and specifications for consumers are similar tems for the Automatic Mutual Exclusion (AME)cal- and not shown here. culus,which encourage programmers to place as much Producers and consumers would start transactions of the program text inside transactions as possible. and collect effects they attempt to make based on their They also presented the semantics and correctness of local views to the global heap.Then they would commit the rollback operation in their systems. their modifications to the global heap with respect to Vitek et al.[1]used a variant of Featherweight the global invariant when their attempts are validated. Javal37 to define a framework to explore various im- Our work is fully mechanized in the Coq proof as- plementation strategies of TM systems and to ensure sistant,including the system,its soundness proof and the correctness of an implementation by establishing a the examples that are demonstrated above.Interested serializability result.And they assumed all codes exe- readers can check out our Coq implementation[281 for cute inside transactions. more details However,most work on TM semantics has just ex- plored definition of abstract machines and execution of Related Work transactional programs,and does not propose rules for certifying general properties of concurrent programs us- Many methods have been proposed for reasoning ing TM. about properties of both sequential and concurrent programs(29-331.But most efforts on concurrent pro 6 Conclusion grams focus on the lock-based programs and do not aim at programs using TM.And the lock-based reason- In this paper we present a system for verifying ing requires programmers to reason about the interfer- concurrent programs using transactional memory.We ence between threads.But as we present in this paper, modeled an assembly-level machine with built-in trans- TM-based reasoning does not.There is an easier way actional memory.We incorporated the well-known enforced by the TM semantics to perform TM-based invariant-based proof method into our system by requir- reasoning. ing the preservation of invariant not only on properties Harris et al.4 require an explicit definition of in- of each thread of a program but also on the shared mem- variants from programmers to track the dependencies ory these threads cooperate on.We proved our reason- between transactions.But they do not specify the prop- ing sound with respect to the TM semantics.And we erties of a program.Concurrent separation logicl35] used a few examples to demonstrate the effectiveness of separates shared memory into pieces,each of which is our techniques.For now,our system can reason about guarded by a lock and respects certain invariant,to safety properties of programs using TM only.Enriching perform the verification of lock-based concurrent pro- the expressiveness of the program logic of our system grams.We are enlightened by these work and specify to enable the verification of liveness properties such as invariants on shared memory to check the correctness fairness will be part of our future work.And we alsoLong Li et al.: Certifying Concurrent Programs Using TM 119 storage while consumers keep consuming goods. The storage is modeled as a finite First In First Out queue in the program. Threads (producers and consumers) oper￾ate on the queue concurrently while keeping the queue consistent: the queue will not overflow and will not be full and empty simultaneously. This invariant is ex￾pressed as ! (Full ∧ Empty) ∧ (0 6 In, Out < BFSIZE), where Full and Empty indicate the queue is full or empty respectively, In points to the location where pro￾ducers are about to put goods and Out points to the location where consumers are about to consume goods. The assembly code for producers and the corre￾sponding invariant for the program are presented in Fig.11. The specifications are also shown of where a producer thread is about to start a transaction (labeled L start, to increase goods (labeled L addin), to sig￾nal the non-emptiness of the storage (labeled L setemp) and to commit the transaction (labeled L commit). And the code and specifications for consumers are similar and not shown here. Producers and consumers would start transactions and collect effects they attempt to make based on their local views to the global heap. Then they would commit their modifications to the global heap with respect to the global invariant when their attempts are validated. Our work is fully mechanized in the Coq proof as￾sistant, including the system, its soundness proof and the examples that are demonstrated above. Interested readers can check out our Coq implementation[28] for more details. 5 Related Work Many methods have been proposed for reasoning about properties of both sequential and concurrent programs[29−33]. But most efforts on concurrent pro￾grams focus on the lock-based programs and do not aim at programs using TM. And the lock-based reason￾ing requires programmers to reason about the interfer￾ence between threads. But as we present in this paper, TM-based reasoning does not. There is an easier way enforced by the TM semantics to perform TM-based reasoning. Harris et al.[34] require an explicit definition of in￾variants from programmers to track the dependencies between transactions. But they do not specify the prop￾erties of a program. Concurrent separation logic[35] separates shared memory into pieces, each of which is guarded by a lock and respects certain invariant, to perform the verification of lock-based concurrent pro￾grams. We are enlightened by these work and specify invariants on shared memory to check the correctness of interaction. And we formalize our reasoning into a PCC[16] system. Recent years, Shao et al. have developed CCAP[21] , CMAP[22] and SAGL[36] as extensions to the PCC framework to verify properties of concurrent programs using locks. And we present an extension to enable verification of concurrent programs using TM. Also, much work has started to explore the seman￾tics of transactional memory. Moore and Grossman[13] have presented type systems to study the behaviors of spawning threads in transactional programs and showed the relation of strong and weak atomicity in TM sys￾tem’s implementations. They presented the semantics of transactions in a λ-calculus. In a later version of their work[14], they expanded to study the semantics of the rollback operation for eager versioning in details. They used different type systems to study different issues. Abadi et al.[15] developed semantics and type sys￾tems for the Automatic Mutual Exclusion (AME) cal￾culus, which encourage programmers to place as much of the program text inside transactions as possible. They also presented the semantics and correctness of the rollback operation in their systems. Vitek et al.[11] used a variant of Featherweight Java[37] to define a framework to explore various im￾plementation strategies of TM systems and to ensure the correctness of an implementation by establishing a serializability result. And they assumed all codes exe￾cute inside transactions. However, most work on TM semantics has just ex￾plored definition of abstract machines and execution of transactional programs, and does not propose rules for certifying general properties of concurrent programs us￾ing TM. 6 Conclusion In this paper we present a system for verifying concurrent programs using transactional memory. We modeled an assembly-level machine with built-in trans￾actional memory. We incorporated the well-known invariant-based proof method into our system by requir￾ing the preservation of invariant not only on properties of each thread of a program but also on the shared mem￾ory these threads cooperate on. We proved our reason￾ing sound with respect to the TM semantics. And we used a few examples to demonstrate the effectiveness of our techniques. For now, our system can reason about safety properties of programs using TM only. Enriching the expressiveness of the program logic of our system to enable the verification of liveness properties such as fairness will be part of our future work. And we also