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