Progress of Concurrent Objects with Partial Methods 20:11 (C,(oc,o,K(0》二in(C,(o,6,x'》 K'=K{i*) 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...lcn.(co.K))=(AcAo) (et I im cn(e)det Iin C oK) (Ci.(ac.co.K(i)))-i.nabort (let ninn.(c))abort (a)program transitions Π(f)=(P,y,C)oo∈P E]se=nx∈dom(se)K=({yn,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,heho.l》eabo四 t.n abort k=(s1.x.C)[E]s =n se=sexn (E[return E](she)r) n(C,(s2,he,ooo》 K=(s1.x.C)[E]s:undefined (E[return E].((sc,hc).co.K))- (t,obj.abort) tn abort [E]se =n (E[print(E)](.h))) (E[skip ].((se.he).)) (C,(so世s,ho)》t(C',(s%世s,hg) dom(s1)=dom(sf) (C.ac)-(C,ac) (C,(oe,(so.hox,C》ob n(C%,(cc,(6,h。),(sxC》 (C,(ae,o,oj》飞c →tn(C,(o2,oo,o》 (C,(so sI,ho))-tabort (C,oc)-tabort (C,(oe,(so,ho),(s1,x,C1)) (任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 Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods 20: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 Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018
20: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(e2))to represent that e is in the form of (t,f,n)(or (t,ret,n)). Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018
20: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)). Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018