Long Li et al.:Certifying Concurrent Programs Using TM 115 well-formed.Thus the verification of a multi-threaded A thread is well-formed if the precondition of the program can be decomposed into the verification of its thread is satisfied and the invariant on the global heap component threads.The reasoning is thread-modular holds.Also the code heap and the instruction sequence in our system. the thread is going to execute are required to be well- formed. 电，p1,.,pn]-P(Well-formed program) And a code heap is well-formed only if every instruc- tion sequence of it is well-formed. Φ=(nu,[1,,n]） Most inference rules for instruction sequence are similar and grouped in the SEQ rule.It requires that Inv H k.乎k,Inu上{pg}(C,H,TS(tk) (PROG) the precondition together with the global invariant en- Φ，p1,pnF(C,H,TS) sures the safe execution of the instruction:and that the 亚，Inur{p}(C,H,T)(Wel-formed thread) resulting state respects the global invariant and satis- Inv H p (HsHw,R,f,B) fies the postcondition which also serves as the precon- dition of the remaining instruction sequence.Note that 亚，Inw上C:亚亚，lmu上{p}f:C[] 业，Inw上{p}(C,H,(H,Hw,R,f,L,B) (THRD) the STARTTRANS rule is also grouped in SEQ rule.Even though the instruction copies the global heap to its local 亚，InvHC:亚(We--formed code heap) heap,it does not need special treatment for its behav- Hf∈dom():重，Inek{w'(f》f:Cf] ior. (CDHP) 乎，nu上C:亚 The BNE and BEQ rules are similar and we present one here.Also they do not make much difference from the Fig.4.Inference rules. SEQ rule except that they check both branches where the control fow will switch depending on the equiva- lence of the values that corresponding registers store. Invp}f:I(Well-formed instruction sequence) The J and JR rules require that it is safe to make a 亚(B.pc)=p"亚，Inu上{p}f+1:I jump to the target address and the global invariant is VS.ImuS.HApS→V(L,w)∈S.L,S.H(0=w preserved after jumping. Inv (Step (S)).HA p'[Step (S)] The COMMIT rule is similar to the BEQ rule except S.InuS.HAp[→(L,w)∈s.L,s.H(U)=w that it branches due to the consistence of the log file. -Inv (Step (S)).H p"[Step(S)] It checks that both successful commit case and roll- (COMMIT) back case are well-formed.And the requirement that Ψ，nuF{p}f:commit:I the resulting state respects the global invariant after 亚(f')=p successful commit actually claims for the checking of S.ImuS.HAp→ the update made by the successfully committed trans- Inv (Step (S)).HA p'[Step (S)] () action on the global heap H.Furthermore,it is easy Ψ，Inwr{p}f:jf' to show that rollback is always allowed.A rollback is (R(r)》=p caused by an update on the global heap.Since we will HS.Invs.HApS→ restore local data structures of transactions,the differ- Inv (Step (S)).HA p'[Step (S)] ence of start and rollback state of a transaction is the (JR) 乎，lnw卜{p}f:jrrs global heap only.But all updates on the global heap (f')=p”重，nwk{p}f+1:I are required to respect the global invariant,and the precondition relies on local data structures only.So it VS.Inv S.HA p [S]-S.R(ra)=S.R(rt) is always safe to roll back a transaction. -Inv (Step (S)).H p"[Step (S)] As shown in the inference rules,the invariant on the HS.Imvs.HAp一s.R(rs)≠s.R(r) Inv (Step (S)).H p'[Step (S)] global heap is required to preserve for every instruc- (BEQ) tion rule,so the invariant on the global heap is guar- 亚，Inu下{p}f:beg rs,rt,f':I anteed all through the program.And the transitions of Efaddu,addiu,subu,sltu,andi,Iw,sw,starttrans} a thread are tracked in the preconditions of its instruc- 业，nw上{p}f+1:I tions. VS.nuS.HApS一 Inv(Step(S)).Hp'[Step (S)] 3.4 Soundness (SEQ) Ψ，Inw上{p}f:;I The soundness of these inference rules with re- Fig.5.Inference rules cont'. spect to the operational semantics of the abstract ma-Long Li et al.: Certifying Concurrent Programs Using TM 115 well-formed. Thus the verification of a multi-threaded program can be decomposed into the verification of its component threads. The reasoning is thread-modular in our system. Φ, [p1, . . . , pn] ` P (Well-formed program) Φ = (Inv, [Ψ1, . . . , Ψn]) Inv H ∀ k. Ψk, Inv ` {pk} (C, H, TS(tk)) Φ, [p1, . . . , pn] ` (C, H, TS) (prog) Ψ, Inv ` {p} (C, H, T) (Well-formed thread) Inv H p (Hs, Hw, R, f, B) Ψ, Inv ` C : Ψ Ψ, Inv ` {p} f : C[f] Ψ, Inv ` {p} (C, H, (Hs, Hw, R, f, L, B)) (thrd) Ψ, Inv ` C : Ψ0 (Well-formed code heap) ∀ f ∈ dom(Ψ0 ) : Ψ, Inv ` {Ψ0 (f)} f : C[f] Ψ, Inv ` C : Ψ0 (cdhp) Fig.4. Inference rules. Ψ, Inv ` {p} f : I (Well-formed instruction sequence) Ψ(B.pc) = p 00 Ψ, Inv ` {p 0} f +1 : I ∀ S. Inv S.H ∧ p [[S]] → ∀ (l, w) ∈ S.L, S.H(l) = w → Inv (Step (S)).H ∧ p 0 [[Step (S)]] ∀ S. Inv S.H ∧ p [[S]] → ¬∀ (l, w) ∈ S.L, S.H(l) = w → Inv (Step (S)).H ∧ p 00 [[Step (S)]] Ψ, Inv ` {p} f : commit;I (commit) Ψ(f 0 ) = p 0 ∀ S. Inv S.H ∧ p [[S]] → Inv (Step (S)).H ∧ p 0 [[Step (S)]] Ψ, Inv ` {p} f : j f 0 (j) Ψ(R(rs)) = p 0 ∀ S. Inv S.H ∧ p [[S]] → Inv (Step (S)).H ∧ p 0 [[Step (S)]] Ψ, Inv ` {p} f : jr rs (jr) Ψ(f 0 ) = p 00 Ψ, Inv ` {p 0} f +1 : I ∀ S. Inv S.H ∧ p [[S]] → S.R(rs) = S.R(rt) → Inv (Step (S)).H ∧ p 00 [[Step (S)]] ∀ S. Inv S.H ∧ p [[S]] → S.R(rs) 6= S.R(rt) → Inv (Step (S)).H ∧ p 0 [[Step (S)]] Ψ, Inv ` {p} f : beq rs, rt, f0 ;I (beq) ι ∈ {addu, addiu, subu, sltu, andi, lw, sw, starttrans} Ψ, Inv ` {p 0} f +1 : I ∀ S. Inv S.H ∧ p [[S]] → Inv (Step (S)).H ∧ p 0 [[Step (S)]] Ψ, Inv ` {p} f : ι;I (seq) Fig.5. Inference rules cont’. A thread is well-formed if the precondition of the thread is satisfied and the invariant on the global heap holds. Also the code heap and the instruction sequence the thread is going to execute are required to be well￾formed. And a code heap is well-formed only if every instruc￾tion sequence of it is well-formed. Most inference rules for instruction sequence are similar and grouped in the SEQ rule. It requires that the precondition together with the global invariant en￾sures the safe execution of the instruction; and that the resulting state respects the global invariant and satis- fies the postcondition which also serves as the precon￾dition of the remaining instruction sequence. Note that the STARTTRANS rule is also grouped in SEQ rule. Even though the instruction copies the global heap to its local heap, it does not need special treatment for its behav￾ior. The BNE and BEQ rules are similar and we present one here. Also they do not make much difference from the SEQ rule except that they check both branches where the control flow will switch depending on the equiva￾lence of the values that corresponding registers store. The J and JR rules require that it is safe to make a jump to the target address and the global invariant is preserved after jumping. The COMMIT rule is similar to the BEQ rule except that it branches due to the consistence of the log file. It checks that both successful commit case and roll￾back case are well-formed. And the requirement that the resulting state respects the global invariant after successful commit actually claims for the checking of the update made by the successfully committed trans￾action on the global heap H. Furthermore, it is easy to show that rollback is always allowed. A rollback is caused by an update on the global heap. Since we will restore local data structures of transactions, the differ￾ence of start and rollback state of a transaction is the global heap only. But all updates on the global heap are required to respect the global invariant, and the precondition relies on local data structures only. So it is always safe to roll back a transaction. As shown in the inference rules, the invariant on the global heap is required to preserve for every instruc￾tion rule, so the invariant on the global heap is guar￾anteed all through the program. And the transitions of a thread are tracked in the preconditions of its instruc￾tions. 3.4 Soundness The soundness of these inference rules with re￾spect to the operational semantics of the abstract ma-