Long Li et al.:Certifying Concurrent Programs Using TM 113 (C,H,t1一T1),,(tn∽Tn）一(C,H,[t一T,,(tk-1一Tk-1),(tkTg),(tk+1Tk+1),(tnTn0 if (C.H,T)(CT)for anyk where (C,H,(H Hw,R,pc,L,B))(C,H,T) if C[pc] then (H T)= addurd,rs,rt (阻，(Hs,Hm,R{ra一R(rs)+R(r)},pc+l,L,B) addiurd,rs,w (H,(田s,Hr,R{ra∽R(rs)+w,pc+1,L,B) suburd,rs,rt (H,(Hs,He,R{rd∽R(rs)-R(r)},pc+1,L,B)】 slturd,rs,rt (H,(Hs,Hw,Rfrd~i,pc+1,L,B))if R(rs)<R(rt),i=1,else i=0 andird,rs,1 (H (H Rrdi},pc+1,L,B))if R(rs)is odd,i=1,else i=0 lwrd,w(rs) (H,(Hs,Hm,R{raHs(Oh,pc+1,(L:(亿，H(),B) ifl走dom(He) (H,(HH,R{rd()},pc+1,L,B)) ifl∈dom(He) where l=R(rs)+Al∈dom(Hs） swrs,w(rd) (H,((HsR(rs)),(HR(rs)),R,pc+1,L,B))if I=R(rd)+wAlE dom(Hs) beqrs,rt:f (H,(Hs:HR,f,L,B)) if R(rs)=R(r) (H,(H.,H,R,pc+1,L,B)) otherwise bners,rt;f (H,(Hs,H,R,f,L,B)) ifR(rs)≠R(re) (H,(Hs H R,pc+1,L,B)) otherwise if (H,(Hs,H,R,f,L,B)) jrrs (H,(s,H如，R,R(r),L,B) starttrans (H (H,,R,pc+1,0,(R,pc))) commit (但yHu),(0,0,R,pc+1,a,B)】 if(L,w)∈L,H()=w (H,(0,B.R,B.pc,0,B)) otherwise Fig.2.Operational semantics counter pc,a log file L for recording the read attempts point.This thread model is enforced by allowing any of its transaction,and a back-up file B for restoring the thread (id tk)to execute at any program point in the state of a transaction when it rolls back.Here we ignore definition of the step function.Thus,we define an in- the fact that a thread may have a private data heap of terleaving model for multi-threaded machines where the its own,because the private data heap does not consist instructions of individual thread execute with sequen- of shared data and it can be treated as an extension of tial consistency. the register file. The register file R maps registers to natural values. The operational semantics for most instructions are quite straightforward.We focus on the transaction re- The log file L records the heap address and the value it lated instructions here.The starttrans instruction stores for every read when executing a transaction.And signals the start of a transaction.It initializes the write the back-up file B records the state of the register file R set H and the log file L to empty and saves current and the program counter pc when a transaction starts. The set of instructions we present here are the com- register file R and program counter pc to the back-up file B to recover the state of the transaction when it rolls monly used subset in RISC machines with additional instructions marking the start (starttrans)and the back.It also copies the global heap H to its local copy H.to act as its view to the global heap when execut- end (commit)of a transaction. ing inside a transaction.The commit instruction checks The step function (of a program P is defined in whether the log file L is consistent with current global Fig.2.The auxiliary function (C,H,T)(C,H,T) heap H.If "yes",the transaction is allowed to commit is used to define the effects of the execution of a thread its effects H to the global heap H.If"no",register file Tk.Here we follow the preemptive thread model where and program counter are restored from the back-up file execution of threads can be preempted at any program B to restart the transaction.For both cases,the localLong Li et al.: Certifying Concurrent Programs Using TM 113 (C, H, [(t1 à T1), . . . , (tn à Tn)]) 7−→ (C, H0 , [(t1 à T1), . . . , (tk−1 à Tk−1), (tk à T 0 k ), (tk+1 à Tk+1), . . . , (tn à Tn)]) if (C, H, Tk) k 7−→(C, H0 , T 0 k ) for any k where (C, H, (Hs, Hw, R, pc, L, B)) k 7−→(C, H0 , T 0 ) if C[pc] = then (H0 , T 0 ) = addu rd, rs, rt (H, (Hs, Hw, R{rd à R(rs) + R(rt)}, pc+1, L, B)) addiu rd, rs, w (H, (Hs, Hw, R{rd à R(rs) + w}, pc+1, L, B)) subu rd, rs, rt (H, (Hs, Hw, R{rd à R(rs) − R(rt)}, pc+1, L, B)) sltu rd, rs, rt (H, (Hs, Hw, R{rd à i}, pc+1, L, B)) if R(rs) < R(rt), i = 1, else i = 0 andi rd, rs, 1 (H, (Hs, Hw, R{rd à i}, pc+1, L, B)) if R(rs) is odd, i = 1, else i = 0 lw rd, w(rs) (H, (Hs, Hw, R{rd à Hs(l)}, pc+1, (L :: (l, Hs(l))), B)) if l /∈ dom(Hw) (H, (Hs, Hw, R{rd à Hs(l)}, pc+1, L, B)) if l ∈ dom(Hw) where l = R(rs) + w ∧ l ∈ dom(Hs) sw rs, w(rd) (H, ((Hs{l à R(rs)}), (Hw ] {l à R(rs)}), R, pc+1, L, B)) if l = R(rd) + w ∧ l ∈ dom(Hs) beq rs, rt, f (H, (Hs, Hw, R, f, L, B)) if R(rs) = R(rt) (H, (Hs, Hw, R, pc+1, L, B)) otherwise bne rs, rt, f (H, (Hs, Hw, R, f, L, B)) if R(rs) 6= R(rt) (H, (Hs, Hw, R, pc+1, L, B)) otherwise j f (H, (Hs, Hw, R, f, L, B)) jr rs (H, (Hs, Hw, R, R(rs), L, B)) starttrans (H, (H, ∅, R, pc+1, ∅, (R, pc))) commit ((H ] Hw), (∅, ∅, R, pc+1, ∅, B)) if ∀ (l, w) ∈ L, H(l) = w (H, (∅, ∅, B.R, B.pc, ∅, B)) otherwise Fig.2. Operational semantics. counter pc, a log file L for recording the read attempts of its transaction, and a back-up file B for restoring the state of a transaction when it rolls back. Here we ignore the fact that a thread may have a private data heap of its own, because the private data heap does not consist of shared data and it can be treated as an extension of the register file. The register file R maps registers to natural values. The log file L records the heap address and the value it stores for every read when executing a transaction. And the back-up file B records the state of the register file R and the program counter pc when a transaction starts. The set of instructions we present here are the com￾monly used subset in RISC machines with additional instructions marking the start (starttrans) and the end (commit) of a transaction. The step function (7−→) of a program P is defined in Fig.2. The auxiliary function (C, H,Tk) k 7−→(C, H0 ,T 0 k ) is used to define the effects of the execution of a thread Tk. Here we follow the preemptive thread model where execution of threads can be preempted at any program point. This thread model is enforced by allowing any thread (id tk) to execute at any program point in the definition of the step function. Thus, we define an in￾terleaving model for multi-threaded machines where the instructions of individual thread execute with sequen￾tial consistency. The operational semantics for most instructions are quite straightforward. We focus on the transaction re￾lated instructions here. The starttrans instruction signals the start of a transaction. It initializes the write set Hw and the log file L to empty and saves current register file R and program counter pc to the back-up file B to recover the state of the transaction when it rolls back. It also copies the global heap H to its local copy Hs to act as its view to the global heap when execut￾ing inside a transaction. The commit instruction checks whether the log file L is consistent with current global heap H. If “yes”, the transaction is allowed to commit its effects Hw to the global heap H. If “no”, register file and program counter are restored from the back-up file B to restart the transaction. For both cases, the local