Progress of Concurrent Objects with Partial Methods（Extended Version）

:26 Hongjin Liang and Xinyu Feng lock些35.lock,lock些(1=L=s) L_acq(){ lock arem(L_ACQ') unlocked芒locko local b :false; locked些t.lockedByt ((-b)A lock AA arem(L_ACQ')) lockedBy:些lock(t≠0) V(b A lockedBycid A arem(skip)) 2 while (!b){ R当VvaGr Gt曾Acg VRel |(unlocked A◆)v(locked A◆A) A arem(LACQ')】 Acq unlocked lockedBy: 3 b :cas(&1,0,cid); Rel lockedBy unlocked D些falsetrue lockedBycid A arem(skip) J些lock L_rel(){ Q些unlocked lockedBycid A arem(L_REL) 5 1:=0; ∫1ifg=locked f©)={0fg上Q {lock A arem(skip)》 Fig.11.Proofs for the test-and-set lock. method.The definite action D for this object can be defined as false true,saying that there is no definite action that a thread needs to complete. The action Acqt(corresponding to the successful cas at line 3)is a delaying action(defined with level 1).When thread t succeeds in cas,termination of other threads'L_acq can be delayed,as allowed by PDF.The thread t has to pay a -token,given in the precondition of L_acq. The definite progress condition(R.G:D(,L=0))now says that thread t is either at a state that it itself can progress(i.e.,O holds),or blocked at the abstract level(i.e.,L=0 does not hold) The metric f()decreases when an environment thread releases L,but can be reset(which means thread t is delayed)if an environment thread successfully acquires the lock. By the Soundness Theorem 7.3,we know the test-and-set lock object satisfies the PDF property, and contextually refines the abstraction generated by the corresponding PDF wrappers in Fig.7, under strongly and weakly fair scheduling. 8.2 Ticket Locks In Fig.12,we prove the ticket lock object satisfies PSF.We introduce some write-only auxiliary variables to help the verification.First,we introduce an array ticket to help specify the queue of the threads requesting the lock.Each array cell ticket[i]records the ID of the unique thread getting the ticket number i(see line 2).Second,we introduce a lock bit l to make the lock acquirement and lock release explicit (see lines 4 and 5). We then define the object invariant lock(s,tl,n,n2).It says that the lock bits 1 and L are equal, n and n2 are the values of owner and next respectively,and tl is the list of the threads recorded in ticket[n],ticket[n +1],...,ticket[n-1](as specified by tickets(tl,n,n2)). The guarantee condition G:describes the possible atomic actions of thread t.Req:adds t at the end of tl of the threads requesting the lock and also increments next.It corresponds to line 2 in the code at the top of Fig.12.Acq:sets the lock bits to t,explicitly indicating the lock acquirement(see line 4).It is also a definite action(see the definition of D)since thread t must acquire the lock if its loop at line 3 terminates.Relt increments owner to dequeue the thread t which currently holds the lock,and resets the lock bits(see line 5).All actions are at level 0.There are no delaying actions. Vol.1,No.1,Article.Publication date:January 2018

:26 Hongjin Liang and Xinyu Feng lock def = ∃s. locks locks def = (l = L = s) unlocked def = lock0 locked def = ∃t. lockedByt lockedByt def = lockt ∧ (t , 0) Rt def = W t ′,t Gt ′ Gt def = Acqt ∨ Relt Acqt def = unlocked n1 lockedByt Relt def = lockedByt n0 unlocked D def = false ❀ true J def = lock Q def = unlocked f (S) = ( 1 if S |= locked 0 if S |= Q L_acq(){ ( lock ∧  ∧ arem(L_ACQ’) ) 1 local b := false; ( ((¬b) ∧ lock ∧  ∧ ♦ ∧ arem(L_ACQ’)) ∨ (b ∧ lockedBycid ∧ arem(skip))) 2 while (!b) { ( ((unlocked ∧ ) ∨ (locked ∧  ∧ ♦)) ∧ arem(L_ACQ’) ) 3 b := cas(&l, 0, cid); 4 } ( lockedBycid ∧ arem(skip) ) } L_rel(){ ( lockedBycid ∧ arem(L_REL) ) 5 l := 0; ( lock ∧ arem(skip) ) } Fig. 11. Proofs for the test-and-set lock. method. The definite action D for this object can be defined as false ❀ true, saying that there is no definite action that a thread needs to complete. The action Acqt (corresponding to the successful cas at line 3) is a delaying action (defined with level 1). When thread t succeeds in cas, termination of other threads’ L_acq can be delayed, as allowed by PDF. The thread t has to pay a -token, given in the precondition of L_acq. The definite progress condition (R,G : D f −→(Q, L=0)) now says that thread t is either at a state that it itself can progress (i.e., Q holds), or blocked at the abstract level (i.e., L=0 does not hold). The metric ft (S) decreases when an environment thread releases L, but can be reset (which means thread t is delayed) if an environment thread successfully acquires the lock. By the Soundness Theorem 7.3, we know the test-and-set lock object satisfies the PDF property, and contextually refines the abstraction generated by the corresponding PDF wrappers in Fig. 7, under strongly and weakly fair scheduling. 8.2 Ticket Locks In Fig. 12, we prove the ticket lock object satisfies PSF. We introduce some write-only auxiliary variables to help the verification. First, we introduce an array ticket to help specify the queue of the threads requesting the lock. Each array cell ticket[i] records the ID of the unique thread getting the ticket number i (see line 2). Second, we introduce a lock bit l to make the lock acquirement and lock release explicit (see lines 4 and 5). We then define the object invariant lock(s,tl,n1,n2). It says that the lock bits l and L are equal, n1 and n2 are the values of owner and next respectively, and tl is the list of the threads recorded in ticket[n1], ticket[n1 + 1], . . . , ticket[n2 − 1] (as specified by tickets(tl,n1,n2)). The guarantee condition Gt describes the possible atomic actions of thread t. Reqt adds t at the end of tl of the threads requesting the lock and also increments next. It corresponds to line 2 in the code at the top of Fig. 12. Acqt sets the lock bits to t, explicitly indicating the lock acquirement (see line 4). It is also a definite action (see the definition of Dt ) since thread t must acquire the lock if its loop at line 3 terminates. Relt increments owner to dequeue the thread t which currently holds the lock, and resets the lock bits (see line 5). All actions are at level 0. There are no delaying actions. , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) 27 tkL_acq(){ tkL_rel({ 1 local i,o; 5 <owner :owner+1;1 :=0>; 2 <i :getAndInc(&next);ticket[i]:=cid>; 2 3 o :=owner;while (i !o){o :owner; 41:=cid; lock(,stlnu,n2)些 (1=L=sA (s head(tl)vs=0))+((owner n1)+(next n2)A (n1 n2))+tickets(tI,n1,n2) G,些Reg VAcg V Rel4 D Vtl,m,n2.lock(0.t:tlm.n)lock(t.t:tln,n2) Reqt,tl.m.n.lock(s.tlm.n)lock(s,t]1) Acqm.lock(0.tm)lock(t.t) Rel.lock(t.t:tlm)lock(0,tlm+1,n) ,mn tht.tlocked(s.mn(om) 兰3n2,k.lock(..t:,i2Ao≤i)f©)={2+1rsf_gmr=0 ifg乍(i-owner=k)*(1≠0) Fig.12.Proofs for the ticket lock(with auxiliary code in gray). By applying the wHL rule of our logic,we need to prove the definite progress conditionJ (R,ld:D(,L=0))for the loop at line 3.Here J,O and f are defined at the bottom of Fig.12. In the definition of,we use tlockedt(s,n,i,n)to say that t is requesting the lock and its ticket number is i.Here th is the list of the threads which are waiting ahead of t,and tl2 is for the threads behind t.Ot specifies the case when th is empty.In this case the lock bits must be 0 and tlocked is reduced to lock,as shown at the bottom of Fig.12. The metric f()is determined by the number of threads ahead of t in the waiting queue and the status of the lock bits.It decreases when an environment thread t'does the definite action D, setting the lock bits to t'.It also decreases when t'releases the lock and increments owner,turning (L0)to (L=0).Thus we can proveJ=(R,Id:D (Q,L=0)). By the Soundness Theorem 7.3,we know the ticket lock object satisfies the PSF property,and contextually refines the abstraction generated by the corresponding PSF wrappers,under both strongly and weakly fair scheduling.The detailed formal proofs are given in Appendix C.1. 8.3 Simple PSF Locks with Await Blocks Figure 13 shows the proofs of a simple lock object implemented with an await statement which guarantees PSF under weak fairness.The acquire method is simply wr(await(10)(1:=cid). The release method resets the lock bit l directly.It has the annotated precondition(1=cid).We still verify the object in our logic with the specifications L_ACQ'and L_REL defined in(2.3). We first define the object invariant P used in the oBj rule.It is defined based on lock,which requires l to have the same value as the abstract lock L.The queue listid records the threads currently waiting for the lock.Here diff(tb)says that the threads in tb are all different.Then the object invariant P further requires that the current thread t is not recorded in listid.It is preserved before and after t calls a method. The object has three kinds of possible actions(see the definition of G).Reqt appends the thread t at the end of listid to request the lock(line 1).Acqt acquires the lock if the lock is available and Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :27 tkL_acq(){ 1 local i, o; 2 <i := getAndInc(&next); ticket[i] := cid >; 3 o := owner; while (i != o) { o := owner; } 4 l := cid; } tkL_rel(){ 5 <owner := owner+1; l := 0 >; } lock(s,tl,n1,n2) def = (l = L = s ∧ (s = head(tl) ∨ s = 0)) ∗ ((owner = n1) ∗ (next = n2) ∧ (n1 ≤ n2)) ∗ tickets(tl,n1,n2) Gt def = Reqt ∨ Acqt ∨ Relt Dt def = ∀tl,n1,n2. lock(0,t::tl,n1,n2) ❀ lock(t,t::tl,n1,n2) Reqt def = ∃s,tl,n1,n2. lock(s,tl,n1,n2) n lock(s,tl++[t],n1,n2 + 1) Acqt def = ∃tl,n1,n2. lock(0,t::tl,n1,n2) n lock(t,t::tl,n1,n2) Relt def = ∃tl,n1,n2. lock(t,t::tl,n1,n2) n lock(0,tl,n1 + 1,n2) Jt def = ∃s,n1,n2,tl1,tl2. tlockedtl1,t,tl2 (s,n1,i,n2) ∧ (o ≤ n1) Qt def = ∃n2,tl2. lock(0,t::tl2,i,n2) ∧ (o ≤ i) f (S) = ( 2k + 1 if S |= (i − owner = k) ∗ (l = 0) 2k if S |= (i − owner = k) ∗ (l , 0) Fig. 12. Proofs for the ticket lock (with auxiliary code in gray). By applying the whl rule of our logic, we need to prove the definite progress condition J ⇒ (R,Id : D f −→ (Q, L=0)) for the loop at line 3. Here J, Q and f are defined at the bottom of Fig. 12. In the definition of Jt , we use tlockedtl1,t,tl2 (s,n1,i,n2) to say that t is requesting the lock and its ticket number is i. Here tl1 is the list of the threads which are waiting ahead of t, and tl2 is for the threads behind t. Qt specifies the case when tl1 is empty. In this case the lock bits must be 0 and tlocked is reduced to lock, as shown at the bottom of Fig. 12. The metric ft (S) is determined by the number of threads ahead of t in the waiting queue and the status of the lock bits. It decreases when an environment thread t ′ does the definite action Dt ′, setting the lock bits to t ′ . It also decreases when t ′ releases the lock and increments owner, turning (L , 0) to (L = 0). Thus we can prove J ⇒ (R,Id: D f −→(Q, L=0)). By the Soundness Theorem 7.3, we know the ticket lock object satisfies the PSF property, and contextually refines the abstraction generated by the corresponding PSF wrappers, under both strongly and weakly fair scheduling. The detailed formal proofs are given in Appendix C.1. 8.3 Simple PSF Locks with Await Blocks Figure 13 shows the proofs of a simple lock object implemented with an await statement which guarantees PSF under weak fairness. The acquire method is simply wrwfair PSF (await(l=0){l:=cid}). The release method resets the lock bit l directly. It has the annotated precondition (l = cid). We still verify the object in our logic with the specifications L_ACQ' and L_REL defined in (2.3). We first define the object invariant P used in the obj rule. It is defined based on lock, which requires l to have the same value as the abstract lock L. The queue listid records the threads currently waiting for the lock. Here diff(tb) says that the threads in tb are all different. Then the object invariant Pt further requires that the current thread t is not recorded in listid. It is preserved before and after t calls a method. The object has three kinds of possible actions (see the definition of G). Reqt appends the thread t at the end of listid to request the lock (line 1). Acqt acquires the lock if the lock is available and , Vol. 1, No. 1, Article . Publication date: January 2018

:28 Hongjin Liang and Xinyu Feng B些s,th.locks(tb)At生tb)where tb=e|(化，1=0')：tb lock(tb)些(Q=L=s)*(listid=t)间Adif(tb) unlocked(tb)locko(tb) lockReqt兰3s,tb.lock(tb)A(t∈tb locked(tb兰lock(tb)A(t≠0)A(ttb)lockedt些th.lockedt(tb Gt些Reg VAcq V Rel4 DVtb.unlocked((t.=0)::tb)locked (b) Reg ,tb.(locks(tb)()locks(b+[(t.)) Acq.unlocked((t.))lockedt(tb)Relb.lockedt (b)unlocked(tb) f©)些{2+1f3,6地，(E上ock,(他H[61=o】+b)As≠0)A=k 12k if 3tb,tb'.unlocked(tb++[(t,'1=0')]++tb))A ltbl =k acquire(){ release(){ Peid A arem(L_ACQ') lockedcid A arem(L_REL) listid :listid ++[(cid,'1=0')]; 1:=0; lockReqeid A arem(L_ACQ') Peid A arem(skip) 2 await (1=0/\cid enhd(listid)){ 3tb.unlocked((cid,'1=0')::tb)A arem(L_ACQ') 3 1 cid;listid listid cid; 3tb.lockedcid(tb)A arem(skip) lockedcid A arem(skip) Fig.13.Proofs for the simple PSF lock under weak fairness. t is at the head of listid (lines 2-4).Relt releases the lock (line 5).Here Acq,is also the definite action of thread t(see the definition of D).None of the actions are delaying actions. To verify the await statement at lines 2-4,we apply the AwArr-w rule in Fig.10,and prove: lockReq(R:Do(1=0Acid enhd(listid),L=0)). (8.1) The metric f is defined at the top of Fig.13.We can see that f()decreases when an environment thread t'performs a definite action,since D will remove t'that is waiting ahead of the thread t. Also fi()decreases when t'releases the lock,turning (L#0)to (L=0).Thus(8.1)holds. By the Soundness Theorem 7.3,we know this simple lock satisfies PSF under weak fairness. 9 RELATED WORK AND CONCLUSION There has been much work on the relationships between linearizability,progress properties and contextual refinement (e.g.,[Filipovic et al.2009;Gotsman and Yang 2011,2012;Liang et al.2013]), and on verifying progress properties or progress-aware refinement (e.g.,[Bostrom and Muller 2015; da Rocha Pinto et al.2016;Gotsman et al.2009:Hoffmann et al.2013:Jacobs et al.2015:Tassarotti et al.2017]).But none of them studies objects with partial methods as we do.On the other hand,our ideas might be general enough to be integrated with these verification methods to support blocking primitives and partial methods.For instance,Tassarotti et al.[2017]propose a higher-order logic based on Iris [Jung et al.2015]for fair refinements.Our wrappers and reasoning method may be applied there to support higher-order refinement reasoning with blocking primitives.The logic by Bostrom and Muller [2015]ensures that no thread will be blocked forever.It supports special built-in blocking primitives for locking,message passing and thread join.Their obligation-based Vol.1,No.1,Article.Publication date:January 2018

:28 Hongjin Liang and Xinyu Feng Pt def = ∃s,tb. locks (tb) ∧ (t < tb) where tb ::= ϵ | (t,‘l=0’) ::tb locks (tb) def = (l = L = s) ∗ (listid = tb) ∧ diff(tb) unlocked(tb) def = lock0 (tb) lockReqt def = ∃s,tb. locks (tb) ∧ (t ∈ tb) lockedt (tb) def = lockt (tb) ∧ (t , 0) ∧ (t < tb) lockedt def = ∃tb. lockedt (tb) Gt def = Reqt ∨ Acqt ∨ Relt Dt def = ∀tb. unlocked((t,‘l=0’) ::tb) ❀ lockedt (tb) Reqt def = ∃s,tb. (locks (tb) ∧ (t < tb)) n locks (tb ++ [(t,‘l=0’)]) Acqt def = ∃tb. unlocked((t,‘l=0’) ::tb) n lockedt (tb) Relt def = ∃tb. lockedt (tb) n unlocked(tb) ft (S) def = ( 2k + 1 if ∃s,tb,tb′ . (S |= locks (tb ++ [(t,‘l=0’)] ++ tb′ ) ∧ s , 0) ∧ |tb| = k 2k if ∃tb,tb′ . (S |= unlocked(tb ++ [(t,‘l=0’)] ++ tb′ )) ∧ |tb| = k acquire(){ ( Pcid ∧ arem(L_ACQ’) ) 1 listid := listid ++ [(cid, 'l=0')]; ( lockReqcid ∧ arem(L_ACQ’) ) 2 await (l = 0 /\ cid = enhd(listid)) { ( ∃tb. unlocked((cid,‘l=0’) ::tb) ∧ arem(L_ACQ’) ) 3 l := cid; listid := listid \ cid; ( ∃tb. lockedcid(tb) ∧ arem(skip) ) 4 } ( lockedcid ∧ arem(skip) ) } release(){ ( lockedcid ∧ arem(L_REL) ) 5 l := 0; ( Pcid ∧ arem(skip) ) } Fig. 13. Proofs for the simple PSF lock under weak fairness. t is at the head of listid (lines 2-4). Relt releases the lock (line 5). Here Acqt is also the definite action of thread t (see the definition of D). None of the actions are delaying actions. To verify the await statement at lines 2-4, we apply the await-w rule in Fig. 10, and prove: lockReq ⇒ (R : D◦ f −→(l = 0 ∧ cid = enhd(listid), L = 0)) . (8.1) The metric f is defined at the top of Fig. 13. We can see that ft (S) decreases when an environment thread t ′ performs a definite action, since Dt ′ will remove t ′ that is waiting ahead of the thread t. Also ft (S) decreases when t ′ releases the lock, turning (L , 0) to (L = 0). Thus (8.1) holds. By the Soundness Theorem 7.3, we know this simple lock satisfies PSF under weak fairness. 9 RELATED WORK AND CONCLUSION There has been much work on the relationships between linearizability, progress properties and contextual refinement (e.g., [Filipović et al. 2009; Gotsman and Yang 2011, 2012; Liang et al. 2013]), and on verifying progress properties or progress-aware refinement (e.g., [Boström and Müller 2015; da Rocha Pinto et al. 2016; Gotsman et al. 2009; Hoffmann et al. 2013; Jacobs et al. 2015; Tassarotti et al. 2017]). But none of them studies objects with partial methods as we do. On the other hand, our ideas might be general enough to be integrated with these verification methods to support blocking primitives and partial methods. For instance, Tassarotti et al. [2017] propose a higher-order logic based on Iris [Jung et al. 2015] for fair refinements. Our wrappers and reasoning method may be applied there to support higher-order refinement reasoning with blocking primitives. The logic by Boström and Müller [2015] ensures that no thread will be blocked forever. It supports special built-in blocking primitives for locking, message passing and thread join. Their obligation-based , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) 29 reasoning strategies may be applied to await blocks too,to verify that the client threads of await will not be permanently blocked. In our previous work we propose the program logic LiLi [Liang and Feng 2016]to verify starvation- free and deadlock-free objects.This work is inspired by several ideas from LiLi: The soundness of LiLi ensures a progress-aware contextual refinement,which gives starvation- freedom or deadlock-freedom,if fed with different abstractions generated by specific code wrappers.Here we take a similar approach,and define new wrappers to generate abstractions for PSF and PDF objects. LiLi sorts progress properties in two dimensions called blocking and delay,and distinguish starvation-freedom and deadlock-freedom by whether delay is permitted.Here the difference between our PSF and PDF also lies in the delay dimension. The program logic proposed in this paper is a generalization of LiLi.Both logics use tokens to support delay,and use similar definite progress conditions to support blocking. However,there are two main problems with LiLi,which are addressed in this paper: LiLi does not provide abstractions for objects with partial methods.When using LiLi to verify lock-based algorithms(such as the counters shown in Fig.1(b)and (d)in this paper),one has to inline the implementations of locks,losing the modularity of verification.Here we define progress-aware abstractions for objects with partial methods,allowing us to verify their clients in a modular way. The inference rules of LiLi do not apply to objects with partial methods,such as the objects in Sec.8 in this paper.We have explained the reasons and our solutions in Sec.7. Schellhorn et al.[2016]propose a proof method for verifying starvation-freedom.Their approach is based on a special predicate which describes the waiting-for relations among the threads.However, their work has similar problems as LiLi,and cannot apply to the examples considered in this paper Gu et al.[2016]verify progress of the ticket lock implementation as part of their verified kernel. Their specification of the lock relies on the behaviors of clients.It requires that the client owning a lock must eventually release it.Then they prove that the acquire method always terminates with the cooperative clients.It is unclear how the approach can be applied for general objects with partial methods. Conclusions and more discussions.We have studied the progress of objects with partial methods in three aspects.First,we define new progress properties,partial starvation-freedom(PSF)and partial deadlock-freedom(PDF).Second,we design wrappers to generate abstractions for PSF and PDF objects under strongly or weakly fair scheduling.Third,we develop a program logic to verify PSF and PDF. Although our program logic verifies both linearizability and progress properties,it is focused more on the latter.Existing work [Khyzha et al.2017;Liang and Feng 2013;Turon et al.2013]has shown that linearizability itself can be challenging to verify,and special mechanisms are needed for very fine-grained objects with non-fixed linearization points(LPs).Our logic cannot verify these objects,but our conjecture is that the mechanisms handling non-fixed LPs(as in [Liang and Feng 2013])are orthogonal to our progress reasoning,and they can be integrated into our logic if needed. The logic follows LiLi's ideas of definite actions and stratified tokens to reason about progress. They can be viewed as special strategies implementing the general principle for termination reasoning,that is to find a well-founded metric that keeps decreasing during the program execution. These ideas and rules give a concrete guide to users on how to construct the metric and the proofs. Although we have tried to make them as general as possible,and they have been shown applicable to many non-trivial algorithms(see [Liang and Feng 2016]and Appendix C),they may not be Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :29 reasoning strategies may be applied to await blocks too, to verify that the client threads of await will not be permanently blocked. In our previous work we propose the program logic LiLi [Liang and Feng 2016] to verify starvation￾free and deadlock-free objects. This work is inspired by several ideas from LiLi: • The soundness of LiLi ensures a progress-aware contextual refinement, which gives starvation￾freedom or deadlock-freedom, if fed with different abstractions generated by specific code wrappers. Here we take a similar approach, and define new wrappers to generate abstractions for PSF and PDF objects. • LiLi sorts progress properties in two dimensions called blocking and delay, and distinguish starvation-freedom and deadlock-freedom by whether delay is permitted. Here the difference between our PSF and PDF also lies in the delay dimension. • The program logic proposed in this paper is a generalization of LiLi. Both logics use tokens to support delay, and use similar definite progress conditions to support blocking. However, there are two main problems with LiLi, which are addressed in this paper: • LiLi does not provide abstractions for objects with partial methods. When using LiLi to verify lock-based algorithms (such as the counters shown in Fig. 1(b) and (d) in this paper), one has to inline the implementations of locks, losing the modularity of verification. Here we define progress-aware abstractions for objects with partial methods, allowing us to verify their clients in a modular way. • The inference rules of LiLi do not apply to objects with partial methods, such as the objects in Sec. 8 in this paper. We have explained the reasons and our solutions in Sec. 7. Schellhorn et al. [2016] propose a proof method for verifying starvation-freedom. Their approach is based on a special predicate which describes the waiting-for relations among the threads. However, their work has similar problems as LiLi, and cannot apply to the examples considered in this paper. Gu et al. [2016] verify progress of the ticket lock implementation as part of their verified kernel. Their specification of the lock relies on the behaviors of clients. It requires that the client owning a lock must eventually release it. Then they prove that the acquire method always terminates with the cooperative clients. It is unclear how the approach can be applied for general objects with partial methods. Conclusions and more discussions. We have studied the progress of objects with partial methods in three aspects. First, we define new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). Second, we design wrappers to generate abstractions for PSF and PDF objects under strongly or weakly fair scheduling. Third, we develop a program logic to verify PSF and PDF. Although our program logic verifies both linearizability and progress properties, it is focused more on the latter. Existing work [Khyzha et al. 2017; Liang and Feng 2013; Turon et al. 2013] has shown that linearizability itself can be challenging to verify, and special mechanisms are needed for very fine-grained objects with non-fixed linearization points (LPs). Our logic cannot verify these objects, but our conjecture is that the mechanisms handling non-fixed LPs (as in [Liang and Feng 2013]) are orthogonal to our progress reasoning, and they can be integrated into our logic if needed. The logic follows LiLi’s ideas of definite actions and stratified tokens to reason about progress. They can be viewed as special strategies implementing the general principle for termination reasoning, that is to find a well-founded metric that keeps decreasing during the program execution. These ideas and rules give a concrete guide to users on how to construct the metric and the proofs. Although we have tried to make them as general as possible, and they have been shown applicable to many non-trivial algorithms (see [Liang and Feng 2016] and Appendix C), they may not be , Vol. 1, No. 1, Article . Publication date: January 2018

30 Hongjin Liang and Xinyu Feng complete and it would be unsurprising if there are examples that they cannot handle.As future work,we would like to verify more examples to explore the scope of the applicability. The specifications of linearizable objects must be atomic,but sometimes we may want to give non-atomic specifications to object methods.We can apply our wrappers to every occurrence of the await blocks in the non-atomic specifications to establish progress-aware refinements.We suspect that our logic can still be used to verify such refinements(as in [Liang et al.2014]).Another potential limitation may be due to the use of the pure Boolean expression B in await(B)(C),which may limit the expressiveness of the specifications.However,our technical development does not rely on this setting.Everything may still hold if we replace B with the more expressive state assertions. Other interesting future work includes automating the verification process.One of the key problems is to infer the definite actions and prove the definite progress conditions.There have been efforts to synthesize the ranking functions for loop termination(see [Cook et al.2011]for an overview),which may provide insights for automating the definite progress proofs.In addition we might be able to follow the ideas in automated rely-guarantee reasoning (e.g.,[Calcagno et al. 2007])to automate the verification in our rely-guarantee logic. ACKNOWLEDGMENTS We would like to thank anonymous referees for their suggestions and comments on earlier versions of this paper.This work is supported in part by grants from National Natural Science Foundation of China(NSFC)under Grant Nos.61379039,61502442 and 61632005. REFERENCES Pontus Bostrom and Peter Muller.2015.Modular Verification of Finite Blocking in Non-terminating Programs.In Proceedings of the 29th European Conference on Object-Oriented Programming(ECOOP 2015).639-663. Cristiano Calcagno,Matthew J.Parkinson,and Viktor Vafeiadis.2007.Modular Safety Checking for Fine-Grained Concur- rency.In Proceedings of the 14th International Symposium on Static Analysis(SAS 2007).233-248. Byron Cook,Andreas Podelski,and Andrey Rybalchenko.2011.Proving Program Termination.Commun.ACM 54,5(2011). 88-98. Pedro da Rocha Pinto,Thomas Dinsdale-Young.Philippa Gardner,and Julian Sutherland 2016.Modular Termination Verification for Non-blocking Concurrency.In Proceedings of the 25th European Symposium on Programming Languages and Systems(ESOP 2016).176-201. Xinyu Feng.2009.Local rely-guarantee reasoning.In POPL.315-327. Ivana Filipovic,Peter O'Hearn,Noam Rinetzky,and Hongseok Yang.2009.Abstraction for Concurrent Objects.In Proceedings of the 18th European Symposium on Programming(ESOP 2009).252-266. Alexey Gotsman,Byron Cook,Matthew J.Parkinson,and Viktor Vafeiadis.2009.Proving that Non-Blocking Algorithms Don't Block.In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages P0PL2009).16-28. Alexey Gotsman and Hongseok Yang.2011.Liveness-Preserving Atomicity Abstraction.In Proceedings of the 38th Interna- tional Conference on Automata,Languages and Programming (ICALP 2011).453-465. Alexey Gotsman and Hongseok Yang.2012.Linearizability with Ownership Transfer.In Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR 2012).256-271. Ronghui Gu,Zhong Shao,Hao Chen,Xiongnan(Newman)Wu,Jieung Kim,Vilhelm Sjoberg.and David Costanzo.2016. CertiKOS:An Extensible Architecture for Building Certified Concurrent OS Kernels.In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation(OSDI 2016).653-669. Maurice Herlihy and Nir Shavit.2008.The Art of Multiprocessor Programming.Morgan Kaufmann Maurice Herlihy and Nir Shavit.2011.On the Nature of Progress.In Proceedings of the 15th International Conference on Principles of Distributed Systems (OPODIS 2011).313-328. Maurice Herlihy and Jeannette Wing.1990.Linearizability:A Correctness Condition for Concurrent Objects.ACM Trans. Program.Lang.Syst.12.3(1990).463-492. Jan Hoffmann,Michael Marmar,and Zhong Shao.2013.Quantitative Reasoning for Proving Lock-Freedom.In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science(LICS 2013).124-133. Bart Jacobs,Dragan Bosnacki,and Ruurd Kuiper.2015.Modular Termination Verification.In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015).664-688. Vol.1,No.1,Article.Publication date:January 2018

:30 Hongjin Liang and Xinyu Feng complete and it would be unsurprising if there are examples that they cannot handle. As future work, we would like to verify more examples to explore the scope of the applicability. The specifications of linearizable objects must be atomic, but sometimes we may want to give non-atomic specifications to object methods. We can apply our wrappers to every occurrence of the await blocks in the non-atomic specifications to establish progress-aware refinements. We suspect that our logic can still be used to verify such refinements (as in [Liang et al. 2014]). Another potential limitation may be due to the use of the pure Boolean expression B in await(B){C}, which may limit the expressiveness of the specifications. However, our technical development does not rely on this setting. Everything may still hold if we replace B with the more expressive state assertions. Other interesting future work includes automating the verification process. One of the key problems is to infer the definite actions and prove the definite progress conditions. There have been efforts to synthesize the ranking functions for loop termination (see [Cook et al. 2011] for an overview), which may provide insights for automating the definite progress proofs. In addition we might be able to follow the ideas in automated rely-guarantee reasoning (e.g., [Calcagno et al. 2007]) to automate the verification in our rely-guarantee logic. ACKNOWLEDGMENTS We would like to thank anonymous referees for their suggestions and comments on earlier versions of this paper. This work is supported in part by grants from National Natural Science Foundation of China (NSFC) under Grant Nos. 61379039, 61502442 and 61632005. REFERENCES Pontus Boström and Peter Müller. 2015. Modular Verification of Finite Blocking in Non-terminating Programs. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 639–663. Cristiano Calcagno, Matthew J. Parkinson, and Viktor Vafeiadis. 2007. Modular Safety Checking for Fine-Grained Concur￾rency. In Proceedings of the 14th International Symposium on Static Analysis (SAS 2007). 233–248. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving Program Termination. Commun. ACM 54, 5 (2011), 88–98. Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular Termination Verification for Non-blocking Concurrency. In Proceedings of the 25th European Symposium on Programming Languages and Systems (ESOP 2016). 176–201. Xinyu Feng. 2009. Local rely-guarantee reasoning. In POPL. 315–327. Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. 2009. Abstraction for Concurrent Objects. In Proceedings of the 18th European Symposium on Programming (ESOP 2009). 252–266. Alexey Gotsman, Byron Cook, Matthew J. Parkinson, and Viktor Vafeiadis. 2009. Proving that Non-Blocking Algorithms Don’t Block. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009). 16–28. Alexey Gotsman and Hongseok Yang. 2011. Liveness-Preserving Atomicity Abstraction. In Proceedings of the 38th Interna￾tional Conference on Automata, Languages and Programming (ICALP 2011). 453–465. Alexey Gotsman and Hongseok Yang. 2012. Linearizability with Ownership Transfer. In Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR 2012). 256–271. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI 2016). 653–669. Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann. Maurice Herlihy and Nir Shavit. 2011. On the Nature of Progress. In Proceedings of the 15th International Conference on Principles of Distributed Systems (OPODIS 2011). 313–328. Maurice Herlihy and Jeannette Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492. Jan Hoffmann, Michael Marmar, and Zhong Shao. 2013. Quantitative Reasoning for Proving Lock-Freedom. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013). 124–133. Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. 2015. Modular Termination Verification. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 664–688. , Vol. 1, No. 1, Article . Publication date: January 2018