(n.sStmt） ::=skip c return E noret (②，)=pxqf卡pA'=q linself lin(E)trylinself (②，)=fΣ卡p∧= I trylin(E)I commit(p)(C)C;C (∑，)=R1*R2if if(B)C else C while (B)C) 21,2,1,兴：（公=*2）Λ(=*) (RelState) =(a,△) A(②1，)FRA(②2，)卡R2 (SpecSer) ={(U1,01),,(Um,8n)} (∑，)=R1⊕R2if (PendThrds) U =(tiT1,...,tnTn} 81,2,1,(公=1⊕2)Λ（②=1⊕） A(②1，)FB1A(②2，)FR2 (AbsOp) r:=(y,n)I (end,n) (RelAss)p,q,I::=true false E=E emp EE Id true] True些true x true Ix→E|E-(Y,E)IE一(end,E) Y(m)(0)=(m',8)(△，n)二（△'，n') 1p*91p⊕gpV9I·: (RelAct)R,G:=pxqI可|R*R|R⊕R|.· (0,n)三(@，n') ({U,)}y△，n)2({U,)》}世△'，n') E,plyE',gl iff Figure 7.Instrumented Code and Relational State Model o,△，n.(a,△)上(E=n)*p =3△'，n'.(△，n)二（△'，n')A(a,△）上(E=n)*g ·兰{(0,0)} where·∈SpecSer I R iff([I]→R)A(R→I×I)A Precise(I) fLg dom(f)n dom(g)=0 △1#△2些U1⊥U2Aa1⊥02，where(W1,01)∈△1A(U2,2)∈△2 Figure 9.Semantics of Actions △1*△2兰{(U1sU2,01w02)1(U1,a1)∈△1A(U2,02)∈△2} 81*2兰(o1w2,△1*△2) Although our logic is based on LRG [8].this approach is mostly in- dependent with the base logic.Similar extensions can also be made where∑1=（(a1,△1)，∑2=(a2,△2)，a1⊥o2and△1t△2 1⊕2些a,AUA2)f=(a,△1)and2=(o,△2) over other logics,such as RGSep [32]. Our logic is proposed to verify object methods only.Verified undefined otherwise object methods are guaranteed to be a contextual refinement of their abstract atomic operations,which ensures linearizability of {E。些IEl. if dom(a)=fv(E) the object.We discuss verification of whole programs consisting of undefined otherwise both client code and object code at the end of Sec.4.3. (o,△)=E=E2if{(E1=E2)}。=trueA△=· (a,△)上emp ifa=0A△=● 4.1 Instrumented Code and States (o,△)=E→E2if3L,n,σ'.{(E1,E2)}。'=(L.n) In Fig.7 we show the syntax of the instrumented code and its Λo=a出{l一n}A△=· state model.As explained in Sec.2.program states for the (a,△)卡x片Eif3n,0.{E}。=nA0={x∽n object method executions now consist of two parts,the physical A△={(08)} object states o and the auxiliary data A.A is a nonempry set of (a,△)FE1一(，E2）if3a1,o2,t,n.a=o1wo2 (0)pairs,each pair representing a speculation of the situation AtE1=tAE2=n at the abstract level.Here 0 is the current abstract object,and A△={({t…(Y,n)},0)} U is a pending thread pool recording the remaining operation to (o,△)卡E一(end,E2)if3o1,2,t,n.a=1yo2 be fulfilled by each thread.It maps a thread id to its remaining A{E1Na1=tA《E2》.2=n abstract operation.which is either(,n)(the operation y needs to A△={({t(end,n),0)} be executed with argument n)or (end,n)(the operation has been ∑卡p*9if321,22.2=B1*22A1FpA2卡9 finished with the return value n).We assume A is always domain- 2卡p⊕9if1,2.2=1⊕22A1FpA22F9 exact,defined as follows: SpecExact(p)if△，△'.(，△)=p)A(-,△)=p)=→（△=△） DomExact(△)gU,8,U',.(U,8)∈△A(U',8)∈△ dom(U)=dom(U)A dom(0)=dom(0'). Figure 8.Semantics of State Assertions It says,all the speculations in A should describe the same set of threads and the same domain of abstract objects.Any A containing a single speculation is domain-exact.Also domain-exactness can Definition 3(Contextual Refinement).IICT iff be preserved under the step of any command in our instrumented n,C1, ·,Cnoc,ao,8.p(a。)=8 language,thus it is reasonable to assume it always holds. ≠Ol(letΠinCl..lCn),(ac,aa)l Below we informally explain the effects over A of the newly CoI(with r do Cill...Il Cn),(e,0)]. introduced commands.We leave their formal semantics to Sec.4.4. The auxiliary command linself executes the unfinished abstract op- Following Filipovic et al.[9].we can prove that linearizability is eration of the current thread in every 0 in A,and changes the ab- equivalent to contextual refinement.We give the proofs in TR [18]. stract object 0 correspondingly.lin(E)executes the abstract opera- Theorem4(Equivalence).Π≤，T←→ⅡgeT. tion of the thread with id E.linself or lin(E)is executed when we know for sure that a step is the linearization point.The trylinself 4.A Relational Rely-Guarantee Style Logic command introduces uncertainty.Since we do not know if the ab- stract operation of the current thread is fulfilled or not at the cur- To prove object linearizability,we first instrument the object imple- rent point,we consider both possibilities.For each ()pair in A mentation by introducing auxiliary states and auxiliary commands that contains unfinished abstract operation of the current thread,we which relate the concrete code with the abstract object and oper- add in Aa new speculation (where the abstract operation ations.Our program logic extends LRG [8]with a relational in- is done and is the resulting abstract object.Since the original terpretation of assertions and new rules for auxiliary commands (U,0)is also kept,we have both speculations in A.Similarly,the 464(InsStmt) C ::= skip | c | return E | noret | linself | lin(E) | trylinself | trylin(E) | commit(p) | C | C; C | if (B) C else C | while (B){C} (RelState) Σ ::= (σ, Δ) (SpecSet) Δ ::= {(U1, θ1),..., (Un, θn)} (PendThrds) U ::= {t1 Υ1,...,tn Υn} (AbsOp) Υ ::= (γ,n) | (end, n) (RelAss) p, q, I ::= true | false | E = E | emp | E → E | x ⇒ E | E (γ,E) | E (end, E) | p ∗ q | p ⊕ q | p ∨ q | ... (RelAct) R, G ::= p q | [p] | R ∗ R | R ⊕ R | ... Figure 7. Instrumented Code and Relational State Model • def = {(∅, ∅)} where • ∈ SpecSet f⊥g def = dom(f) ∩ dom(g) = ∅ Δ1 Δ2 def = U1⊥U2 ∧ θ1⊥θ2 , where (U1,θ1)∈Δ1 ∧ (U2,θ2)∈Δ2 Δ1 ∗ Δ2 def = {(U1 U2, θ1 θ2) | (U1,θ1)∈Δ1 ∧ (U2,θ2)∈Δ2} Σ1 ∗ Σ2 def = (σ1 σ2, Δ1 ∗ Δ2) where Σ1 = (σ1, Δ1), Σ2 = (σ2, Δ2), σ1⊥σ2 and Δ1 Δ2 Σ1 ⊕ Σ2 def = (σ, Δ1∪Δ2) if Σ1 = (σ,Δ1) and Σ2 = (σ,Δ2) undefined otherwise {{E}}σ def = Eσ if dom(σ) = fv(E) undefined otherwise (σ, Δ) |= E1 = E2 iff {{(E1 = E2)}}σ = true ∧ Δ = • (σ, Δ) |= emp iff σ = ∅ ∧ Δ = • (σ, Δ) |= E1 → E2 iff ∃l, n, σ . {{(E1, E2)}}σ = (l, n) ∧ σ = σ {l n} ∧ Δ = • (σ, Δ) |= x ⇒ E iff ∃n, θ. {{E}}σ = n ∧ θ = {x n} ∧ Δ = {(∅, θ)} (σ, Δ) |= E1 (γ,E2) iff ∃σ1, σ2,t, n. σ = σ1 σ2 ∧{{E1}}σ1 =t ∧ {{E2}}σ2 =n ∧ Δ = {({t (γ,n)}, ∅)} (σ, Δ) |= E1 (end, E2) iff ∃σ1, σ2,t, n. σ = σ1 σ2 ∧{{E1}}σ1 =t ∧ {{E2}}σ2 =n ∧ Δ = {({t (end, n)}, ∅)} Σ |= p ∗ q iff ∃Σ1, Σ2. Σ=Σ1 ∗ Σ2 ∧ Σ1 |= p ∧ Σ2 |= q Σ |= p ⊕ q iff ∃Σ1, Σ2. Σ=Σ1 ⊕ Σ2 ∧ Σ1 |= p ∧ Σ2 |= q SpecExact(p) iff ∀Δ,Δ . (( ,Δ) |=p) ∧ (( ,Δ ) |=p) =⇒ (Δ=Δ ) Figure 8. Semantics of State Assertions Definition 3 (Contextual Refinement). Π ϕ Γ iff ∀n, C1,...,Cn, σc, σo, θ. ϕ(σo) = θ =⇒ O[ ([ let Π in C1 ...Cn), (σc, σo) ]] ⊆ O[ ([ with Γ do C1 ...Cn), (σc, θ) ]] . Following Filipovic´ et al. [9], we can prove that linearizability is equivalent to contextual refinement. We give the proofs in TR [18]. Theorem 4 (Equivalence). Π ϕ Γ ⇐⇒ Π ϕ Γ. 4. A Relational Rely-Guarantee Style Logic To prove object linearizability, we first instrument the object imple￾mentation by introducing auxiliary states and auxiliary commands, which relate the concrete code with the abstract object and oper￾ations. Our program logic extends LRG [8] with a relational in￾terpretation of assertions and new rules for auxiliary commands. (Σ, Σ ) |= p q iff Σ |= p ∧ Σ |= q (Σ, Σ ) |= [p] iff Σ |= p ∧ Σ=Σ (Σ, Σ ) |= R1 ∗ R2 iff ∃Σ1, Σ2, Σ 1, Σ 2. (Σ = Σ1 ∗ Σ2) ∧ (Σ = Σ 1 ∗ Σ 2) ∧ (Σ1, Σ 1) |= R1 ∧ (Σ2, Σ 2) |= R2 (Σ, Σ ) |= R1 ⊕ R2 iff ∃Σ1, Σ2, Σ 1, Σ 2. (Σ = Σ1 ⊕ Σ2) ∧ (Σ = Σ 1 ⊕ Σ 2) ∧ (Σ1, Σ 1) |= R1 ∧ (Σ2, Σ 2) |= R2 Id def = [true] True def = true true (∅, n) γ −→ (∅, n ) γ(n)(θ)=(n , θ ) (Δ, n) γ −→ (Δ , n ) ({(U, θ)} Δ, n) γ −→ ({(U, θ )} Δ , n ) [E, p]γ[E , q] iff ∀σ, Δ, n. (σ, Δ) |= (E =n) ∗ p =⇒ ∃Δ , n . (Δ, n) γ −→ (Δ , n ) ∧ ((σ, Δ ) |= (E =n ) ∗ q) I R iff ([I] ⇒ R) ∧ (R ⇒ I I) ∧ Precise(I) Figure 9. Semantics of Actions Although our logic is based on LRG [8], this approach is mostly in￾dependent with the base logic. Similar extensions can also be made over other logics, such as RGSep [32]. Our logic is proposed to verify object methods only. Verified object methods are guaranteed to be a contextual refinement of their abstract atomic operations, which ensures linearizability of the object. We discuss verification of whole programs consisting of both client code and object code at the end of Sec. 4.3. 4.1 Instrumented Code and States In Fig. 7 we show the syntax of the instrumented code and its state model. As explained in Sec. 2, program states Σ for the object method executions now consist of two parts, the physical object states σ and the auxiliary data Δ. Δ is a nonempty set of (U, θ) pairs, each pair representing a speculation of the situation at the abstract level. Here θ is the current abstract object, and U is a pending thread pool recording the remaining operation to be fulfilled by each thread. It maps a thread id to its remaining abstract operation, which is either (γ,n) (the operation γ needs to be executed with argument n) or (end, n) (the operation has been finished with the return value n). We assume Δ is always domain￾exact, defined as follows: DomExact(Δ) def = ∀U, θ, U , θ . (U, θ) ∈ Δ ∧ (U , θ ) ∈ Δ =⇒ dom(U)=dom(U ) ∧ dom(θ)=dom(θ ) . It says, all the speculations in Δ should describe the same set of threads and the same domain of abstract objects. Any Δ containing a single speculation is domain-exact. Also domain-exactness can be preserved under the step of any command in our instrumented language, thus it is reasonable to assume it always holds. Below we informally explain the effects over Δ of the newly introduced commands. We leave their formal semantics to Sec. 4.4. The auxiliary command linself executes the unfinished abstract op￾eration of the current thread in every U in Δ, and changes the ab￾stract object θ correspondingly. lin(E) executes the abstract opera￾tion of the thread with id E. linself or lin(E) is executed when we know for sure that a step is the linearization point. The trylinself command introduces uncertainty. Since we do not know if the ab￾stract operation of the current thread is fulfilled or not at the cur￾rent point, we consider both possibilities. For each (U, θ) pair in Δ that contains unfinished abstract operation of the current thread, we add in Δ a new speculation (U , θ ) where the abstract operation is done and θ is the resulting abstract object. Since the original (U, θ) is also kept, we have both speculations in Δ. Similarly, the 464