Progress of Concurrent Objects with Partial Methods（Extended Version）

:16 Hongjin Liang and Xinyu Feng the following client program(5.1).The initial value of the shared variable x is 0. [_]Aco;print(0);[_]REL; [_]ace;print(2); X:=1; while(x=1){ (5.1) [_lace;print(1);[_]REL; [_]RE;[_]ace;print(3); The client can produce a trace satisfying prog-t when it uses the ticket lock.It first executes the left thread until termination and then executes the right thread.Then every method call terminates, printing out 0,1,2 and an infinite number of 3.Thus prog-t holds.When the test-and-set lock is used instead,the same client can produce a trace satisfying prog-p but not prog-t.In the execution, the second call to L_acq in the left thread never finishes.It prints out 0,2 and an infinite number of 3,but not 1.Such an execution is not possible when the client uses the ticket lock,under fair scheduling.This shows how different object implementations affect termination of method calls Note that neither of the two execution traces satisfies well-blocked,because every method call in the traces either terminates or is enabled infinitely often. On the other hand,the client(5.1)can produce a well-blocked trace no matter it uses the ticket lock or the test-and-set lock.It executes the right thread first until termination and then executes the left thread.Then the first call to lock acquire of the left thread is always blocked,and only 2 is printed during the execution.The non-termination of the method call is caused by the particular execution context,in which the method call is not supposed to return,regardless of the object implementations.This is why the same well-blocked condition is used in both definitions of PSF and PDF for both strongly and weakly fair executions of the object implementation. PSF(or PDF)and starvation-freedom (or deadlock-freedom)coincide if we require each await block in I is in the special form of await(true)(C)-Since the methods in I are always enabled, well-blocked(T,((let r in Cill...II Cn),Sa))now requires that there is no pending invocation in T. This is stronger than both prog-t(T)and prog-p(T).Therefore we can remove the disjunction branch about well-blocked in Defs.5.1 and 5.2,resulting in definitions equivalent to starvation-freedom and deadlock-freedom respectively. 6 PROGRESS-AWARE ABSTRACTION OF OBJECTS In this section we study the abstraction of linearizable and PSF(or PDF)objects.Similar to Theo- rem 4.4,we want theorems showing that linearizability along with PSF(or PDF)of an object II is equivalent to a contextual refinement between II and some abstract object II',where II'can be syntactically derived from the atomic specification I. We first define the progress-aware contextual refinement for objects under different fairness x of scheduling (xE [sfair,wfair)).As Def.6.1 shows,II contextually refines II'under the x-fair scheduling if,in any execution context,II generates no more externally observable event traces than II'.The set of event traces OxI(let II in Cill...Il Cn),(oc,)]is defined in Fig.6,where each event trace is extracted from the x-fair trace T in T(let II in Ci ll...Il Cn),(c,o,)1.The refinement is progress-aware because we use the whole execution trace T here,from which we can tell whether the corresponding execution terminates or not. Definition 6.1(Progress-Aware Contextual Refinement). Π二Π'fn,C1,,Cn,oc,o,∑.p(o)=Σ→ xI(let II in Cill...IICn),(,)]cOxl(let II'in Cill...IlCn),(c,)] Wrappers for atomic specifications.As explained in Sec.2,one of the major contributions of this paper is to define wrappers for atomic partial specifications I,which transform the method specifi- cation await(B)(C)in I into a(possibly non-atomic)abstract specification for each combination of progress(PSF or PDF)and fairness(sfair or wfair),as shown in Table 2. Vol.1,No.1,Article.Publication date:January 2018

