112 J.Comput.Sci.Technol.,Jan.2009,Vol.24.No.1 the transaction aborts,the undo log is used to restore To focus on the reasoning issue,we model the ab- the old version of data stract machine with strict semantics of atomicity and Lazy versioning buffers all new data versions until isolation and require that all access to shared data must the transaction completes.The new versions will be appear within transactions.The TM system in our sys- copied to the actual memory when the transaction com- tem will be a lazy versioning.lazy conflict detection mits.If the transaction aborts,the buffer is discarded system.Being at the assembly level,the granularity of and no further compensation is needed. conflict detection is naturally word-level.And we do Conflict detection signals the multiple access to the not support nested transaction for now since it is much same data with at least one transaction attempting more a performance consideration than the semantics to write a new version.Detection relies on tracking of transaction basis.We leave this to our future work. the read set (addresses read from)and write set (ad- dresses written to)for each transaction.Under eager 3 The System conflict detection,the system checks for conflicts when- ever transactions read or write data.While under lazy In this section,we first present an abstract machine conflict detection,all checks are delayed until the end with transaction structures and its operational seman- of each transaction (i.e.,when it tries to commit). tics.Then we present a program logic of this machine for reasoning. 2.2 Violations 3.1 Abstract Machine TM systems are supposed to enforce the properties of atomicity(all-or-nothing)and isolation (intermedi- Fig.1 defines the abstract machine and the syntax ate state not visible to other threads).But practical of the assembly language.A program P consists of a implementations may violate these properties more or code heap C,a global shared data heap H(referred to less and may lead to unexpected behaviors of programs as a "global heap"in the remainder of this paper)and using TM as follows numbers of threads TS working on the global heap con- Atomicity Violation.In practice,the rollback op- currently.The code heap C maps labels to instructions. eration of eager versioning and the commit operation of The data heap H maps heap addresses to natural values. lazy versioning are time-consuming.If the TM system And the threads TS are modeled as a partial mapping allows other threads to access the data which rollback from thread id t(natural numbers)to its owner thread or commit may modify during their execution,threads T.Each thread T consists of a local view of the global may get invalid data (read data ahead of rollback or heap H.(referred to as a "local heap"in the remainder commit operations)or lose update (write data ahead). of this paper),a write set Hw for recording the write The solution is to claim exclusiveness for the data that attempts of its transaction,a register file R,a program rollback or commit is about to access before their exe- cution. (Program) :=(C,H,T3) Isolation Violation.Threads may see the inter- (Threads) TS :={t∽T}* (Thread) T mediate state of a transaction when implementations = (Hs:HR,pc,L:B) (BackFile) of eager versioning do not claim exclusiveness for the :=(R,pc) addresses it writes to.Blundell et al.4 discussed this (CodeHeap) 0 ={f…}" (Heap) H.Hs = issue and called it weak atomicity. w) (WriteSet) Hw :={亿w}* Privatization Issue.The atomicity and isolation (LogFile) 8= (L,w)::L properties of TM systems do not specify whether the (RegFile) = {r4w}" access to shared data is allowed to bypass the TM sys- (Reg) 三 {rkk∈o31 tem's mechanisms (outside transactions).If "yes",it (Labels)t,f,l,pc:= n (nat nums) introduces the privatization problem25)we will not ad- (WordVal) ::=n (nat nums) dress for now.If "no",then TM systems should han- (Instr） :addurd,rs,rt l addiurd,rs,w dle the access to shared data outside transactions too, suburd,rs,rt|slturd,rs,rt because they may lead to unexpected behaviors of pro- I andird:rs:1 lw rd;w(rs) grams.Shpeisman et al.26]discussed this problem and I sw rs,w(rd)|begrs,rt,f solved it by adding barriers with respect to TM system I bners,rt,f ljfljrrs for every access to memory outside transactions.These starttrans commit barriers can be treated as featherweight transactions in (InstrSeq) our opinion. Fig.1.Machine syntax.112 J. Comput. Sci. & Technol., Jan. 2009, Vol.24, No.1 the transaction aborts, the undo log is used to restore the old version of data. Lazy versioning buffers all new data versions until the transaction completes. The new versions will be copied to the actual memory when the transaction com￾mits. If the transaction aborts, the buffer is discarded and no further compensation is needed. Conflict detection signals the multiple access to the same data with at least one transaction attempting to write a new version. Detection relies on tracking the read set (addresses read from) and write set (ad￾dresses written to) for each transaction. Under eager conflict detection, the system checks for conflicts when￾ever transactions read or write data. While under lazy conflict detection, all checks are delayed until the end of each transaction (i.e., when it tries to commit). 2.2 Violations TM systems are supposed to enforce the properties of atomicity (all-or-nothing) and isolation (intermedi￾ate state not visible to other threads). But practical implementations may violate these properties more or less and may lead to unexpected behaviors of programs using TM as follows. • Atomicity Violation. In practice, the rollback op￾eration of eager versioning and the commit operation of lazy versioning are time-consuming. If the TM system allows other threads to access the data which rollback or commit may modify during their execution, threads may get invalid data (read data ahead of rollback or commit operations) or lose update (write data ahead). The solution is to claim exclusiveness for the data that rollback or commit is about to access before their exe￾cution. • Isolation Violation. Threads may see the inter￾mediate state of a transaction when implementations of eager versioning do not claim exclusiveness for the addresses it writes to. Blundell et al.[24] discussed this issue and called it weak atomicity. • Privatization Issue. The atomicity and isolation properties of TM systems do not specify whether the access to shared data is allowed to bypass the TM sys￾tem’s mechanisms (outside transactions). If “yes”, it introduces the privatization problem[25] we will not ad￾dress for now. If “no”, then TM systems should han￾dle the access to shared data outside transactions too, because they may lead to unexpected behaviors of pro￾grams. Shpeisman et al.[26] discussed this problem and solved it by adding barriers with respect to TM system for every access to memory outside transactions. These barriers can be treated as featherweight transactions in our opinion. To focus on the reasoning issue, we model the ab￾stract machine with strict semantics of atomicity and isolation and require that all access to shared data must appear within transactions. The TM system in our sys￾tem will be a lazy versioning, lazy conflict detection system. Being at the assembly level, the granularity of conflict detection is naturally word-level. And we do not support nested transaction for now since it is much more a performance consideration than the semantics of transaction basis. We leave this to our future work. 3 The System In this section, we first present an abstract machine with transaction structures and its operational seman￾tics. Then we present a program logic of this machine for reasoning. 3.1 Abstract Machine Fig.1 defines the abstract machine and the syntax of the assembly language. A program P consists of a code heap C, a global shared data heap H (referred to as a “global heap” in the remainder of this paper) and numbers of threads TS working on the global heap con￾currently. The code heap C maps labels to instructions. The data heap H maps heap addresses to natural values. And the threads TS are modeled as a partial mapping from thread id t (natural numbers) to its owner thread T. Each thread T consists of a local view of the global heap Hs (referred to as a “local heap” in the remainder of this paper), a write set Hw for recording the write attempts of its transaction, a register file R, a program (Program) P ::= (C, H, TS) (Threads) TS ::= {t à T} ∗ (Thread) T ::= (Hs, Hw, R, pc, L, B) (BackFile) B ::= (R, pc) (CodeHeap) C ::= {f à ι} ∗ (Heap) H, Hs ::= {l à w} ∗ (WriteSet) Hw ::= {l à w} ∗ (LogFile) L ::= ∅ | (l, w) :: L (RegFile) R ::= {r à w} ∗ (Reg) r ::= {rk} k∈{0,...,31} (Labels) t, f, l, pc ::= n (nat nums) (WordVal) w ::= n (nat nums) (Instr) ι ::= addu rd, rs, rt | addiu rd, rs, w | subu rd, rs, rt | sltu rd, rs, rt | andi rd, rs, 1 | lw rd, w(rs) | sw rs, w(rd) | beq rs, rt, f | bne rs, rt, f | j f | jr rs | starttrans | commit (InstrSeq) I ::= ι | ι;I Fig.1. Machine syntax