Progress of Concurrent Objects with Partial Methods（Extended Version）

Progress of Concurrent Objects with Partial Methods(Extended Version) :11 (C,(oe,o,K(d)二in(C,(a6,ax'》 K'=Kik'】 btids(let II in Cll...C..ICn.(..K))=(Ac.A) (det i))(let i) C=skip K(i)=o C=end e=(i.term) btids(let II in cill...Ci...llCn.(co,K))=(Ac.Ao) (et I im cn(e)det Iin C oK) (Ci.(ac.co.K(i)))-i.nabort (let ninn.(c))abort (a)program transitions II(f)=(P,y.C)oEP [E]se=n x E dom(sc)K=(y~n).x,E[skip]) [x=f(se,h.o,》fm n(C,(c,he)oo,k》 f生dom()oroo生Πf).Por[Else undefined or x生dom(sc） E(x=fg1.(e,he,o.ol》L.cabort四 t.n abort k=(s1.x.C)[E]s =n se=sexn (E[return E](she))r) n(C,(sk,he),oo,o》 K=(s1.x.C)[E]s:undefined (E[return E].((sc,hc).o.K))- (t,obj.abort) tn abort [E]se =n (EI print(E)]((.h) (E[skip ].((se.he).)) (C,(sous,ho)t(C',(s%世s,h%)》 dom(s1)=dom(sf) (C.ac)-(C,ac) (C,(oe,(5o,hox,C》ob n(C%,(cc,(6,h。),(sxC》 (C,(ce,oo,)c →tn(C,(o2,oo,o》 (C,(so sI,ho))-tabort (C,oc)-tabort (C,(oe,(so,ho).(s1.x.C))) (任obj.abort) t.n abort (C,(ac,oo,o)) (t.clt,abort) tn abort (b)thread transitions [B]s true (C,(s,h))(skip.(s',h')) [B]s true (C,(s,h))abort (E[await(B)(C)].(s,h))-t(E[skip ].(s',h')) (E[await(B)(C)].(s,h))-t abort (c)local thread transitions Fig.4.Selected operational semantics rules. respectively.The output event(t,out,n)is generated by the print(E)command.(t,term)records the termination of the thread t.We also introduce a special event(spawn,n),which is inserted at the beginning of each event trace to record the creation of n threads at the beginning of the whole Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :11 (Cˆ i , (σc ,σo ,K (i))) e −→i,Π (Cˆ′ i , (σ ′ c ,σ ′ o ,κ ′ ))) K ′ = K {i ❀ κ ′ } btids(let Π in Cˆ 1 ∥ . . .Cˆ′ i . . . ∥Cˆ n, (σ ′ c ,σ ′ o ,K ′ )) = (∆c ,∆o ) (let Π in Cˆ 1 ∥ . . .Cˆ i . . . ∥Cˆ n, (σc ,σo ,K )) p (e,∆c ,∆o ) −−−−−−−−→ (let Π in Cˆ 1 ∥ . . .Cˆ′ i . . . ∥Cˆ n, (σ ′ c ,σ ′ o ,K ′ )) Cˆ i = skip K (i) = ◦ Cˆ′ i = end e = (i,term) btids(let Π in Cˆ 1 ∥ . . .Cˆ i . . . ∥Cˆ n, (σc ,σo ,K )) = (∆c ,∆o ) (let Π in Cˆ 1 ∥ . . .Cˆ i . . . ∥Cˆ n, (σc ,σo ,K )) p (e,∆c ,∆o ) −−−−−−−−→ (let Π in Cˆ 1 ∥ . . .Cˆ′ i . . . ∥Cˆ n, (σc ,σo ,K )) (Cˆ i , (σc ,σo ,K (i))) e −→i,Π abort (let Π in Cˆ 1 ∥ . . .Cˆ i . . . ∥Cˆ n, (σc ,σo ,K )) p (e,∅,∅) −−−−−−→ abort (a) program transitions Π(f ) = (P,y,C) σo ∈ P JEKsc = n x ∈ dom(sc ) κ = ({y ❀ n},x,E[ skip ]) (E[ x := f (E) ], ((sc ,hc ),σo ,◦)) (t,f ,n) −−−−−−→t,Π (C, ((sc ,hc ),σo ,κ)) f < dom(Π) or σo < Π(f ).P or JEKsc undefined or x < dom(sc ) (E[ x := f (E) ], ((sc ,hc ),σo ,◦)) (t,clt,abort) −−−−−−−−−−→t,Π abort κ = (sl ,x,C) JEKsl = n s′ c = sc {x ❀ n} (E[ return E ], ((sc ,hc ),σo ,κ)) (t,ret,n) −−−−−−−→t,Π (C, ((s ′ c ,hc ),σo ,◦)) κ = (sl ,x,C) JEKsl undefined (E[ return E ], ((sc ,hc ),σo ,κ)) (t,obj,abort) −−−−−−−−−−−→t,Π abort JEKsc = n (E[ print(E) ], ((sc ,hc ),σo ,◦)) (t,out,n) −−−−−−−→t,Π (E[ skip ], ((sc ,hc ),σo ,◦)) (C, (so ⊎ sl ,ho )) −_t (C ′ , (s ′ o ⊎ s ′ l ,h ′ o )) dom(sl ) = dom(s ′ l ) (C, (σc , (so ,ho ), (sl ,x,C1))) (t,obj) −−−−−→t,Π (C ′ , (σc , (s ′ o ,h ′ o ), (s ′ l ,x,C1))) (C,σc ) −_t (C ′ ,σ ′ c ) (C, (σc ,σo ,◦)) (t,clt) −−−−−→t,Π (C ′ , (σ ′ c ,σo ,◦)) (C, (so ⊎ sl ,ho )) −_t abort (C, (σc , (so ,ho ), (sl ,x,C1))) (t,obj,abort) −−−−−−−−−−−→t,Π abort (C,σc ) −_t abort (C, (σc ,σo ,◦)) (t,clt,abort) −−−−−−−−−−→t,Π abort (b) thread transitions JBKs = true (C, (s,h)) −_∗ t (skip, (s ′ ,h ′ )) (E[ await(B){C} ], (s,h))−_t (E[ skip ], (s ′ ,h ′ )) JBKs = true (C, (s,h)) −_∗ t abort (E[ await(B){C} ], (s,h))−_t abort (c) local thread transitions Fig. 4. Selected operational semantics rules. respectively. The output event (t,out,n) is generated by the print(E) command. (t,term) records the termination of the thread t. We also introduce a special event (spawn,n), which is inserted at the beginning of each event trace to record the creation of n threads at the beginning of the whole , Vol. 1, No. 1, Article . Publication date: January 2018

:12 Hongjin Liang and Xinyu Feng program execution.Its use is shown in Sec.5.An event trace E is a(possibly infinite)sequence of events,and a program trace T is a(possibly infinite)sequence of labels t. The sets Ac and Ao in the label record the IDs of threads that are blocked in the client code and object methods respectively.They are generated by the function btids defined in Fig.3.Recall that a thread t is executing the client code if its call stack is empty,i.e.K(t)=o.We also define en(C) as the enabling condition for C,which ensures that C can execute at least one step unless it has terminated.Here the execution context E defines the position of the command to be executed next. The second rule in Fig.4(a)shows that end is used as a flag marking the termination of a thread. A termination event (t,term)is generated correspondingly. The first two rules in Fig.4(b)show that method calls can only be executed in the client code (i.e.,when the stack k is empty),and it is the clients'responsibility to ensure that the precondition P(defined in Fig.3)of the method holds over the object data.If P does not hold,the method invocation step aborts.Similarly,as shown in the subsequent rules,the return command can only be executed in the object method,and the print command can only be in the client code.Other commands can be executed either in the client or in the object,and the transitions are made over oc and oo respectively.In Fig.4(c)we show the operational semantics for await(B)(C).Note that there is no transition rule when B is false,which means that the thread is blocked.Transition rules of other commands are standard and omitted here. More discussions about partial methods.There are actually two reasons that make a method partial.The first is due to non-termination when the method is called under certain conditions.The second is due to abnormal termination,i.e.,the method aborts or terminates with incorrect states or return values.Since the goal of this work is to study progress,the paper focuses on the first kind of partial methods.In our language,we specify the two kinds of partial methods differently.For the first kind,we use the enabling condition B in await(B)(C)to specify when the method should not be blocked.For the second kind,we use the annotated precondition P to specify the condition needed for the method to execute safely and to generate correct results.For instance,although the lock's release method L_REL in specification(2.3)always terminates,it needs an annotated precondition l=cid to prevent client threads not owning the lock from releasing it. 4 LINEARIZABILITY AND BASIC CONTEXTUAL REFINEMENT In this section we formally define linearizability [Herlihy and Wing 1990]of an object II with respect to its abstract specification I.As explained in Sec.2.2,I is an atomic partial specification for II.It has the same syntax with II(see Fig.2),but each method body in I is always an await block await(B)(C)(followed by a return E command).We also assume that the methods in I are safe, i.e.,they never abort. History events,externally observable events,and traces.We call (t,f,n),(t,ret,n)and (t,obj,abort) history events,and (t,out,n),(t,obj,abort)and (t,clt,abort)externally observable events.In Fig.5 we define TW,S]as the prefix closed set of finite traces T generated during the execution of (W,S).HW,S]contains the set of histories projected from traces in TW,S].Here get_hist(T) returns a subsequence consisting of the history events projected from the corresponding labels in T.Similarly OW,S]contains the set of externally observable event traces projected from traces in TW,S],where get_obsv(T)is a subsequence consisting of externally observable events only. As defined below,an event trace E is linearizable with respect to &'i.e.,<lin &'if they have the same sub-trace when projected over individual threads(projection represented as El),and E is a permutation of &but preserves the order of non-overlapping method calls in E'.Here we use is_inv(e)(or is_ret(ez))to represent that e is in the form of (t,f,n)(or(t,ret,n)). Vol.1,No.1,Article.Publication date:January 2018

:12 Hongjin Liang and Xinyu Feng program execution. Its use is shown in Sec. 5. An event trace E is a (possibly infinite) sequence of events, and a program trace T is a (possibly infinite) sequence of labels ι. The sets ∆c and ∆o in the label record the IDs of threads that are blocked in the client code and object methods respectively. They are generated by the function btids defined in Fig. 3. Recall that a thread t is executing the client code if its call stack is empty, i.e., K (t) = ◦. We also define en(Cˆ) as the enabling condition for Cˆ, which ensures that Cˆ can execute at least one step unless it has terminated. Here the execution context E defines the position of the command to be executed next. The second rule in Fig. 4(a) shows that end is used as a flag marking the termination of a thread. A termination event (t,term) is generated correspondingly. The first two rules in Fig. 4(b) show that method calls can only be executed in the client code (i.e., when the stack κ is empty), and it is the clients’ responsibility to ensure that the precondition P (defined in Fig. 3) of the method holds over the object data. If P does not hold, the method invocation step aborts. Similarly, as shown in the subsequent rules, the return command can only be executed in the object method, and the print command can only be in the client code. Other commands can be executed either in the client or in the object, and the transitions are made over σc and σo respectively. In Fig. 4(c) we show the operational semantics for await(B){C}. Note that there is no transition rule when B is false, which means that the thread is blocked. Transition rules of other commands are standard and omitted here. More discussions about partial methods. There are actually two reasons that make a method partial. The first is due to non-termination when the method is called under certain conditions. The second is due to abnormal termination, i.e., the method aborts or terminates with incorrect states or return values. Since the goal of this work is to study progress, the paper focuses on the first kind of partial methods. In our language, we specify the two kinds of partial methods differently. For the first kind, we use the enabling condition B in await(B){C} to specify when the method should not be blocked. For the second kind, we use the annotated precondition P to specify the condition needed for the method to execute safely and to generate correct results. For instance, although the lock’s release method L_REL in specification (2.3) always terminates, it needs an annotated precondition l=cid to prevent client threads not owning the lock from releasing it. 4 LINEARIZABILITY AND BASIC CONTEXTUAL REFINEMENT In this section we formally define linearizability [Herlihy and Wing 1990] of an object Π with respect to its abstract specification Γ. As explained in Sec. 2.2, Γ is an atomic partial specification for Π. It has the same syntax with Π (see Fig. 2), but each method body in Γ is always an await block await(B){C} (followed by a return E command). We also assume that the methods in Γ are safe, i.e., they never abort. History events, externally observable events, and traces. We call (t, f ,n), (t,ret,n) and (t,obj,abort) history events, and (t,out,n), (t,obj,abort) and (t,clt,abort) externally observable events. In Fig. 5 we define T JW ,SK as the prefix closed set of finite traces T generated during the execution of (W ,S). HJW ,SK contains the set of histories projected from traces in T JW ,SK. Here get_hist(T ) returns a subsequence E consisting of the history events projected from the corresponding labels in T . Similarly OJW ,SK contains the set of externally observable event traces projected from traces in T JW ,SK, where get_obsv(T ) is a subsequence E consisting of externally observable events only. As defined below, an event trace E is linearizable with respect to E ′ , i.e., E ≼lin E ′ , if they have the same sub-trace when projected over individual threads (projection represented as E |t ), and E is a permutation of E ′ but preserves the order of non-overlapping method calls in E ′ . Here we use is_inv(e) (or is_ret(e2)) to represent that e is in the form of (t, f ,n) (or (t,ret,n)). , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) :13 T[w,S】世T1w',S.(w,S)已(w',S)v(w,S)乙abort) HIw,S】兰{E13T.E=get_hist(T)AT∈T[w,SI) O[W.S]I 3T.8=get_obsv(T)ATETIW.S]) match(ee)is_inv(e)is_ret(e2)(tid(e)=tid(e)) is_inv(e) match(e1,e2)seq(E) Vt.seq(Elt) seq(e) seq(e :e) seq(e1 :e2 :8) well formed(E) well_formed(8) E'E extensions(E)is_ret(e)well_formed(&'++[e]) E extensions(E) E'++[e]E extensions(E) truncate(e)些e truncate(e::8) e::truncate(s)if is ret(e)or Ji.match(e.S(i)) truncate(S) otherwise completions(S)(truncate(S)I&'E extensions(E)) ©些{t1o,,tn→} r(,)iff 3n,C1.....Cn.c.(HI(let r in CIll...IICn).(c,,))A seq(E) Fig.5.Auxiliary definitions for linearizability. Definition 4.1(Linearizable Histories).E n &iff both the following hold. (1)Vt.Elt 8'l. (2)There exists a bijectionπ：{1，.，lel}→{1，..，le'l}such that Vi.e(i)=e'(π(i)and Vi,j.i<jnis_ret(8(i))A is_inv((j))=(i)<(j). Definition 4.2 says II is linearizable with respect to I and the state abstraction function (see Fig.3)if,for any trace generated by II with the initial object data o,the corresponding complete trace Ce is always linearizable with some sequential trace &'generated by I with initial object data E such that (o)=E.Some of the key notations are defined in Fig.5.We use to represent the initial thread pool where each thread has an empty call stack.completions(E)appends matching return events for some pending invocations in E,and discards the other pending invocations,so that in the resulting trace every invocation has a matching return.We use++for list concatenation, and [e1,...,en]for a list consisting of a sequence of elements.We use tid(e)for the thread ID in e. Definition 4.2(Linearizability ofObjects).The object implementation II is linearizable with respect toI,written as II≤gI,if n,C1,.,Cn,oc,o,∑，8.8∈H[(letΠinC1ll..lCm),(oe,o,@)lA(p(o)=) 3c,8'.(Ec E completions(E))A(r(,8))A(Ec <lin 8) Abstraction of linearizable objects.Filipovic et al.[Filipovic et al.2009]has shown that linearizabil- ity is equivalent to a contextual refinement.As defined below,II contextually refines I under the state abstraction function if,for any clients C1...Cn as the execution context,and for any initial object data related by o,executing II generates no more externally event traces than executing T. Theorem 4.4 shows the equivalence between linearizability and the contextual refinement. Definition 4.3(Basic Contextual Refinement).IIff n,C1,.,Cn,oc,0,∑.(p(o)=)→ [(letⅡin Cill...llCn),(oe,o,@)l∈OI(let r in Cill..lCn),(oe,Σ，@)l. Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :13 T JW ,SK def = {T | ∃W ′ ,S ′ . (W ,S) T 7−→∗ (W ′ ,S ′ ) ∨ (W ,S) T 7−→∗ abort} HJW ,SK def = {E | ∃T . E = get_hist(T ) ∧T ∈ T JW ,SK } OJW ,SK def = {E | ∃T . E = get_obsv(T ) ∧T ∈ T JW ,SK } match(e1,e2) def = is_inv(e1) ∧ is_ret(e2) ∧ (tid(e1) = tid(e2)) seq(ϵ ) is_inv(e) seq(e :: ϵ ) match(e1,e2) seq(E) seq(e1 :: e2 :: E) ∀t. seq(E |t ) well_formed(E) well_formed(E) E ∈ extensions(E) E ′ ∈ extensions(E) is_ret(e) well_formed(E ′++[e]) E ′++[e] ∈ extensions(E) truncate(ϵ ) def = ϵ truncate(e ::E) def = ( e ::truncate(E) if is_ret(e) or ∃i. match(e,E(i)) truncate(E) otherwise completions(E) def = {truncate(E ′ ) | E′ ∈ extensions(E)} } def = {t1 ❀ ◦,. . . ,tn ❀ ◦} Γ ◃ (Σ,E) iff ∃n,C1,. . . ,Cn,σc . ￾ E ∈HJ(let Γ in C1 ∥ . . . ∥Cn ), (σc ,Σ,})K
∧ seq(E) Fig. 5. Auxiliary definitions for linearizability. Definition 4.1 (Linearizable Histories). E ≼lin E ′ iff both the following hold. (1) ∀t. E |t = E ′ |t . (2) There exists a bijection π : {1,. . . , |E |} → {1,. . . , |E′ |} such that ∀i. E(i) = E ′ (π (i)) and ∀i,j. i < j ∧ is_ret(E(i)) ∧ is_inv(E(j)) =⇒ π (i) < π (j) . Definition 4.2 says Π is linearizable with respect to Γ and the state abstraction function φ (see Fig. 3) if, for any trace E generated by Π with the initial object data σ, the corresponding complete trace Ec is always linearizable with some sequential trace E ′ generated by Γ with initial object data Σ such that φ(σ ) = Σ. Some of the key notations are defined in Fig. 5. We use } to represent the initial thread pool where each thread has an empty call stack. completions(E) appends matching return events for some pending invocations in E, and discards the other pending invocations, so that in the resulting trace every invocation has a matching return. We use ++ for list concatenation, and [e1,. . . ,en] for a list consisting of a sequence of elements. We use tid(e) for the thread ID in e. Definition 4.2 (Linearizability of Objects). The object implementation Π is linearizable with respect to Γ, written as Π ≼ lin φ Γ, iff ∀n,C1,. . . ,Cn,σc ,σ,Σ,E. E ∈ HJ(let Π in C1 ∥ . . . ∥Cn ), (σc ,σ,})K ∧ (φ(σ ) = Σ) =⇒ ∃Ec ,E ′ . (Ec ∈ completions(E)) ∧ (Γ ◃ (Σ,E ′ )) ∧ (Ec ≼ lin E ′ ) Abstraction of linearizable objects. Filipović et al. [Filipović et al. 2009] has shown that linearizabil￾ity is equivalent to a contextual refinement. As defined below, Π contextually refines Γ under the state abstraction function φ if, for any clients C1 . . .Cn as the execution context, and for any initial object data related by φ, executing Π generates no more externally event traces than executing Γ. Theorem 4.4 shows the equivalence between linearizability and the contextual refinement. Definition 4.3 (Basic Contextual Refinement). Π ⊑ fin φ Γ iff ∀n,C1,. . . ,Cn,σc ,σ,Σ. (φ(σ ) = Σ) =⇒ OJ(let Π in C1 ∥ . . . ∥Cn ), (σc ,σ,})K ⊆ OJ(let Γ in C1 ∥ . . . ∥Cn ), (σc ,Σ,})K . , Vol. 1, No. 1, Article . Publication date: January 2018

