Characterizing Progress Properties via Contextual Refinements 237 div-tids(T)(t(I(T)=)} O.IW,S](get_obsv(T)I TETIW,S]} OaIw,S】些{get.obsv(T)|T∈Tlw,S]Aiso(T)} OIW,S]{getobsv(T)I TET.IW,S]Afair(T)} OIW,S]{(get_obsv(T),divtids(T))I TTIW,S]} OnIW,]{(get-obsv(T),div-tids(T))TTIW,S]Afair(T)} Fig.8.Generation of Complete Event Traces (t1,fi,1):(t2,f2,n2):(t1,obj)(t3,clt)(t3,clt):(t3,clt). If T is infinite,fair(T)requires every non-terminating thread be scheduled in- finitely often;and iso(T)requires eventually only one thread be scheduled.We can see that a fair schedule is a good schedule satisfying sched. At the bottom of Figure 6 we define the progress properties formally.We omit the parameter T in the formulae to simplify the presentation.An event trace T is wait-free(i.e.,wait-free(T)holds)if under the good schedule sched,it guarantees prog-t unless it ends with a fault.lock-free(T)is similar except that it guarantees prog-s.Starvation-freedom and deadlock-freedom guarantee prog-t and prog-s under fair scheduling.Obstruction-freedom guarantees prog-t if some pending thread is always scheduled(sched)and runs in isolation (iso). Figure 7 contains lemmas that relate progress properties.For instance,an event trace is starvation-free,iff it is wait-free or not fair.These lemmas give us the relationship lattice in Figure 1.To close the lattice,we also define a progress property in the sequential setting.Sequential termination guarantees that every method call must finish in a trace produced by a sequential client.The formal definition is given in the companion TR 14,and we prove that it is implied by each of the five progress properties for concurrent objects. 5 Equivalence to Contextual Refinements We extend the basic contextual refinement in Definition 3 to observe progress as well as linearizability.For each progress property,we carefully choose the observable behaviors at the concrete and the abstract levels. 5.1 Observable Behaviors In Figure 8,we define various observable behaviors for the termination-sensitive contextual refinements. We use IW,S]to represent the set of observable event traces produced by complete executions of (W,S).Recall that get_obsv(T)gets the sub-trace of T consisting of all the observable events only.Unlike the prefix-closed set OW,S],this definition utilizes TW,S(see Figure 6)whose event traces are all complete and could be infinite.Thus it allows us to observe divergence of theCharacterizing Progress Properties via Contextual Refinements 237 div tids(T ) def = {t | (|(T |t)| = ω ) } OωW, S def = {get obsv(T ) | T ∈ TωW, S } OiωW, S def = {get obsv(T ) | T ∈ TωW, S ∧ iso(T )} OfωW, S def = {get obsv(T ) | T ∈ TωW, S ∧ fair(T )} OtωW, S def = {(get obsv(T ), div tids(T )) | T ∈ TωW, S } OftωW, S def = {(get obsv(T ), div tids(T )) | T ∈ TωW, S ∧ fair(T )} Fig. 8. Generation of Complete Event Traces (t1, f1, n1):: (t2, f2, n2):: (t1, obj):: (t3, clt):: (t3, clt):: (t3, clt)::... If T is infinite, fair(T ) requires every non-terminating thread be scheduled in- finitely often; and iso(T ) requires eventually only one thread be scheduled. We can see that a fair schedule is a good schedule satisfying sched. At the bottom of Figure 6 we define the progress properties formally. We omit the parameter T in the formulae to simplify the presentation. An event trace T is wait-free (i.e., wait-free(T ) holds) if under the good schedule sched, it guarantees prog-t unless it ends with a fault. lock-free(T ) is similar except that it guarantees prog-s. Starvation-freedom and deadlock-freedom guarantee prog-t and prog-s under fair scheduling. Obstruction-freedom guarantees prog-t if some pending thread is always scheduled (sched) and runs in isolation (iso). Figure 7 contains lemmas that relate progress properties. For instance, an event trace is starvation-free, iff it is wait-free or not fair. These lemmas give us the relationship lattice in Figure 1. To close the lattice, we also define a progress property in the sequential setting. Sequential termination guarantees that every method call must finish in a trace produced by a sequential client. The formal definition is given in the companion TR [14], and we prove that it is implied by each of the five progress properties for concurrent objects. 5 Equivalence to Contextual Refinements We extend the basic contextual refinement in Definition 3 to observe progress as well as linearizability. For each progress property, we carefully choose the observable behaviors at the concrete and the abstract levels. 5.1 Observable Behaviors In Figure 8, we define various observable behaviors for the termination-sensitive contextual refinements. We use OωW, S to represent the set of observable event traces produced by complete executions of (W, S). Recall that get obsv(T ) gets the sub-trace of T consisting of all the observable events only. Unlike the prefix-closed set OW, S, this definition utilizes TωW, S (see Figure 6) whose event traces are all complete and could be infinite. Thus it allows us to observe divergence of the