(C,(ae,oo,K()》,n(C,(c2,。,) letⅡinCl..C..‖Cn,(oc,oo,)e(etΠinCl..Ci...Cn,(a2,a。,K{ix') (a)Program Transitions Π(f)=(g,C)【Ele=nx∈dom(oc)k=({y“n以，x,E[skip]) f是dom(四)or【Ele undefined or r是dom(ae) Ef(E)(e)(C;moret,(e)) (E()(e)))nabort k=(01,I,C)[ElGowa =n ae=detxn} [Eloc =n (E[return E]())() :.n(C,(a2,ao,o》 (E[print(E)],())(ou) .n(E[skip],(c,o,)) (C,o wa)t(C',owa)dom(a1)=dom(aj) (noret,）s:ohj.abort t,abort (C,(ae;o;(a1,I,Ce)))n(C',(de,p:(aj,r,Ce))) (b)Thread Transitions IE,lo undefined(1≤j≤i)orx是dom(a) (C;a)(skip,' (C,o)abort (E[x :cons(E1,...,Ei)],a)-tabort (E[(C)].)(E[skip].') (E[(C)],o)-◆t abort (c)Thread Transitions Inside Method Calls Figure 5.Selected Rules of Concrete Operational Semantics (AbsObj)B∈Par一AbsVal (MSpec）Y∈lnt+AbsObj一Imt×AbsObj We use HW,(e,)]to represent the set of histories pro- duced by the executions of W with the initial client memory (0Spec）T={f11,,fn∽m} oc.the object oo,and empty call stacks for all threads,and use (AbsProg)W::=skip with I do Cll...IlC H[W,(e,0)]to generate histories from the abstract program W with the initial client memory oe and the abstract object 0. Figure 6.Object Specification and Abstract Program A legal sequential history H is a history generated by any client using the specification I and an initial abstract object 0. abstract operation generates a pair of invocation and return events TP(8,H)些 atomically.Due to space limit,we give the semantics in TR [18]. 3n,C1,...,Cn:c.HE HI(with I do C1ll...IICn),(c:)l Linearizability.Linearizability [16]is defined using the notion of Then an object is linearizable iff all its completed concurrent histo- histories,which are special event traces H consisting of only object ries are linearizable w.rt.some legal sequential histories. events (i.e.,invocations,returns and object faults). Definition 2(Linearizability of Objects).The object's implemen- Below we use H(i)for the i-th event of H,and H for the tation II is linearizable w.r.t.its specification T under a refinement length of H.Hl represents the sub-history consisting of all the mapping,denoted byⅡ≤eT,if events whose thread id is t.The predicates is_inv(e)and is_res(e) mean that the event e is a method invocation and a response (i.e.,a Vn,C1,...,Cn;de,do,0,H. return or an object fault)respectively.We say a response e2 matches H∈Hl(letΠinC1ll..lCn),(ac,a。)lA(o(ao)=) → an invocation e iff they have the same thread id. 3He,H'.He∈completions(H)AfD(O,H')AHe≤nH A history H is sequential iff the first event of H is an invoca- Here the mapping relates concrete objects to abstract ones: tion,and each invocation,except possibly the last,is immediately followed by a matching response.Then H is well-formed iff,for all (RefMap)p∈Mem一AbsObj t.Ht is sequential.H is complete iff it is well-formed and every The side condition ()=0 in the above definition requires invocation has a matching response.An invocation is pending if no the initial concrete object o to be a well-formed data structure matching response follows it.We handle pending invocations in an representing a valid object 0. incomplete history H following the standard linearizability defini- tion [16]:we append zero or more response events to H,and drop 3.3 Contextual Refinement and Linearizability the remaining pending invocations.Then we get a set of complete Next we define contextual refinement between the concrete object histories.which is denoted by completions(H).We give formal and its specification,and prove its equivalence to linearizability definitions of the above concepts in TR [18]. This equivalence will serve as the basis of our logic soundness w.r.t. Definition 1(Linearizable Histories).Hn H'iff linearizability. Informally,the contextual refinement says,for any set of client 1.∀t.H:=H'; threads,the program W has no more observable behaviors than the 2.there exists a bijectionπ：{l,,lH}→{1，，lH'T}such corresponding abstract program W.Below we use [W,(e,)] that Vi.H(i)=H((i))and to represent the set of observable event traces generated during the i,i.i<jA is-res(H(i)A is_inv(H()=→T()<π(i) executions of W with the initial state (e,)(and empty stacks) It is defined similarly as W,(e,)but now the traces consist That is,H is linearizable w.nt.H'if the latter is a permutation of of observable events only (output events,client faults or object the former,preserving the order of events in the same threads and faults).The observable event traces [w,(c,0)]generated by the order of the non-overlapping method calls. the abstract program is defined similarly 463(Ci, (σc, σo, K(i))) e −→i,Π (C i, (σ c, σ o, κ )) (let Π in C1 ...Ci ...Cn, (σc, σo, K)) e −→ (let Π in C1 ...C i ...Cn, (σ c, σ o, K{i κ })) (a) Program Transitions Π(f)=(y, C) Eσc = n x ∈ dom(σc) κ = ({y n}, x, E[skip ]) (E[ x := f(E) ], (σc, σo, ◦)) (t,f,n) −−−−→t,Π (C; noret, (σc, σo, κ)) f ∈ dom(Π) or Eσc undefined or x ∈ dom(σc) (E[ x := f(E) ], (σc, σo, ◦)) (t,clt,abort) −−−−−−−→t,Π abort κ = (σl, x, C) Eσoσl = n σ c = σc{x n} (E[ return E ], (σc, σo, κ)) (t,ok,n) −−−−−→t,Π (C, (σ c, σo, ◦)) Eσc = n (E[ print(E) ], (σc, σo, ◦)) (t,out,n) −−−−−→t,Π (E[skip ], (σc, σo, ◦)) (noret, s) (t,obj,abort) −−−−−−−→t,Π abort (C, σo σl) −t (C , σ o σ l) dom(σl) = dom(σ l) (C, (σc, σo, (σl, x, Cc))) −→t,Π (C , (σc, σ o, (σ l, x, Cc))) (b) Thread Transitions Ej σ undefined (1 ≤ j ≤ i) or x ∈ dom(σ) (E[ x := cons(E1,...,Ei) ], σ) −t abort (C, σ) −∗ t (skip, σ ) (E[ C ], σ) −t (E[skip ], σ ) (C, σ) −∗ t abort (E[ C ], σ) −t abort (c) Thread Transitions Inside Method Calls Figure 5. Selected Rules of Concrete Operational Semantics (AbsObj) θ ∈ PVar  AbsVal (MSpec) γ ∈ Int → AbsObj  Int × AbsObj (OSpec) Γ ::= {f1 γ1,...,fn γn} (AbsProg) W ::= skip | with Γ do C ...C Figure 6. Object Specification and Abstract Program abstract operation generates a pair of invocation and return events atomically. Due to space limit, we give the semantics in TR [18]. Linearizability. Linearizability [16] is defined using the notion of histories, which are special event traces H consisting of only object events (i.e., invocations, returns and object faults). Below we use H(i) for the i-th event of H, and |H| for the length of H. H|t represents the sub-history consisting of all the events whose thread id is t. The predicates is inv(e) and is res(e) mean that the event e is a method invocation and a response (i.e., a return or an object fault) respectively. We say a response e2 matches an invocation e1 iff they have the same thread id. A history H is sequential iff the first event of H is an invoca￾tion, and each invocation, except possibly the last, is immediately followed by a matching response. Then H is well-formed iff, for all t, H|t is sequential. H is complete iff it is well-formed and every invocation has a matching response. An invocation is pending if no matching response follows it. We handle pending invocations in an incomplete history H following the standard linearizability defini￾tion [16]: we append zero or more response events to H, and drop the remaining pending invocations. Then we get a set of complete histories, which is denoted by completions(H). We give formal definitions of the above concepts in TR [18]. Definition 1 (Linearizable Histories). H lin H iff 1. ∀t. H|t = H |t; 2. there exists a bijection π : {1,..., |H|} → {1,..., |H |} such that ∀i. H(i) = H (π(i)) and ∀i, j. i < j ∧ is res(H(i)) ∧ is inv(H(j)) =⇒ π(i) < π(j). That is, H is linearizable w.r.t. H if the latter is a permutation of the former, preserving the order of events in the same threads and the order of the non-overlapping method calls. We use H [[ W,(σc, σo) ]] to represent the set of histories pro￾duced by the executions of W with the initial client memory σc, the object σo, and empty call stacks for all threads, and use H [[ W,(σc, θ) ]] to generate histories from the abstract program W with the initial client memory σc and the abstract object θ. A legal sequential history H is a history generated by any client using the specification Γ and an initial abstract object θ. Γ  (θ, H) def = ∃n, C1,...,Cn, σc. H ∈ H[ ([ with Γ do C1 ...Cn), (σc, θ) ]] Then an object is linearizable iff all its completed concurrent histo￾ries are linearizable w.r.t. some legal sequential histories. Definition 2 (Linearizability of Objects). The object’s implemen￾tation Π is linearizable w.r.t. its specification Γ under a refinement mapping ϕ, denoted by Π ϕ Γ, iff ∀n, C1,...,Cn, σc, σo, θ, H. H ∈ H[ ([ let Π in C1 ...Cn), (σc, σo) ]] ∧ (ϕ(σo) = θ) =⇒ ∃Hc, H . Hc ∈ completions(H) ∧ Γ  (θ, H ) ∧ Hc lin H Here the mapping ϕ relates concrete objects to abstract ones: (RefMap) ϕ ∈ Mem  AbsObj The side condition ϕ(σo) = θ in the above definition requires the initial concrete object σo to be a well-formed data structure representing a valid object θ. 3.3 Contextual Refinement and Linearizability Next we define contextual refinement between the concrete object and its specification, and prove its equivalence to linearizability. This equivalence will serve as the basis of our logic soundness w.r.t. linearizability. Informally, the contextual refinement says, for any set of client threads, the program W has no more observable behaviors than the corresponding abstract program W. Below we use O [[ W,(σc, σo) ]] to represent the set of observable event traces generated during the executions of W with the initial state (σc, σo) (and empty stacks). It is defined similarly as H [[ W,(σc, σo) ]], but now the traces consist of observable events only (output events, client faults or object faults). The observable event traces O [[ W,(σc, θ) ]] generated by the abstract program is defined similarly. 463