114 J.Comput.Sci.Technol.,Jan.2009,Vol.24.No.1 heap Hs,write set H and log file L are set empty when the transaction completes.Since the intermedi- The lw and sw instructions operate on local heap H ate state of a transaction is not visible to the other only.Thus all the access attempts to the global heap H threads.the violation of the invariant will not be ob- are required to operate on the local copy Hs first and served by other threads,the global heap will always be take effect on the global heap H until the correspond- in a consistent state that respects the invariant.To en- ing transaction commits.So the non-transactional ac force such reasoning,we track the state of thread-local cess to shared memory H is denied.The lw instruction data structures during the execution of a thread to en- reads data and appends the log file L when the ad- sure that the desired properties are correctly enforced. dress it reads from is not in the domain of the write And we also make sure that the update operation on set H.The sw instruction updates the local heap H. the global heap does not violate the invariant on the directly and performs a unique merge on the write set global heap. H recording its write attempt to the global heap H. Fig.3 defines the specification constructs in our sys- The function defines a unique merge on heaps as tem for such reasoning.A program specification con- follows: sists of a global invariant Inv and code heap specifica- tions for threads.The global invariant Inv speci- V1.(Ha出H6)()= H6(),1∈H6; fies the restrictions on the global heap H when multi- Ha (1),I ple threads are working on it concurrently.The code heap specification maps labels to preconditions.The The abstract machine records the values but not the global invariant Inv and the precondition p for an in- versions of the global heap in logs as what Herlihy et struction together form the expectations at that pro- al.7 have done and identifies the consistency of the log gram point. file L by checking whether all logged tuples (l,w)reflect the mapping relation in H（付(l,w)∈L,H()=w) The implementation strategies of data versioning and (State) S::=(H,Hs,Hw,R,pc,L,B) conflict detection may vary in different TM systems. (Pstate)Sp ::=(Hs,H,R,pc,B) However,verification should check the consistency of (Spred)p ∈Pstate-Prop both branches no matter what mechanisms cause the (Invariant)Inv E Heap-Prop control fow to branch.So we implement a relatively (ProgSpec）Φ=(nU,1,.,乎n]) simple mechanism in the abstract machine to remove the nondeterminacy of the system. (CdHpSpec）Ψ：={fp}" (Coerc)S]::(Hs;H:R,pc,B) As shown in Fig.2.all instructions operate on local data structures of threads except commit.So the effects Fig.3.Specification syntax (on the global heap)of a transaction are not visible to other threads until the transaction commits.The isola- The validity of a precondition depends on the lo- tion property is properly established.Also the update cal data structures only.Note that the log file L is operation on the global heap and the rollback operation excluded,because programmers will not observe the on local structures are defined to finish in a single step, transitions of the log file and the well-formedness of we achieve atomicity by definitions. a commit instruction relies on the well-formedness of The abstract machine we present here may have both branches,the state of the log file is not vital. poor performance due to redundant rollbacks:success- ful commit of other threads will always cause a trans- 3.3 Inference Rules action to roll back,if the transaction has a read from The inference rules for a program are shown in Fig.4, the address that is just updated,no matter it happens and the rules for instructions are shown in Fig.5.We before(conflict occurs)or after that commit (should be use the following judgement forms to define the infer- fine).But it defines a semantics of TM systems strictly ence rules: and works fine with reasoning as we show later. Φ，p,,pn上P (well-formed program), 3.2 Program Specifications 亚，Inw上{p}(C,H,T) (well-formed thread). 亚，Inw上C:亚' (well-formed code heap), In our system,transactions are identified as atomic 亚，Imw上{p}f:I (well-formed instr.sequence). operations that modify the global heap with respect to certain invariant.This invariant may be violated during A program is well-formed if the global heap respects the execution of a transaction,but will be reestablished the invariant on it and every thread of the program is114 J. Comput. Sci. & Technol., Jan. 2009, Vol.24, No.1 heap Hs, write set Hw and log file L are set empty. The lw and sw instructions operate on local heap Hs only. Thus all the access attempts to the global heap H are required to operate on the local copy Hs first and take effect on the global heap H until the correspond￾ing transaction commits. So the non-transactional ac￾cess to shared memory H is denied. The lw instruction reads data and appends the log file L when the ad￾dress it reads from is not in the domain of the write set Hw. The sw instruction updates the local heap Hs directly and performs a unique merge on the write set Hw recording its write attempt to the global heap H. The function ] defines a unique merge on heaps as follows: ∀ l. (Ha ] Hb) (l) = ½ Hb (l), l ∈ Hb; Ha (l), l 6∈ Hb. The abstract machine records the values but not the versions of the global heap in logs as what Herlihy et al.[7] have done and identifies the consistency of the log file L by checking whether all logged tuples (l, w) reflect the mapping relation in H (∀ (l, w) ∈ L, H(l) = w). The implementation strategies of data versioning and conflict detection may vary in different TM systems. However, verification should check the consistency of both branches no matter what mechanisms cause the control flow to branch. So we implement a relatively simple mechanism in the abstract machine to remove the nondeterminacy of the system. As shown in Fig.2, all instructions operate on local data structures of threads except commit. So the effects (on the global heap) of a transaction are not visible to other threads until the transaction commits. The isola￾tion property is properly established. Also the update operation on the global heap and the rollback operation on local structures are defined to finish in a single step, we achieve atomicity by definitions. The abstract machine we present here may have poor performance due to redundant rollbacks: success￾ful commit of other threads will always cause a trans￾action to roll back, if the transaction has a read from the address that is just updated, no matter it happens before (conflict occurs) or after that commit (should be fine). But it defines a semantics of TM systems strictly and works fine with reasoning as we show later. 3.2 Program Specifications In our system, transactions are identified as atomic operations that modify the global heap with respect to certain invariant. This invariant may be violated during the execution of a transaction, but will be reestablished when the transaction completes. Since the intermedi￾ate state of a transaction is not visible to the other threads, the violation of the invariant will not be ob￾served by other threads, the global heap will always be in a consistent state that respects the invariant. To en￾force such reasoning, we track the state of thread-local data structures during the execution of a thread to en￾sure that the desired properties are correctly enforced. And we also make sure that the update operation on the global heap does not violate the invariant on the global heap. Fig.3 defines the specification constructs in our sys￾tem for such reasoning. A program specification Φ con￾sists of a global invariant Inv and code heap specifica￾tions Ψ for threads. The global invariant Inv speci- fies the restrictions on the global heap H when multi￾ple threads are working on it concurrently. The code heap specification Ψ maps labels to preconditions. The global invariant Inv and the precondition p for an in￾struction together form the expectations at that pro￾gram point. (State) S ::= (H, Hs, Hw, R, pc, L, B) (Pstate) Sp ::= (Hs, Hw, R, pc, B) (Spred) p ∈ Pstate → Prop (Invariant) Inv ∈ Heap → Prop (ProgSpec) Φ ::= (Inv, [Ψ1, . . . , Ψn]) (CdHpSpec) Ψ ::= {f à p} ∗ (Coerc) [[S]] ::= (Hs, Hw, R, pc, B) Fig.3. Specification syntax. The validity of a precondition depends on the lo￾cal data structures only. Note that the log file L is excluded, because programmers will not observe the transitions of the log file and the well-formedness of a commit instruction relies on the well-formedness of both branches, the state of the log file is not vital. 3.3 Inference Rules The inference rules for a program are shown in Fig.4, and the rules for instructions are shown in Fig.5. We use the following judgement forms to define the infer￾ence rules: Φ, [p1, . . . , pn] ` P (well-formed program), Ψ,Inv ` {p} (C, H, T) (well-formed thread), Ψ,Inv ` C : Ψ 0 (well-formed code heap), Ψ,Inv ` {p} f : I (well-formed instr. sequence). A program is well-formed if the global heap respects the invariant on it and every thread of the program is