:14 Hongjin Liang and Xinyu Feng THEOREM4.4(BASIC EQUIVALENCE FOR LINEARIZABILITY).I≤T←→IEPT. 5 PROGRESS PROPERTIES In this section we define the new progress properties,partial starvation-freedom(PSF)and partial deadlock-freedom (PDF),for objects with partial methods. We first define the trace set TW,S]in Fig.6.It contains the (possibly infinite)whole execution traces T generated by (W,S)but with a special label((spawn,Wl),Ac,Ao)inserted at the begin- ning.Here we use |Wl to represent the number of threads in W.The event(spawn,IWl)is used to define fairness,as explained below.Ac and Ao records the threads blocked in clients and object methods respectively(see the definition of btids in Fig.3).At the beginning of an execution,Ao must be an empty set since no threads are in method calls.The whole execution trace T may be generated under three cases,Le.,the execution of(W.S)diverges,aborts or gets stuck(terminates or is blocked).We write (W.S)for an infinite execution.In this case,the length ofT must be infinite,written as ITl =@ Strong and weak fairness.As defined in Fig.6,a trace T is strongly fair,represented as sfair(T),if each thread either terminates,or is executed infinitely many times if it is infinitely often enabled (i-o-enabled).We know a thread is enabled if it is not in the blocked sets Ac and Ao.T()represents the j-th element in the trace T.Similarly,wfair(T)says that T is a weakly fair trace.It requires that each thread either terminates,or is executed infinitely many times if it is always enabled after certain step on the trace(e-a-enabled). Thread progress and program progress.We use prog-t(T)in Fig.6 to say that every method call eventually terminates.It ensures that each individual thread calling a method eventually returns prog-p(T)says that there is always at least one method call that terminates.It ensures that the whole program is making progress.Here pend_inv(T)represents the set of method invocation events that do not have matching returns.T(1..i)represents the prefix of T with length i. Partial starvation-freedom(PSF)and partial deadlock-freedom(PDF).We want to define PSF as a generalization of starvation-freedom.We say an object II is partially starvation-free if,under fair scheduling(with strong or weak fairness),each method call eventually returns(as required in starvation-freedom),unless it is eventually always disabled(i.e.,it is not supposed to return in this particular execution context).In the latter case the non-termination is caused by inappropriate invocations of the methods in the client code and the object implementation should not be blamed. Although the idea is intuitive,it is challenging to formalize it.This is because when we say a method is disabled we are thinking at an abstract level,where the abstract disabling condition cannot be syntactically inferred based on the low-level object implementation II.For instance,the lock implementations in Fig.1 use non-blocking commands only,so they are always enabled to execute one more step at this level,although we intend to say at a more abstract level that the L_acq()operation is disabled when the lock is unavailable. To address this problem,we refer to the abstract object specification I when defining the progress of a concrete object II.Recall that method specifications in I are in the form of await(B)(C),so we know that the method is disabled when B does not hold. We formalize the idea as Def.5.1.Under the scheduling fairness x(where xE (sfair,wfair), as defined in Fig.6),we say the object II is PSF with respect to an abstract specification I and a state abstraction functionie.PSF(I).if any x-fair trace T generated by ((let II in Cl.. Cn),(oc,,))either aborts,or satisfies prog-t,or we could blame the client for the blocking of each pending invocation Vol.1,No.1,Article.Publication date:January 2018

