Long Li et al.:Certifying Concurrent Programs Using TM 117 iv forki forki-1=i-1),indicating that the i-th next to him always.Note that we cannot ensure fairness philosopher is not holding forks or he is holding both in our system.Verification of such liveness properties forks he need or his fork is being held by others,where is part of our future work. forks are free or picked in pairs and a philosopher is try- The corresponding specification and program for our ing to pick his own fork and the fork of the philosopher system are shown in Fig.8.Only the code for Thread is given because that of Thread2 is similar.In this ex- InuH是u.HIfork1→v*fork2→v ample,Inv defines the invariant on the global heap for this program (fork fork2). L1:-{pc=L1} We explain the code block labeled L1,which cor- starttrans responds to the operations of picking up both forks -{日v.H,I fork1一v*fork2一v AHe IF emp A B.pc L1} for philosopher 1.The precondition of this block in- dicates that all jumpings to this block are allowed be- lw ti forki zero cause (pc =L1)is always valid when it is about to ex- -{日v.H,I fork1一v*fork2一U AH IF emp A B.pc L1 A R(t1)=H (fork1)} ecute the instruction labeled L1.After the block starts bne t1 zero L3 a transaction,the write attempts H of this transac- -{Hs I fork1一0*fork2→0 tion are set empty and the global heap H is copied to AHe I-emp A B.pc L1} local H.,so the local heap also respects the global in- addiu t2 zero 1 variant here (Inv H.).Also the target of rollback is -{HsI-fork1一0*fork2→0 set where the transaction starts (B.pc =L1).Then it AHe I-emp A B.pc L1 A R(t2)=1} tries to pick up both forks (updates H.)after checking sw t2 fork1 zero that the forks are free at its view.Note that the invari- -{H I-fork11*fork20 ant is broken locally(H,fork1一1*fork2一0) AHe IF fork11A B.pc L1 A R(t2)=1} when the first fork is picked(sw t2 fork zero),and sw t2 fork2 zero is reestablished when the other fork is also picked before -{H。IFfork1-1*for2一1 the transaction commits.Then it commits its picking AH IF fork1一1*fork2→1∧B.pc=L1} up(Hw l fork1→1*fork2→l)to the global heap commit H if no forks have been picked and are being held by -{true} the other (Thread2)during its try. j L2 Note that the reasoning of Thread needs no infor- mation of Thread2.Due to the guarantee that all modi- L2:-{pc=L2 fications to the global heap will respect the global in- starttrans variant,we are able to perform such reasoning.And -{臼v.Hs l fork1→v*fork2一U it is obvious that the composition of such reasoning is AHLe I-emp A B.pc L2} easy,since we need only to identify the compatibility addiu t3 zero 0 of the invariants of different threads to increase concur- -{月v.Hs l fork1→v*fork2一U rency. AHe I-emp A B.pc L2 A R(t3)=0} sw t3 fork zero When reasoning about the lock-based program for -{扫v.Hs l fork1→0*fork2一u this examplel211,programmers are required to en- AHLe I-fork10A B.pc L2A R(t3)=0} sure the non-interference between every two threads. sw t3 fork2 zero And when composing threads,the non-interference be- -{Hs IF fork1→0*for2→0 tween the newly-added one and all the existent is re- AHw I-fork1一0*fork2→0∧B.pc=L2]} quired.The concurrency-control mechanism,transac- commit tional memory,significantly eases the reasoning. -{true} Interestingly,we can perform a similar reasoning for j L1 the corresponding high-level programs in Fig.7.We know that (fork fork2)is valid when the trans- L3:-{pc=L3AH4 Ifork1→1*fork2→1 action starts.And the forks are free to pick if(fork= AHw I-emp A B.pc =L1} 0=fork2).Then the philosopher will commit his pick- commit ing attempts successfully if shared memory has not been -{true updated by the other thread.Finally,shared memory j L1 remains in a state that respects the invariant (forki= Fig.8.Dining Philosophers in our system. 1=fork2).Long Li et al.: Certifying Concurrent Programs Using TM 117 i ∨ forki = forki−1 = i − 1), indicating that the i-th philosopher is not holding forks or he is holding both forks he need or his fork is being held by others, where forks are free or picked in pairs and a philosopher is try￾ing to pick his own fork and the fork of the philosopher Inv H , ∃ v. H ° fork1 7→ v ∗ fork2 7→ v L1: −{pc = L1} starttrans −{∃ v.Hs ° fork1 7→ v ∗ fork2 7→ v ∧Hw ° emp ∧ B.pc = L1} lw t1 fork1 zero −{∃ v.Hs ° fork1 7→ v ∗ fork2 7→ v ∧Hw ° emp ∧ B.pc = L1 ∧ R(t1) = Hs(fork1)} bne t1 zero L3 −{Hs ° fork1 7→ 0 ∗ fork2 7→ 0 ∧Hw ° emp ∧ B.pc = L1} addiu t2 zero 1 −{Hs ° fork1 7→ 0 ∗ fork2 7→ 0 ∧Hw ° emp ∧ B.pc = L1 ∧ R(t2) = 1} sw t2 fork1 zero −{Hs ° fork1 7→ 1 ∗ fork2 7→ 0 ∧Hw ° fork1 7→ 1 ∧ B.pc = L1 ∧ R(t2) = 1} sw t2 fork2 zero −{Hs ° fork1 7→ 1 ∗ fork2 7→ 1 ∧Hw ° fork1 7→ 1 ∗ fork2 7→ 1 ∧ B.pc = L1} commit −{true} j L2 L2: −{pc = L2} starttrans −{∃ v.Hs ° fork1 7→ v ∗ fork2 7→ v ∧Hw ° emp ∧ B.pc = L2} addiu t3 zero 0 −{∃ v.Hs ° fork1 7→ v ∗ fork2 7→ v ∧Hw ° emp ∧ B.pc = L2 ∧ R(t3) = 0} sw t3 fork1 zero −{∃ v.Hs ° fork1 7→ 0 ∗ fork2 7→ v ∧Hw ° fork1 7→ 0 ∧ B.pc = L2 ∧ R(t3) = 0} sw t3 fork2 zero −{Hs ° fork1 7→ 0 ∗ fork2 7→ 0 ∧Hw ° fork1 7→ 0 ∗ fork2 7→ 0 ∧ B.pc = L2} commit −{true} j L1 L3: −{pc = L3 ∧ Hs ° fork1 7→ 1 ∗ fork2 7→ 1 ∧Hw ° emp ∧ B.pc = L1} commit −{true} j L1 Fig.8. Dining Philosophers in our system. next to him always. Note that we cannot ensure fairness in our system. Verification of such liveness properties is part of our future work. The corresponding specification and program for our system are shown in Fig.8. Only the code for Thread1 is given because that of Thread2 is similar. In this ex￾ample, Inv defines the invariant on the global heap for this program (fork1 = fork2). We explain the code block labeled L1, which cor￾responds to the operations of picking up both forks for philosopher 1. The precondition of this block in￾dicates that all jumpings to this block are allowed be￾cause (pc = L1) is always valid when it is about to ex￾ecute the instruction labeled L1. After the block starts a transaction, the write attempts Hw of this transac￾tion are set empty and the global heap H is copied to local Hs, so the local heap also respects the global in￾variant here (Inv Hs). Also the target of rollback is set where the transaction starts (B.pc = L1). Then it tries to pick up both forks (updates Hs) after checking that the forks are free at its view. Note that the invari￾ant is broken locally (Hs ° fork1 7→ 1 ∗ fork2 7→ 0) when the first fork is picked (sw t2 fork1 zero), and is reestablished when the other fork is also picked before the transaction commits. Then it commits its picking up (Hw ° fork1 7→ 1 ∗ fork2 7→ 1) to the global heap H if no forks have been picked and are being held by the other (Thread2) during its try. Note that the reasoning of Thread1 needs no infor￾mation of Thread2. Due to the guarantee that all modi- fications to the global heap will respect the global in￾variant, we are able to perform such reasoning. And it is obvious that the composition of such reasoning is easy, since we need only to identify the compatibility of the invariants of different threads to increase concur￾rency. When reasoning about the lock-based program for this example[21], programmers are required to en￾sure the non-interference between every two threads. And when composing threads, the non-interference be￾tween the newly-added one and all the existent is re￾quired. The concurrency-control mechanism, transac￾tional memory, significantly eases the reasoning. Interestingly, we can perform a similar reasoning for the corresponding high-level programs in Fig.7. We know that (fork1 = fork2) is valid when the trans￾action starts. And the forks are free to pick if (fork1 = 0 = fork2). Then the philosopher will commit his pick￾ing attempts successfully if shared memory has not been updated by the other thread. Finally, shared memory remains in a state that respects the invariant (fork1 = 1 = fork2)