:16 Hongjin Liang and Xinyu Feng the following client program (5.1). The initial value of the shared variable x is 0. [ _ ]acq; print(0); [ _ ]rel; x:=1; [ _ ]acq; print(1); [ _ ]rel; [ _ ]acq; print(2); while(x=1){ [ _ ]rel; [ _ ]acq; print(3); } (5.1) The client can produce a trace satisfying prog-t when it uses the ticket lock. It first executes the left thread until termination and then executes the right thread. Then every method call terminates, printing out 0, 1, 2 and an infinite number of 3. Thus prog-t holds. When the test-and-set lock is used instead, the same client can produce a trace satisfying prog-p but not prog-t. In the execution, the second call to L_acq in the left thread never finishes. It prints out 0, 2 and an infinite number of 3, but not 1. Such an execution is not possible when the client uses the ticket lock, under fair scheduling. This shows how different object implementations affect termination of method calls. Note that neither of the two execution traces satisfies well-blocked, because every method call in the traces either terminates or is enabled infinitely often. On the other hand, the client (5.1) can produce a well-blocked trace no matter it uses the ticket lock or the test-and-set lock. It executes the right thread first until termination and then executes the left thread. Then the first call to lock acquire of the left thread is always blocked, and only 2 is printed during the execution. The non-termination of the method call is caused by the particular execution context, in which the method call is not supposed to return, regardless of the object implementations. This is why the same well-blocked condition is used in both definitions of PSF and PDF for both strongly and weakly fair executions of the object implementation. PSF (or PDF) and starvation-freedom (or deadlock-freedom) coincide if we require each await block in Γ is in the special form of await(true){C} — Since the methods in Γ are always enabled, well-blocked(T , ((let Γ in C1 ∥ . . . ∥Cn ),Sa )) now requires that there is no pending invocation in T . This is stronger than both prog-t(T ) and prog-p(T ). Therefore we can remove the disjunction branch about well-blocked in Defs. 5.1 and 5.2, resulting in definitions equivalent to starvation-freedom and deadlock-freedom respectively. 6 PROGRESS-AWARE ABSTRACTION OF OBJECTS In this section we study the abstraction of linearizable and PSF (or PDF) objects. Similar to Theo￾rem 4.4, we want theorems showing that linearizability along with PSF (or PDF) of an object Π is equivalent to a contextual refinement between Π and some abstract object Π ′ , where Π ′ can be syntactically derived from the atomic specification Γ. We first define the progress-aware contextual refinement for objects under different fairness χ of scheduling (χ ∈ {sfair,wfair}). As Def. 6.1 shows, Π contextually refines Π ′ under the χ-fair scheduling if, in any execution context, Π generates no more externally observable event traces than Π ′ . The set of event traces Oχ J(let Π in C1 ∥ . . . ∥Cn ), (σc ,σ )K is defined in Fig. 6, where each event trace E is extracted from the χ-fair trace T in TωJ(let Π in C1 ∥ . . . ∥ Cn ), (σc ,σ,})K. The refinement is progress-aware because we use the whole execution trace T here, from which we can tell whether the corresponding execution terminates or not. Definition 6.1 (Progress-Aware Contextual Refinement). Π ⊑ χ φ Π ′ iff ∀n,C1,. . . ,Cn,σc ,σ,Σ. φ(σ ) = Σ =⇒ Oχ J(let Π in C1 ∥ . . . ∥Cn ), (σc ,σ )K ⊆ Oχ J(let Π ′ in C1 ∥ . . . ∥Cn ), (σc ,Σ)K Wrappers for atomic specifications. As explained in Sec. 2, one of the major contributions of this paper is to define wrappers for atomic partial specifications Γ, which transform the method specifi￾cation await(B){C} in Γ into a (possibly non-atomic) abstract specification for each combination of progress (PSF or PDF) and fairness (sfair or wfair), as shown in Table 2. , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) :17 wrpro(T)(f) 些(e,x,wr(await(B)C方returnE月 if r(f)=(P,x,await(B)(C);return E) wrs(await(B)(C])await(B)(C) wr(await(B)IC)些1 istid:=listid++[cid,B)小 await(BA cid enhd(listid))(C;listid:=listid\cid; wr德(await(B)IC)g while (done); await(B A -done)(C;done :true;)done :false; while (done)(); WIPDE(await(B){C)些 await(B A-done)(C;done:=true;)done :false; await(-done)() wrpr(p)(a)些 a'w(listid~e)ifo(o)=a' undefined ifo生dom(p) wr(p)世p wrpp()(a) '(done~false)if o(o)=o' undefined if o dom(o) Fig.7.Definition of wrappers. Before introducing the definition of the wrappers in Fig.7,we first show our abstraction theorem (Theorem 6.2)for linearizable and PSF (or PDF)objects.It establishes the equivalence between the progress-aware contextual refinement and linearizability with PSF(or PDF). THEOREM 6.2 (ABSTRACTION THEOREM).Let Prog E (PSF,PDF)and X E(sfair,wfair),then I≤TA Progz.n(四)=1 wrProg(T), wherer)and the wrappers for T and are defined in Fig.7.We also assume that the variables listid and done introduced in the wrapper code are fresh,i.e.,listid,done FV(,,)). To prove the theorem,we define compositional operational semantics that can generate separate traces for objects and clients,and build simulations using the object semantics.Detailed proofs are given in Appendix A. Next we introduce the definition of the wrappers in detail The wrapper wris simply an identity function.It maps the atomic specification await(B)(C)to itself.This is because under strongly fair scheduling await(B)(C)will eventually be executed unless it is eventually always disabled.This is exactly what we need for PSF of linearizable objects,which requires that the invocation of each method eventually returns,unless the corresponding high-level atomic operation await(B)(C)is eventually always disabled(as specified by well-blocked in Fig.6). Wrapper for PSF under weakly fair scheduling.Under weakly fair scheduling,however,we cannot guarantee that await(B)(C)is eventually executed even if B holds infinitely often.Therefore it alone cannot satisfy PSF.That's why we define wr(await(B)(C)),which guarantees that the atomic operation is eventually executed if B holds infinitely often.We introduce a blocking queue listid in the object state,which is a sequence of(t,B')pairs,showing that the thread t requests to execute an atomic operation with the enabling condition B.Note that the enabling condition B is recorded syntactically in listid,represented as'B'.The operator enhd(listid)returns the first Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :17 wr χ Prog (Γ)(f ) def = (P,x, wr χ Prog (await(B){C}); return E) if Γ(f ) = (P,x, await(B){C}; return E) wrsfair PSF (await(B){C}) def = await(B){C} wrwfair PSF (await(B){C}) def = listid := listid++[(cid,‘B’)]; await(B ∧ cid = enhd(listid)){C; listid := listid\cid; } wrsfair PDF (await(B){C}) def = while (done){}; await(B ∧ ¬done){C; done := true; }; done := false; while (done){}; wrwfair PDF (await(B){C}) def = await(B ∧ ¬done){C; done := true; }; done := false; await(¬done){} wrwfair PSF (φ)(σ ) def = ( σ ′ ⊎ {listid ❀ ϵ } if φ(σ ) = σ ′ undefined if σ < dom(φ) wrsfair PSF (φ) def = φ wr χ PDF (φ)(σ ) def = ( σ ′ ⊎ {done ❀ false} if φ(σ ) = σ ′ undefined if σ < dom(φ) Fig. 7. Definition of wrappers. Before introducing the definition of the wrappers in Fig. 7, we first show our abstraction theorem (Theorem 6.2) for linearizable and PSF (or PDF) objects. It establishes the equivalence between the progress-aware contextual refinement and linearizability with PSF (or PDF). Theorem 6.2 (Abstraction Theorem). Let Prog ∈ {PSF,PDF} and χ ∈ {sfair,wfair}, then Π ≼ lin φ Γ ∧ Progχ φ,Γ (Π) ⇐⇒ Π ⊑ χ φD wr χ Prog (Γ) , where φD = wr χ Prog (φ), and the wrappers for Γ and φ are defined in Fig. 7. We also assume that the variables listid and done introduced in the wrapper code are fresh, i.e., listid,done < FV({Π, Γ,φ}). To prove the theorem, we define compositional operational semantics that can generate separate traces for objects and clients, and build simulations using the object semantics. Detailed proofs are given in Appendix A. Next we introduce the definition of the wrappers in detail. The wrapper wrsfair PSF is simply an identity function. It maps the atomic specification await(B){C} to itself. This is because under strongly fair scheduling await(B){C} will eventually be executed unless it is eventually always disabled. This is exactly what we need for PSF of linearizable objects, which requires that the invocation of each method eventually returns, unless the corresponding high-level atomic operation await(B){C} is eventually always disabled (as specified by well-blocked in Fig. 6). Wrapper for PSF under weakly fair scheduling. Under weakly fair scheduling, however, we cannot guarantee that await(B){C} is eventually executed even if B holds infinitely often. Therefore it alone cannot satisfy PSF. That’s why we define wrwfair PSF (await(B){C}), which guarantees that the atomic operation is eventually executed if B holds infinitely often. We introduce a blocking queue listid in the object state, which is a sequence of (t,‘B’) pairs, showing that the thread t requests to execute an atomic operation with the enabling condition B. Note that the enabling condition B is recorded syntactically in listid, represented as ‘B’. The operator enhd(listid) returns the first , Vol. 1, No. 1, Article . Publication date: January 2018

:18 Hongjin Liang and Xinyu Feng thread on the list whose enabling condition is true.It evaluates the syntactic enabling conditions 'B'recorded in listid on the fly.Note that different pairs in listid may have different enabling conditions B.In the code generated by wr(await(B)(C)).we first append the current thread ID and the enabling condition'B'at the end of the list.In the subsequent command the thread waits until both B holds and cid enhd(listid)'.Then it atomically executes C and deletes the current thread in the queue. This wrapper guarantees that C is eventually executed when B becomes infinitely often true because we know B A cid=enhd(listid)will be eventually always true,and then the weakly fair scheduling guarantees the execution of C.This is because,whenever B becomes true,either cid enhd(listid)holds or there is a pair (t',B')such that B'At'=enhd(listid)holds.In the first case,other threads trying to execute the object methods must be blocked at the await command. Therefore B cannot be changed to false by other threads.Therefore B A cid=enhd(listid)is always true until the current thread executes the atomic block.In the second case t'must be able to finish its method,following the same argument above.Therefore there will be one less thread waiting in front of the current thread cid.Since B becomes true infinitely often,we eventually reach the first case. As a result,the wrapper does not terminate in a weakly fair execution only if B is eventually always false.In that case the execution trace is well-blocked(see Fig.6),still satisfying PSF. One may argue that the abstraction generated by the wrapper is not very useful because it may not be much simpler than the object implementation.For instance,if we consider the acquire method of locks,the abstraction is almost the same as queue locks or ticket locks.But we want to emphasize that our wrapper is a general one that works for any object method implementation with an atomic specification in the form of await(B)(C).Therefore we know the method's progress-aware abstraction can always be in this form,no matter how complex its implementation is. Wrapper for PDF under weakly fair scheduling.For the right column in Table 2,we first introduce the wrapper at the bottom right corner.The definition of PDF says a method can be non-terminating if(1)it is eventually always disabled,as specified by well-blocked(see Fig.6);or(2)there are always other method calls terminating,as specified by prog-p.Note that the second condition allows the method to be non-terminating even if it is eventually always enabled under weakly fair scheduling. As an example,the Treiber stack with a partial pop in Fig.8 demonstrates one such scenario.The pop method is blocked when the stack is empty.It is linearizable with respect to the following specification await(S#nil)(tmp :head(S);S :tail(S);)return tmp; (6.1) where S is the abstraction of the stack and tmp is a thread-local temporary variable. In the following execution context (6.2), pop();II while(true){push(0); (6.2) the call of the concrete method pop may never terminate because its cas command may always fail, although the enabling condition at the abstract level(S#nil)is eventually always true.However, if we replace the method implementation with the specification(6.1),pop must terminate under weakly fair scheduling.This shows that the concrete implementation cannot contextually refine this simple specification(6.1). Our first attempt to address this problem is to introduce a new object variable done(initialized to false),and let the wrapper wrtransform await(B)(C)into: await(B A-done)(C;done :true);done :false; (6.3) Actually the conjunct B in the await condition in the wrapper could be omitted,because B must be true when cid= enhd(listid)holds. .Vol.1,No.1,Article.Publication date:January 2018

:18 Hongjin Liang and Xinyu Feng thread on the list whose enabling condition is true. It evaluates the syntactic enabling conditions ‘B’ recorded in listid on the fly. Note that different pairs in listid may have different enabling conditions B. In the code generated by wrwfair PSF (await(B){C}), we first append the current thread ID and the enabling condition ‘B’ at the end of the list. In the subsequent command the thread waits until both B holds and cid = enhd(listid) 1 . Then it atomically executes C and deletes the current thread in the queue. This wrapper guarantees that C is eventually executed when B becomes infinitely often true because we know B ∧ cid = enhd(listid) will be eventually always true, and then the weakly fair scheduling guarantees the execution of C. This is because, whenever B becomes true, either cid = enhd(listid) holds or there is a pair (t ′ ,B ′ ) such that B ′ ∧t ′ = enhd(listid) holds. In the first case, other threads trying to execute the object methods must be blocked at the await command. Therefore B cannot be changed to false by other threads. Therefore B ∧ cid = enhd(listid) is always true until the current thread executes the atomic block. In the second case t ′ must be able to finish its method, following the same argument above. Therefore there will be one less thread waiting in front of the current thread cid. Since B becomes true infinitely often, we eventually reach the first case. As a result, the wrapper does not terminate in a weakly fair execution only if B is eventually always false. In that case the execution trace is well-blocked (see Fig. 6), still satisfying PSF. One may argue that the abstraction generated by the wrapper is not very useful because it may not be much simpler than the object implementation. For instance, if we consider the acquire method of locks, the abstraction is almost the same as queue locks or ticket locks. But we want to emphasize that our wrapper is a general one that works for any object method implementation with an atomic specification in the form of await(B){C}. Therefore we know the method’s progress-aware abstraction can always be in this form, no matter how complex its implementation is. Wrapper for PDF under weakly fair scheduling. For the right column in Table 2, we first introduce the wrapper at the bottom right corner. The definition of PDF says a method can be non-terminating if (1) it is eventually always disabled, as specified by well-blocked (see Fig. 6); or (2) there are always other method calls terminating, as specified by prog-p. Note that the second condition allows the method to be non-terminating even if it is eventually always enabled under weakly fair scheduling. As an example, the Treiber stack with a partial pop in Fig. 8 demonstrates one such scenario. The pop method is blocked when the stack is empty. It is linearizable with respect to the following specification await(S , nil){tmp := head(S); S := tail(S); }; return tmp; (6.1) where S is the abstraction of the stack and tmp is a thread-local temporary variable. In the following execution context (6.2), pop(); || while(true){ push(0); } (6.2) the call of the concrete method pop may never terminate because its cas command may always fail, although the enabling condition at the abstract level (S , nil) is eventually always true. However, if we replace the method implementation with the specification (6.1), pop must terminate under weakly fair scheduling. This shows that the concrete implementation cannot contextually refine this simple specification (6.1). Our first attempt to address this problem is to introduce a new object variable done (initialized to false), and let the wrapper wrwfair PDF transform await(B){C} into: await(B ∧ ¬done){C; done := true}; done := false; (6.3) 1 Actually the conjunct B in the await condition in the wrapper could be omitted, because B must be true when cid = enhd(listid) holds. , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) :19 initialize(){Top :null; pop(){ 91oca1×,b,t,v; 10 b :false; push(v){ 11ocal×,b,t; 11 while (!b){ 2 b :false; 12 t :Top; 13 3×:=cons(v,nul1); if (t !null){ 4 while (!b){ 14 v :t.data; 5 t:=Top; 15 x :t.next; 16 6 x.next :t; b:=cas(&Top,t,x); 7 b :cas(&Top,t,x); 17 18 83 19 return v; 2 initialize'(){initialize();done false;} push'(v){push(v);DLY_NOOP] pop'(v){tmp :pop();DLY_NOOP;return tmp} DLY_NOOP await(-done)(done :=truel:done:=false; push'(1); r0 :pop'(); push'(2); r1:=pop'(); print(r0); print(r1); while(true]{push'(0)}; Fig.8.Treiber stacks with partial pops. Therefore the resulting await command may not be executed even if B is always true,because done can be set to true infinitely often when other threads finish the atomic block.Also note done is reset to false at the end of each await command,therefore the condition -done cannot always disable the await command,which may cause deadlock.As a result,there is always some thread that can finish the wrapper(ie.,prog-p holds)unless the B-s of all the pending invocations are eventually always false(i.e.,well-blocked holds),thus PDF holds. However,this is not the end of the story.If the code(6.3)fails to terminate,C must not be executed and no effects(over the object data)are generated.However,it is possible for PDF methods to finish C and make the effects visible to other threads but fail to terminate.As an example we define the push'and pop'methods in Fig.8 as a new implementation of the Treiber stack.They call the push and pop methods respectively and then execute the code snippet DLY_NOOP before they return.DLY_NOOP simply waits until done becomes false and then atomically sets it to true,and finally resets it to false.The only purpose of DLY_NOOP is to allow the methods to be delayed by other threads or to delay others. Then we consider the client code shown at the bottom of Fig.8.Under weakly fair scheduling it is possible that the call of pop'()by the left thread never terminates but the thread on the right prints out 1.That is,although the pop'()on the left does not terminate,it does generate effects over the stack and the effects happen before the pop'()on the right.Such an external event trace cannot be generated if we replace the concrete push'()and pop'()methods with the abstract method code generated using the wrapper(6.3)defined above.Thus the contextual refinement between the concrete code and the wrapped specification does not hold. Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :19 initialize(){ Top := null; } push(v){ 1 local x, b, t; 2 b := false; 3 x := cons(v, null); 4 while (!b) { 5 t := Top; 6 x.next := t; 7 b := cas(&Top, t, x); 8 } } pop(){ 9 local x, b, t, v; 10 b := false; 11 while (!b) { 12 t := Top; 13 if (t != null) { 14 v := t.data; 15 x := t.next; 16 b := cas(&Top, t, x); 17 } 18 } 19 return v; } initialize'(){ initialize(); done := false;} push'(v){ push(v); DLY_NOOP} pop'(v){ tmp := pop(); DLY_NOOP; return tmp} DLY_NOOP def = await(¬done){done := true}; done := false; r0 := pop'(); print(r0); push'(1); push'(2); r1 := pop'(); print(r1); while(true}{ push'(0) }; Fig. 8. Treiber stacks with partial pops. Therefore the resulting await command may not be executed even if B is always true, because done can be set to true infinitely often when other threads finish the atomic block. Also note done is reset to false at the end of each await command, therefore the condition ¬done cannot always disable the await command, which may cause deadlock. As a result, there is always some thread that can finish the wrapper (i.e., prog-p holds) unless the B-s of all the pending invocations are eventually always false (i.e., well-blocked holds), thus PDF holds. However, this is not the end of the story. If the code (6.3) fails to terminate,C must not be executed and no effects (over the object data) are generated. However, it is possible for PDF methods to finish C and make the effects visible to other threads but fail to terminate. As an example we define the push’ and pop’ methods in Fig. 8 as a new implementation of the Treiber stack. They call the push and pop methods respectively and then execute the code snippet DLY_NOOP before they return. DLY_NOOP simply waits until done becomes false and then atomically sets it to true, and finally resets it to false. The only purpose of DLY_NOOP is to allow the methods to be delayed by other threads or to delay others. Then we consider the client code shown at the bottom of Fig. 8. Under weakly fair scheduling it is possible that the call of pop’() by the left thread never terminates but the thread on the right prints out 1. That is, although the pop’() on the left does not terminate, it does generate effects over the stack and the effects happen before the pop’() on the right. Such an external event trace cannot be generated if we replace the concrete push’() and pop’() methods with the abstract method code generated using the wrapper (6.3) defined above. Thus the contextual refinement between the concrete code and the wrapped specification does not hold. , Vol. 1, No. 1, Article . Publication date: January 2018

:20 Hongjin Liang and Xinyu Feng Our solution is to append an await command at the end of(6.3),so that the resulting code wr(await(B)(C))(see Fig.7)may finish C but still be blocked at the end. Wrapper for PDF under strongly fair scheduling.Much of the effort to define wr(await(B)(C)) is to allow the resulting code to be non-terminating even if B is eventually always true.We need to do the same to define wr(await(B)(C).but it is more challenging with strongly fair scheduling because await(-done)()cannot be blocked under strongly fair scheduling if done is infinitely often true.Therefore we use while-loops in wr(await(B)(C)to allow the method to be delayed when done is infinitely often true2.Note that while(done)()terminates when done is false. Wrappers for the state abstraction function.Since the program transformations by the wrappers introduce new object variables such as listid and done,we need to change the state abstraction function accordingly,which is defined as wr)in Fig.7(x(sfair,wfair)and Prog (PSF,PDF)). More discussions.There could be different ways to define the wrappers to validate the Abstraction Theorem 6.2.We do not intend to claim that our definitions are the simplest ones(and it is unclear how to formally compare the complexity of different wrappers),but we would like to point out that,although some of the wrappers look complex,the complexity is partly due to the effort to have general wrappers that work for any atomic specifications in the form of await(B)(C).It is possible to have simpler wrappers for specific objects.For instance,the lock specification I in(2.3) defined in Sec.2.2 can already serve as an abstraction for the test-and-set lock object IITas(which is a PDF lock)under weakly fair scheduling.i.e.Isholds. 7 PROGRAM LOGIC We extend the program logic LiLi [Liang and Feng 2016]to verify progress properties of concurrent objects with partial methods.LiLi is a rely-guarantee style program logic to verify linearizability and starvation-freedom/deadlock-freedom of concurrent objects.It establishes progress-aware contextual refinements between concrete object implementations and abstract(total)specifications. The key ideas of LiLi to verify progress are the following: A thread can be blocked,relying on the actions of other threads(i.e.,its environment)to make progress.To ensure it eventually progresses,we must guarantee that the environment actions that the thread waits for eventually occur. To avoid circularity in rely-guarantee reasoning,each thread specifies a set of definite actions D,which are state transitions specified in the form of pQ.The thread guarantees that, whenever a definite action PO is "enabled"(i.e.,the assertion P holds),the transition must occur so that O eventually holds,regardless of the environment behaviors .A blocked thread must wait for a set of definite actions of other threads,and the size of the set must be decreasing(so that the thread is eventually unblocked). A thread may delay the progress of others,i.e.,to make other threads to execute more steps than they need when executed in isolation.To ensure deadlock-freedom,LiLi disallows a thread to be delayed infinitely often without whole system progress.This is achieved by using tokens as resources and each delaying action must consume a token. These ideas to reason about blocking and delay are general enough for verifying objects with partial methods,but we have to first generalize LiLi in the following two aspects: 2Actually the conjunct-done in the await condition in the wrapper could be removed,because the loop while (done) before the await block can already produce the non-terminating behaviors when other threads finish the method infinitely often(ie.,done is infinitely often true).Here we keep the conjunct-done to make the wrapper more intuitive. .Vol.1,No.1,Article.Publication date:January 2018

:20 Hongjin Liang and Xinyu Feng Our solution is to append an await command at the end of (6.3), so that the resulting code wrwfair PDF (await(B){C}) (see Fig. 7) may finish C but still be blocked at the end. Wrapper for PDF under strongly fair scheduling. Much of the effort to define wrwfair PDF (await(B){C}) is to allow the resulting code to be non-terminating even if B is eventually always true. We need to do the same to define wrsfair PDF (await(B){C}), but it is more challenging with strongly fair scheduling because await(¬done){} cannot be blocked under strongly fair scheduling if done is infinitely often true. Therefore we use while-loops in wrsfair PDF (await(B){C}) to allow the method to be delayed when done is infinitely often true2 . Note that while (done){} terminates when done is false. Wrappers for the state abstraction function. Since the program transformations by the wrappers introduce new object variables such as listid and done, we need to change the state abstraction function φ accordingly, which is defined as wr χ Prog (φ) in Fig. 7 (χ ∈ {sfair,wfair} and Prog ∈ {PSF,PDF}). More discussions. There could be different ways to define the wrappers to validate the Abstraction Theorem 6.2. We do not intend to claim that our definitions are the simplest ones (and it is unclear how to formally compare the complexity of different wrappers), but we would like to point out that, although some of the wrappers look complex, the complexity is partly due to the effort to have general wrappers that work for any atomic specifications in the form of await(B){C}. It is possible to have simpler wrappers for specific objects. For instance, the lock specification Γ in (2.3) defined in Sec. 2.2 can already serve as an abstraction for the test-and-set lock object Πtas (which is a PDF lock) under weakly fair scheduling, i.e., Πtas ⊑ wfair φ Γ holds. 7 PROGRAM LOGIC We extend the program logic LiLi [Liang and Feng 2016] to verify progress properties of concurrent objects with partial methods. LiLi is a rely-guarantee style program logic to verify linearizability and starvation-freedom/deadlock-freedom of concurrent objects. It establishes progress-aware contextual refinements between concrete object implementations and abstract (total) specifications. The key ideas of LiLi to verify progress are the following: • A thread can be blocked, relying on the actions of other threads (i.e., its environment) to make progress. To ensure it eventually progresses, we must guarantee that the environment actions that the thread waits for eventually occur. • To avoid circularity in rely-guarantee reasoning, each thread specifies a set of definite actions D, which are state transitions specified in the form of P ❀ Q. The thread guarantees that, whenever a definite action P ❀ Q is “enabled” (i.e., the assertion P holds), the transition must occur so that Q eventually holds, regardless of the environment behaviors. • A blocked thread must wait for a set of definite actions of other threads, and the size of the set must be decreasing (so that the thread is eventually unblocked). • A thread may delay the progress of others, i.e., to make other threads to execute more steps than they need when executed in isolation. To ensure deadlock-freedom, LiLi disallows a thread to be delayed infinitely often without whole system progress. This is achieved by using tokens as resources and each delaying action must consume a token. These ideas to reason about blocking and delay are general enough for verifying objects with partial methods, but we have to first generalize LiLi in the following two aspects: 2Actually the conjunct ¬done in the await condition in the wrapper could be removed, because the loop while (done){ } before the await block can already produce the non-terminating behaviors when other threads finish the method infinitely often (i.e., done is infinitely often true). Here we keep the conjunct ¬done to make the wrapper more intuitive. , Vol. 1, No. 1, Article . Publication date: January 2018