Rules in the bottom half show how to do rely-guarantee style (C;o)(C,') C≠E[return-] concurrency reasoning,which are very similar to those in LRG [8] As in LRG,we use a precise invariant I to specify the boundary (C,(a,△)-→：(C,(a',△) of the well-formed shared resource.The ATOM rule says we could U.(W,)e△→U(t)=(end,[E].) reason sequentially about code in the atomic block.Then we can lift it to the concurrent setting as long as its effects over the shared (E[return E],(o,△)）-→t(skip,(a,△)》 resource satisfy the guarantee G.which is fenced by the invariant I. △：△ In this step we assume the environment does not update shared re- source,thus using ld as the rely condition (see Fig.9).To allow (E[linself],(a,△)-→t(E[skip],(a,△)》 general environment behaviors,we should apply the ATOM-R rule IEl。=t△→x△y later,which requires that R be fenced by I and the pre-and post- conditions be stable with respect to R.Here Sta(p,),R)re- (E(trylin(E)l,(a,△)-→t(E[skip],(a,△U△)》 quires that p and g be stable with respect to R,a standard require- SpecExact(p) ment in rely-guarantee reasoning.More rules are shown in TR [18). (a,△lp=(,△) (E[commit(p)l,(a,△)→t(E[skip],(a,△) Linking with client program verification.Our relational logic is introduced for object verification,but it can also be used to verify (C,)→：(C,) (E,)=R client code,since it is just an extension over the general-purpose (C,)(@,y) (C,)R(C,y) concurrent logic LRG (which includes the rule for parallel com- position).Moreover,as we will see in Sec.5,our logic ensures Auxiliary Definitions: contextual refinement.Therefore,to verify a program W,we could replace the object implementation with the abstract operations and U(t)=(Y,n) y(n)()=(n',8) U(t)=(end,n) verify the corresponding abstract program W instead.Since W ab- (U,a)--t(U{t(end,n)},0) (U,0)-t(U,9) stracts away concrete object representation and method implemen- tation details,this approach provides us with"separation and in- (U,8)--t(U',0)） △→t△ formation hiding"[26]over the object,but still keeps enough in- 010 {(0,)}出△→：{(U',8)}U△ formation (i.e.,the abstract operations)about the method calls in (a,△)lp=(a',△)if concurrent client verification. ,△"，△p-(a=a'uaA(△=△'u△"A(a',△p)=p) 4.4 Semantics and Partial Correctness A(△'ldm(△p)=△p)A(△"ldm(△p)n△p=0) We first show some key operational semantics rules for the instru- lD((U,0)I dom({(U,0)))=DA3U,0'.(UWU',W')EA} mented code in Fig.11. dom(△)g(dom(U),dom(e)where(U,a)∈△ A single step execution of the instrumented code by thread t is represented as (C,)(C,').When we reach the Figure 11.Operational Semantics in the Relational State Model return E command (the second rule),we require that there be no uncertainty about thread t at the abstract level in A.That is,in every speculation in A,we always know t's operation has been finished conditions.We could prove the logic ensures partial correctness by with the same return value E.Meanings of the auxiliary commands showing R.G.I Ft ipCfg implies R.G,I Et ipCigt.The have been explained before.Here we use the auxiliary definition details are shown in TR [18].In the next section,we give a stronger △→t△'to formally define their transitions over△.The semantics soundness of the logic,i.e.soundness w.rt.linearizability of commit(p)requires p to be speculation-exact (see Fig.8).Also it uses (A)p=(',A')to filter out the wrong speculations.To 5. Soundness via Simulation ensure locality,this filter allows A to contain some extra resource Our logic intuitively relates the concrete object code with its ab- such as the threads and their abstract operations other than those stract level specification.In this section we formalize the intuition described in p.For example,the following A describes two threads and prove that the logic indeed ensures object linearizability.The t and t2,but we could mention only ti in commit(p). proof is constructed in the following steps.We propose a new rely- 了t1Y1,n1) t1(end,n guarantee-based forward-backward simulation between the con- △： t22,n2t2end,n」 crete code and the abstract operation.We prove the simulation is compositional and implies contextual refinement between the two If p is t(,n),then commit(p)will keep only the left sides,and our logic indeed establishes such a simulation.Thus the speculation and discard the other.p can also be t(,n) t(end,n),then commit(p)will keep both speculations. logic establishes contextual refinement.Finally we get linearizabil- ity following Theorem 4. Given the thread-local semantics,we could next define the tran- Below we first define a rely-guarantee-based forward-backward sition ((C),which describes the behavior of thread simulation.It extends RGSim [19]with the support of the helping t with interference R from the environment. mechanism and speculations. Semantics preservation by the instrumentation.It is easy to see Definition 5(Simulation for Method).(,C)GYiff that the newly introduced auxiliary commands do not change the physical state o,nor do they affect the program control flow.Thus n,o,△.(o,△)卢(t一(，n)*(x=n)*p) the instrumentation does not change program behaviors,unless the =→(C:noret,o)≤r:Gp△. auxiliary commands are inserted into the wrong places and they get Whenever(C,a):G:A.we have the following: stuck,but this can be prevented by our program logic. 1.if C E return.,then Soundness w.r.t.partial correctness.Following LRG [8],we (a)for any C'and a',if (C,)(C',). could give semantics of the logic judgment as R,G,Ip)Cfg) then there exists△'such that△三△'， which encodes partial correctness of C w.rt.the pre-and post- (a,△)，(a',△)=(G*True)and(C',o)h:Gp△ 466Rules in the bottom half show how to do rely-guarantee style concurrency reasoning, which are very similar to those in LRG [8]. As in LRG, we use a precise invariant I to specify the boundary of the well-formed shared resource. The ATOM rule says we could reason sequentially about code in the atomic block. Then we can lift it to the concurrent setting as long as its effects over the shared resource satisfy the guarantee G, which is fenced by the invariant I. In this step we assume the environment does not update shared re￾source, thus using Id as the rely condition (see Fig. 9). To allow general environment behaviors, we should apply the ATOM-R rule later, which requires that R be fenced by I and the pre- and post￾conditions be stable with respect to R. Here Sta({p, q}, R) re￾quires that p and q be stable with respect to R, a standard require￾ment in rely-guarantee reasoning. More rules are shown in TR [18]. Linking with client program verification. Our relational logic is introduced for object verification, but it can also be used to verify client code, since it is just an extension over the general-purpose concurrent logic LRG (which includes the rule for parallel com￾position). Moreover, as we will see in Sec. 5, our logic ensures contextual refinement. Therefore, to verify a program W, we could replace the object implementation with the abstract operations and verify the corresponding abstract program W instead. Since W ab￾stracts away concrete object representation and method implemen￾tation details, this approach provides us with “separation and in￾formation hiding” [26] over the object, but still keeps enough in￾formation (i.e., the abstract operations) about the method calls in concurrent client verification. 4.4 Semantics and Partial Correctness We first show some key operational semantics rules for the instru￾mented code in Fig. 11. A single step execution of the instrumented code by thread t is represented as (C, Σ) −→ t (C , Σ ). When we reach the return E command (the second rule), we require that there be no uncertainty about thread t at the abstract level in Δ. That is, in every speculation in Δ, we always know t’s operation has been finished with the same return value E. Meanings of the auxiliary commands have been explained before. Here we use the auxiliary definition Δ →t Δ to formally define their transitions over Δ. The semantics of commit(p) requires p to be speculation-exact (see Fig. 8). Also it uses (σ, Δ)|p = (σ , Δ ) to filter out the wrong speculations. To ensure locality, this filter allows Δ to contain some extra resource such as the threads and their abstract operations other than those described in p. For example, the following Δ describes two threads t1 and t2, but we could mention only t1 in commit(p). Δ : t1 (γ1, n1) t2 (γ2, n2) , t1 (end, n 1) t2 (end, n 2)  If p is t1 (γ1, n1), then commit(p) will keep only the left speculation and discard the other. p can also be t1 (γ1, n1) ⊕ t1 (end, n 1), then commit(p) will keep both speculations. Given the thread-local semantics, we could next define the tran￾sition (C, Σ) R −→t (C, Σ), which describes the behavior of thread t with interference R from the environment. Semantics preservation by the instrumentation. It is easy to see that the newly introduced auxiliary commands do not change the physical state σ, nor do they affect the program control flow. Thus the instrumentation does not change program behaviors, unless the auxiliary commands are inserted into the wrong places and they get stuck, but this can be prevented by our program logic. Soundness w.r.t. partial correctness. Following LRG [8], we could give semantics of the logic judgment as R, G, I |=t {p}C{q}, which encodes partial correctness of C w.r.t. the pre- and post- (C, σ) −t (C , σ ) C = E[ return ] (C, (σ, Δ)) −→t (C , (σ , Δ)) ∀U. (U, )∈Δ =⇒ U(t)=(end, Eσ) (E[ return E ], (σ, Δ)) −→t (skip, (σ, Δ)) Δ →t Δ (E[ linself ], (σ, Δ)) −→t (E[skip ], (σ, Δ )) Eσ = t Δ →t Δ (E[ trylin(E) ], (σ, Δ)) −→t (E[skip ], (σ, Δ∪Δ )) SpecExact(p) (σ, Δ)|p = ( , Δ ) (E[ commit(p) ], (σ, Δ)) −→t (E[skip ], (σ, Δ )) (C, Σ) −→t (C , Σ ) (C, Σ) R −→t (C , Σ ) (Σ, Σ ) |= R (C, Σ) R −→t (C, Σ ) Auxiliary Definitions: U(t)=(γ,n) γ(n)(θ)=(n , θ ) (U, θ) t (U{t (end, n )}, θ ) U(t)=(end, n) (U, θ) t (U, θ) ∅ →t ∅ (U, θ) t (U , θ ) Δ →t Δ {(U, θ)} Δ →t {(U , θ )} ∪ Δ (σ, Δ)|p = (σ , Δ ) iff ∃σ,Δ,Δp. (σ = σ σ) ∧ (Δ = Δ Δ) ∧ ((σ ,Δp) |= p) ∧ (Δ |dom(Δp) = Δp) ∧ (Δ|dom(Δp) ∩ Δp = ∅) Δ|D def = {(U,θ) | dom({(U,θ)})=D∧ ∃U ,θ . (U U , θ θ )∈Δ} dom(Δ) def = (dom(U), dom(θ)) where (U, θ) ∈ Δ Figure 11. Operational Semantics in the Relational State Model conditions. We could prove the logic ensures partial correctness by showing R, G, I t {p}C{q} implies R, G, I |=t {p}C{q}. The details are shown in TR [18]. In the next section, we give a stronger soundness of the logic, i.e. soundness w.r.t. linearizability. 5. Soundness via Simulation Our logic intuitively relates the concrete object code with its ab￾stract level specification. In this section we formalize the intuition and prove that the logic indeed ensures object linearizability. The proof is constructed in the following steps. We propose a new rely￾guarantee-based forward-backward simulation between the con￾crete code and the abstract operation. We prove the simulation is compositional and implies contextual refinement between the two sides, and our logic indeed establishes such a simulation. Thus the logic establishes contextual refinement. Finally we get linearizabil￾ity following Theorem 4. Below we first define a rely-guarantee-based forward-backward simulation. It extends RGSim [19] with the support of the helping mechanism and speculations. Definition 5 (Simulation for Method). (x, C) t R;G;p γ iff ∀n, σ, Δ. (σ, Δ) |= (t (γ,n) ∗ (x = n) ∗ p) =⇒ (C; noret, σ) t R;G;p Δ . Whenever (C, σ) t R;G;p Δ, we have the following: 1. if C = E[ return ], then (a) for any C and σ , if (C, σ) −t (C , σ ), then there exists Δ such that Δ ⇒ Δ , ((σ, Δ),(σ , Δ )) |= (G ∗ True) and (C , σ ) t R;G;p Δ ; 466