236 H.Liang et al. Definition.An object I7 satisfies P under a refinement mapping P(IT),iff n,Ci.,Cn,S,T.T∈TI(letⅡinCl.llCn),S]A(S∈dom(p)=→P(T). T.IW,S]{(spawn,IW):T (（w,s)“.V(w],S)工*(skip,-)V(wJ,S)T*abort} Llet II in Cill...Cn let II in (Ci;end)ll...l(Cn;end) llet II in Ci ll...Il C n tnum((spawn,n)::T)n pend_inv(T)eli.e=T(i)A is_inv(e)A3j.(j>imatch(e,T(j)))} prog-t(T)iff Vi,e.eE pend_jnv(T(1..i))=j.j>iA match(e,T(j)) prog-s(T)i证i,e.e∈pend_inv(T(1.i)=→3j.j>iAis-ret(T)】 abt(T)iff 3i.is_abt(T(i)) sched(T)证lTl=w A pend_inv(T)≠0=→3e.e∈pend_inv(T)AI(Tltid())川=w fair(T)i证lT|=w=→t∈[1.tnum(T)小.l(Tl)川=w V last(Tl)=(t,term) iso(T)iff T=w=→3t,i.(付i.j≥i=→tid(T)=t) wait-free iff sched prog-t V abt starvation-free iff fair=prog-t V abt lock-free iff sched prog-s V abt deadlock-free iff fair prog-s V abt obstruction-free iff sched A iso=prog-t V abt Fig.6.Formalizing Progress Properties lock-free wait-free V prog-s starvation-free←→wait-free V-fair obstruction-free←→lock-free V-iso deadlock-free lock-free V-fair Fig.7.Relationships between Progress Properties termination of the thread.We also insert the spawning event(spawn,n)at the beginning of T,where n is the number of threads in W.Then we can use tnum(T) to get the number n,which is needed to define fairness,as shown below. Before formulating each progress property over event traces,we first define some auxiliary properties in Figure 6.prog-t(T)guarantees that every method call in T eventually finishes.prog-s(T)guarantees that some pending method call finishes.Different from prog-t,the return event T(j)in prog-s does not have to be a matching return of the pending invocation e.abt(T)says that T ends with a fault event. There are three useful conditions on scheduling.The basic requirement for a good schedule is sched.If T is infinite and there exist pending calls,then at least one pending thread should be scheduled infinitely often.In fact,there are two possible reasons causing a method call of thread t to pend.Either t is no longer scheduled,or it is always scheduled but the method call never finishes.sched rules out the bad schedule where no thread with an invoked method is active. For instance,the following infinite trace does not satisfy sched.236 H. Liang et al. Definition. An object Π satisfies P under a refinement mapping ϕ, Pϕ(Π), iff ∀n, C1,. . . ,Cn, S,T. T ∈ Tω(let Π in C1...Cn), S ∧ (S ∈dom(ϕ)) =⇒ P(T ). TωW, S def = {(spawn, |W|)::T | (W, S) T −→ω · ∨ (W, S) T −→∗(skip, ) ∨ (W, S) T −→∗abort} let Π in C1 ...Cn def = let Π in (C1; end)...(Cn; end) |let Π in C1 ... Cn| def = n tnum((spawn, n)::T ) def = n pend inv(T ) def = {e | ∃i. e=T (i) ∧ is inv(e) ∧ ¬∃j. (j>i ∧ match(e, T (j)))} prog-t(T ) iff ∀i, e. e ∈ pend inv(T (1..i)) =⇒ ∃j. j > i ∧ match(e, T (j)) prog-s(T ) iff ∀i, e. e ∈ pend inv(T (1..i)) =⇒ ∃j. j > i ∧ is ret(T (j)) abt(T ) iff ∃i. is abt(T (i)) sched(T ) iff |T | = ω ∧ pend inv(T ) = ∅ =⇒ ∃e. e ∈ pend inv(T ) ∧ |(T |tid(e))| = ω fair(T ) iff |T | = ω =⇒ ∀t ∈ [1..tnum(T )]. |(T |t)| = ω ∨ last(T |t)=(t, term) iso(T ) iff |T | = ω =⇒ ∃t, i. (∀j. j ≥ i =⇒ tid(T (j)) = t) wait-free iff sched =⇒ prog-t ∨ abt starvation-free iff fair =⇒ prog-t ∨ abt lock-free iff sched =⇒ prog-s ∨ abt deadlock-free iff fair =⇒ prog-s ∨ abt obstruction-free iff sched ∧ iso =⇒ prog-t ∨ abt Fig. 6. Formalizing Progress Properties lock-free ⇐⇒ wait-free ∨ prog-s starvation-free ⇐⇒ wait-free ∨ ¬fair obstruction-free ⇐⇒ lock-free ∨ ¬iso deadlock-free ⇐⇒ lock-free ∨ ¬fair Fig. 7. Relationships between Progress Properties termination of the thread. We also insert the spawning event (spawn, n) at the beginning of T , where n is the number of threads in W. Then we can use tnum(T ) to get the number n, which is needed to define fairness, as shown below. Before formulating each progress property over event traces, we first define some auxiliary properties in Figure 6. prog-t(T ) guarantees that every method call in T eventually finishes. prog-s(T ) guarantees that some pending method call finishes. Different from prog-t, the return event T (j) in prog-s does not have to be a matching return of the pending invocation e. abt(T ) says that T ends with a fault event. There are three useful conditions on scheduling. The basic requirement for a good schedule is sched. If T is infinite and there exist pending calls, then at least one pending thread should be scheduled infinitely often. In fact, there are two possible reasons causing a method call of thread t to pend. Either t is no longer scheduled, or it is always scheduled but the method call never finishes. sched rules out the bad schedule where no thread with an invoked method is active. For instance, the following infinite trace does not satisfy sched.