:14 Hongjin Liang and Xinyu Feng Theorem 4.4 (Basic Eqivalence for Linearizability). Π ≼ lin φ Γ ⇐⇒ Π ⊑ fin φ Γ. 5 PROGRESS PROPERTIES In this section we define the new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF), for objects with partial methods. We first define the trace set TωJW ,SK in Fig. 6. It contains the (possibly infinite) whole execution traces T generated by (W ,S) but with a special label ((spawn, |W |),∆c ,∆o ) inserted at the begin￾ning. Here we use |W | to represent the number of threads in W . The event (spawn, |W |) is used to define fairness, as explained below. ∆c and ∆o records the threads blocked in clients and object methods respectively (see the definition of btids in Fig. 3). At the beginning of an execution, ∆o must be an empty set since no threads are in method calls. The whole execution trace T may be generated under three cases, i.e., the execution of (W ,S) diverges, aborts or gets stuck (terminates or is blocked). We write (W ,S) T 7−→ω · for an infinite execution. In this case, the length of T must be infinite, written as |T | = ω. Strong and weak fairness. As defined in Fig. 6, a trace T is strongly fair, represented as sfair(T ), if each thread either terminates, or is executed infinitely many times if it is infinitely often enabled (i-o-enabled). We know a thread is enabled if it is not in the blocked sets ∆c and ∆o . T (j) represents the j-th element in the trace T . Similarly, wfair(T ) says that T is a weakly fair trace. It requires that each thread either terminates, or is executed infinitely many times if it is always enabled after certain step on the trace (e-a-enabled). Thread progress and program progress. We use prog-t(T ) in Fig. 6 to say that every method call eventually terminates. It ensures that each individual thread calling a method eventually returns. prog-p(T ) says that there is always at least one method call that terminates. It ensures that the whole program is making progress. Here pend_inv(T ) represents the set of method invocation events that do not have matching returns. T (1..i) represents the prefix of T with length i. Partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). We want to define PSF as a generalization of starvation-freedom. We say an object Π is partially starvation-free if, under fair scheduling (with strong or weak fairness), each method call eventually returns (as required in starvation-freedom), unless it is eventually always disabled (i.e., it is not supposed to return in this particular execution context). In the latter case the non-termination is caused by inappropriate invocations of the methods in the client code and the object implementation should not be blamed. Although the idea is intuitive, it is challenging to formalize it. This is because when we say a method is disabled we are thinking at an abstract level, where the abstract disabling condition cannot be syntactically inferred based on the low-level object implementation Π. For instance, the lock implementations in Fig. 1 use non-blocking commands only, so they are always enabled to execute one more step at this level, although we intend to say at a more abstract level that the L_acq() operation is disabled when the lock is unavailable. To address this problem, we refer to the abstract object specification Γ when defining the progress of a concrete object Π. Recall that method specifications in Γ are in the form of await(B){C}, so we know that the method is disabled when B does not hold. We formalize the idea as Def. 5.1. Under the scheduling fairness χ (where χ ∈ {sfair,wfair}, as defined in Fig. 6), we say the object Π is PSF with respect to an abstract specification Γ and a state abstraction function φ, i.e., PSFχ φ,Γ (Π), if any χ-fair trace T generated by ((let Π in C1 ∥ . . . ∥ Cn ), (σc ,σ,})) either aborts, or satisfies prog-t, or we could blame the client for the blocking of each pending invocation. , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) :15 Taw,S】g{((spawn,.lwD,△e,△o):TI btids(w,S)=(ac,△o)A (((W.S).)v((W.S)abort)v3W.S'.((W.S)(W'.s))A-(.(W'.s)) llet II in C:ll ..Il Cnl n tnum((spawn,n),△c,△o):T)些n evt0些eif1=(e,△e,Ao) bset0兰△eU△oif1=(e,△c,△o) i-o-enabled(t,T)ifVi.3j≥i.t生bset(TU) “infinitely often" e-a-enabled(t,T)if3i.i≥i.t生bset(TU) "eventually always" sfair(T)iff ITI==Vt E [1..tnum(T)].evt(last(Tlt))=(t,term)v (i-o-enabled(t,T)I(Tlt)1=@) wfair(T)iff IT|=0=Vt E [1..tnum(T)].evt(last(Tlt))=(t,term)v(e-a-enabled(t,T)I(Tlt)=@) pend_inv(T)leli.e=evt(T())Ais_inv(e)>i.match(e.evt(T()))) abt(T)iff Ji.is_abt(evt(T(i))) prog-t(T)iff pend_inv(T)=0 prog-p(T)ifi,e.e∈pend_inv(T(1.i)→3j>i.is_ret(evt(TU)》 e-a-disabled(tT)if3i.≥i,l=TU).t∈bset() “eventually always'" well-blocked(T,(Wa,Sa))iff 3Ta.Ta E TlWa,Sa]A(get_hist(T)=get_hist(Ta)) A (Ve.eE pend_inv(Ta)=e-a-disabled(tid(e),Ta)) OxIW,(oe,co月些{8|3T.T∈TIw,(ae,oo,©lAx(T)Aget_obsv(T)=8l X∈{sfair,wfair) Fig.6.Fairness and progress. In the last case,we must be able to find a trace Ta generated by the execution of the abstract object I(with the abstract object state related to o by )such that it has the same method invocation and return history with T,and every pending invocation in this abstract trace Ta is eventually always disabled.See the definition of well-blocked in Fig.6 for the formal details. Definition 5.1(Partially Starvation-Free Objects).PSF( Vn,C1.....Cn,ac,,T.TE Tl(let II in Cill...IICn),(c,,)]A ((a)=)Ax(T) abt(T)V prog-t(T)v well-blocked(T,((let r in Ci ll...II Cn),(c,,))). We also define PDF in Def.5.2.It is similar to PSF,but requires prog-p instead of prog-t. Definition 5.2(Partially Deadlock-Free Objects).PDF Vn.C1....,Cn,c,,,T.TE Tl(let II in Cill...llCn),(oc,,)]A ((a)=)Ax(T) abt(T)V prog-p(T)V well-blocked(T,((let r in Cill...IICn),(c,,))). The above definitions consider the three factors that may affect the termination of a method call:the scheduling fairness x,the object implementation II which determines whether its traces satisfy prog-t or prog-p,and the execution context Cill...Il Cn which may make inappropriate method invocations so that well-blocked holds.Consider the lock objects in Fig.1(a)and (c)and Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :15 TωJW ,SK def = {((spawn, |W |),∆c ,∆o ) ::T | btids(W ,S) = (∆c ,∆o ) ∧ (((W ,S) T 7−→ω · ) ∨ ((W ,S) T 7−→∗ abort) ∨ ∃W ′ ,S ′ . ((W ,S) T 7−→∗ (W ′ ,S ′ )) ∧ ¬(∃ι. (W ′ ,S ′ ) ι 7−→ _)) } |let Π in C1 ∥ . . . ∥ Cn | def = n tnum(((spawn,n),∆c ,∆o ) ::T ) def = n evt(ι) def = e if ι = (e,∆c ,∆o ) bset(ι) def = ∆c ∪ ∆o if ι = (e,∆c ,∆o ) i-o-enabled(t,T ) iff ∀i. ∃j ≥ i. t < bset(T (j)) “infinitely often” e-a-enabled(t,T ) iff ∃i. ∀j ≥ i. t < bset(T (j)) “eventually always” sfair(T ) iff |T |=ω =⇒ ∀t ∈ [1..tnum(T )]. evt(last(T |t )) = (t,term) ∨ (i-o-enabled(t,T ) ⇒ |(T |t )| = ω) wfair(T ) iff |T |=ω =⇒ ∀t ∈ [1..tnum(T )]. evt(last(T |t )) = (t,term) ∨ (e-a-enabled(t,T ) ⇒ |(T |t )| = ω) pend_inv(T ) def = {e | ∃i. e = evt(T (i)) ∧ is_inv(e) ∧ ¬∃j > i. match(e,evt(T (j))) } abt(T ) iff ∃i. is_abt(evt(T (i))) prog-t(T ) iff pend_inv(T ) = ∅ prog-p(T ) iff ∀i,e. e ∈ pend_inv(T (1..i)) =⇒ ∃j > i. is_ret(evt(T (j))) e-a-disabled(t,T ) iff ∃i. ∀j ≥ i,ι = T (j). t ∈ bset(ι) “eventually always” well-blocked(T , (Wa,Sa )) iff ∃Ta . Ta ∈ TωJWa,SaK ∧ (get_hist(T ) = get_hist(Ta )) ∧ (∀e. e ∈ pend_inv(Ta ) =⇒ e-a-disabled(tid(e),Ta )) Oχ JW , (σc ,σo )K def = {E | ∃T . T ∈ TωJW , (σc ,σo ,})K ∧ χ (T ) ∧ get_obsv(T ) = E } χ ∈ {sfair,wfair} Fig. 6. Fairness and progress. In the last case, we must be able to find a traceTa generated by the execution of the abstract object Γ (with the abstract object state Σ related to σ by φ) such that it has the same method invocation and return history with T , and every pending invocation in this abstract trace Ta is eventually always disabled. See the definition of well-blocked in Fig. 6 for the formal details. Definition 5.1 (Partially Starvation-Free Objects). PSFχ φ,Γ (Π) iff ∀n,C1,. . . ,Cn,σc ,σ,Σ,T . T ∈ TωJ(let Π in C1 ∥ . . . ∥Cn ), (σc ,σ,})K ∧ (φ(σ ) = Σ) ∧ χ (T ) =⇒ abt(T ) ∨ prog-t(T ) ∨ well-blocked(T , ((let Γ in C1 ∥ . . . ∥Cn ), (σc ,Σ,}))) . We also define PDF in Def. 5.2. It is similar to PSF, but requires prog-p instead of prog-t. Definition 5.2 (Partially Deadlock-Free Objects). PDFχ φ,Γ (Π) iff ∀n,C1,. . . ,Cn,σc ,σ,Σ,T . T ∈ TωJ(let Π in C1 ∥ . . . ∥Cn ), (σc ,σ,})K ∧ (φ(σ ) = Σ) ∧ χ (T ) =⇒ abt(T ) ∨ prog-p(T ) ∨ well-blocked(T , ((let Γ in C1 ∥ . . . ∥Cn ), (σc ,Σ,}))) . The above definitions consider the three factors that may affect the termination of a method call: the scheduling fairness χ, the object implementation Π which determines whether its traces satisfy prog-t or prog-p, and the execution context C1 ∥ . . . ∥Cn which may make inappropriate method invocations so that well-blocked holds. Consider the lock objects in Fig. 1(a) and (c) and , Vol. 1, No. 1, Article . Publication date: January 2018