Characterizing Progress Properties via Contextual Refinements 235 We use ITA D(Sa,T)to mean that T'is a legal sequential history generated by any client using the specification I7 with an abstract initial state sa Definition 2 (Linearizability of Objects).The object's implementation IT is linearizable u.r.t.ⅡA under a refinement mapping p,denoted byⅡ≤eⅡA,if Vn,C1,...,Cn,S,Sa,T.TE HI(let I in Cill...IICn),S]A ((S)=Sa) =→3Tc,T'.Te∈completions(T)AⅡA>(Sa,T)A Te Zin T'. Here the partial mapping p:State-State relates concrete states to abstract ones. The side condition (S)=Sa in the above definition requires the initial concrete state S to be well-formed in that it represents a valid abstract state Sa.For instance,may need S to contain a linked list and relate it to an abstract mathematical set in Sa for a set object.Besides,o should always require the client states in S and Sa to be identical. Next we define a contextual refinement between the concrete object and its specification,which is equivalent to linearizability. Definition 3 (Basic Contextual Refinement).II IA iff Vn,C1,...,Cn,S,Sa.((S)=Sa) =→OI(letⅡinCl..‖Cn),S]cOI(letⅡin Cll..lCn),Sal Remember that OW,S]represents the prefix-closed set of observable event traces generated during the executions of(W,S),which is defined in Figure 5. Following Filipovic et al.[4],we can prove that linearizability is equivalent to this contextual refinement.We give the proofs in the TR [14]. Theorem4(Basic Equivalence).Ⅱ≤eⅡA→ⅡSeⅡA: Theorem 4 allows us to use I IA to identify linearizable objects.However, we cannot use it to characterize progress properties of objects.For the following example,ITEIA holds although no concrete method call of f could finish(we assume this object contains a method f only). Ⅱ(f):hile(true)skip;ⅡA(f):skip; C:print(1);f();print(1); The reason is that II ITA considers a prefir-closed set of event traces at the abstract side.For the above client C,the observable behaviors of let I7 in C can all be found in the prefix-closed set of behaviors produced by let IA in C. 4 Formalizing Progress Properties We define progress in Figure 6 as properties over both event traces T and object implementations I7.We say an object implementation II has a progress property P iff all its event traces have the property.Here we use T to generate the event traces.Its definition in Figure 6 is similar to TIW,S]of Figure 5,but TlW,S] is for the set of finite or infinite event traces produced by complete executions. We use (W,S).to denote the existence of a T-labelled infinite execution. (W,S)T(skip,)represents a terminating execution that produces T.By using W,we append end at the end of each thread to explicitly mark theCharacterizing Progress Properties via Contextual Refinements 235 We use ΠA (Sa, T ) to mean that T is a legal sequential history generated by any client using the specification ΠA with an abstract initial state Sa. Definition 2 (Linearizability of Objects). The object’s implementation Π is linearizable w.r.t. ΠA under a refinement mapping ϕ, denoted by Π ϕ ΠA, iff ∀n, C1,...,Cn, S, Sa,T. T ∈ H(let Π in C1 ...Cn), S ∧ (ϕ(S) = Sa) =⇒ ∃Tc, T . Tc ∈ completions(T ) ∧ ΠA (Sa, T ) ∧ Tc lin T . Here the partial mapping ϕ:StateState relates concrete states to abstract ones. The side condition ϕ(S) = Sa in the above definition requires the initial concrete state S to be well-formed in that it represents a valid abstract state Sa. For instance, ϕ may need S to contain a linked list and relate it to an abstract mathematical set in Sa for a set object. Besides, ϕ should always require the client states in S and Sa to be identical. Next we define a contextual refinement between the concrete object and its specification, which is equivalent to linearizability. Definition 3 (Basic Contextual Refinement). Π ϕ ΠA iff ∀n, C1,...,Cn, S, Sa. (ϕ(S) = Sa) =⇒ O(let Π in C1 ...Cn), S ⊆ O(let ΠA in C1 ...Cn), Sa . Remember that OW, S represents the prefix-closed set of observable event traces generated during the executions of (W, S), which is defined in Figure 5. Following Filipovi´c et al. [4], we can prove that linearizability is equivalent to this contextual refinement. We give the proofs in the TR [14]. Theorem 4 (Basic Equivalence). Π ϕ ΠA ⇐⇒ Π ϕ ΠA. Theorem 4 allows us to use Π ϕ ΠA to identify linearizable objects. However, we cannot use it to characterize progress properties of objects. For the following example, Π ϕ ΠA holds although no concrete method call of f could finish (we assume this object contains a method f only). Π(f) : while(true) skip; ΠA(f) : skip; C : print(1); f(); print(1); The reason is that Π ϕ ΠA considers a prefix-closed set of event traces at the abstract side. For the above client C, the observable behaviors of let Π in C can all be found in the prefix-closed set of behaviors produced by let ΠA in C. 4 Formalizing Progress Properties We define progress in Figure 6 as properties over both event traces T and object implementations Π. We say an object implementation Π has a progress property P iff all its event traces have the property. Here we use Tω to generate the event traces. Its definition in Figure 6 is similar to T W, S of Figure 5, but TωW, S is for the set of finite or infinite event traces produced by complete executions. We use (W, S) T −→ω · to denote the existence of a T -labelled infinite execution. (W, S) T −→ ∗ (skip, ) represents a terminating execution that produces T . By using W , we append end at the end of each thread to explicitly mark the