20:4 Hongjin Liang and Xinyu Feng L_initialize(){1 :=0; tkL_initialize(){owner :=0;next =0; L_acq(){ tkL_acq(){ 1 local b :false; 1 local i,o; 2 while(!b){b :cas(&1,0,cid); 2 i:=getAndInc(&next); 3 o :owner;while(i!=o){o :owner; } L_rel(){ 31:=0； tkL_rel(){ 4 owner :owner +1; (a)test-and-set lock implementation (c)ticket lock implementation inc(){L_acq();x:=x+1;L_rel(); inc_tkL(){tkL_acq();x:=x+1;tkL_rel(); (b)counter with a test-and-set lock (d)counter with a ticket lock INC()[x:=x+1;} (e)atomic spec.INC Fig.1.Counters with locks. In the rest of this paper,we first give an informal overview of the background and our key ideas in Sec.2.Then we introduce the object language in Sec.3,and linearizability and the basic contextual refinement in Sec.4.We propose our new progress properties in Sec.5,and give the progress-aware contextual refinement and the abstraction theorem in Sec.6.We present the logic in Sec.7 and show the examples we have verified in Sec.8.Finally,we discuss related work and conclude in Sec.9. 2 BACKGROUND AND OVERVIEW OF KEY IDEAS Below we first give an overview of linearizability,starvation-freedom,deadlock-freedom and contextual refinement.Then we analyze the problems in defining progress of concurrent objects with partial methods,and explain our solutions informally. 2.1 Background A concurrent object usually satisfies linearizability,a standard safety criterion,and certain progress property,describing when and how method calls of the object are guaranteed to terminate. Linearizability.A concurrent object is linearizable,if each method call appears to take effect instantaneously at some moment between its invocation and return [Herlihy and Wing 1990]. Intuitively,linearizability requires the implementation of each method to have the same effect as an atomic specification. Consider the two implementations of the counter object in Fig.1(b)and(d).We assume that every primitive command is executed atomically.A counter provides a method inc for incrementing the shared data x.Both implementations use locks to synchronize the increments.Intuitively they have the same effect as the atomic specification INC()in Fig.1(e),so they are linearizable. The locks themselves could also be viewed as standalone objects.For instance,the test-and-set lock object in Fig.1(a)provides the methods L_acq and L_rel for a thread to acquire and release Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018.20:4 Hongjin Liang and Xinyu Feng L_initialize(){ l := 0; } L_acq(){ 1 local b := false; 2 while(!b){ b := cas(&l, 0, cid); } } L_rel(){ 3 l := 0; } (a) test-and-set lock implementation inc(){ L_acq(); x:=x+1; L_rel(); } (b) counter with a test-and-set lock tkL_initialize(){ owner := 0; next := 0; } tkL_acq(){ 1 local i, o; 2 i := getAndInc(&next); 3 o := owner; while(i!=o){ o := owner; } } tkL_rel(){ 4 owner := owner + 1; } (c) ticket lock implementation inc_tkL(){ tkL_acq(); x:=x+1; tkL_rel(); } (d) counter with a ticket lock INC(){x:=x+1;} (e) atomic spec. INC Fig. 1. Counters with locks. In the rest of this paper, we first give an informal overview of the background and our key ideas in Sec. 2. Then we introduce the object language in Sec. 3, and linearizability and the basic contextual refinement in Sec. 4. We propose our new progress properties in Sec. 5, and give the progress-aware contextual refinement and the abstraction theorem in Sec. 6. We present the logic in Sec. 7 and show the examples we have verified in Sec. 8. Finally, we discuss related work and conclude in Sec. 9. 2 BACKGROUND AND OVERVIEW OF KEY IDEAS Below we first give an overview of linearizability, starvation-freedom, deadlock-freedom and contextual refinement. Then we analyze the problems in defining progress of concurrent objects with partial methods, and explain our solutions informally. 2.1 Background A concurrent object usually satisfies linearizability, a standard safety criterion, and certain progress property, describing when and how method calls of the object are guaranteed to terminate. Linearizability. A concurrent object is linearizable, if each method call appears to take effect instantaneously at some moment between its invocation and return [Herlihy and Wing 1990]. Intuitively, linearizability requires the implementation of each method to have the same effect as an atomic specification. Consider the two implementations of the counter object in Fig. 1(b) and (d). We assume that every primitive command is executed atomically. A counter provides a method inc for incrementing the shared data x. Both implementations use locks to synchronize the increments. Intuitively they have the same effect as the atomic specification INC() in Fig. 1(e), so they are linearizable. The locks themselves could also be viewed as standalone objects. For instance, the test-and-set lock object in Fig. 1(a) provides the methods L_acq and L_rel for a thread to acquire and release Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018