20:10 Hongjin Liang and Xinyu Feng (ThrdID) E Nat (Store) 5,s PVar-Val (Heap) h,h∈ Nat-Val (Data) 0,∑ =(s,h) (CallStk) K.k = oI(sI,x,C) (ThrdPool) K,区 = {t1K1,,tn→Kn} (PState) S,S = (Gc,Go,K) (LState) s,6 = (oc,0o,) (ExecCtxt) E = []I E;C (Pre) 乎(Data) (AbsFun) ∈Data凵Datd (Event)e ::=(t,f,n)(t,ret,n)I (t,obj)I (t,obj.abort)I (t,out,n) I(t,clt)I(t.clt,abort)(t,term)|(spawn,n) (BldSet)△ (PEvent)t=(e,△c,△o) (ETrace) ::=eIe:8 (co-inductive) (PTrace)T :=E I::T (co-inductive) en(C)B if 3E.C'.C=E[await(B)(C] true otherwise (ao,x)B iff [B](oo-swx.s》=true Ak≠o e B iff [B]ac.s true btids(let IIinCll.…lCn,(oc,oo,K)》些(tlK()=oA-(ce卡en(Ch, {tIK(t)≠oA-(oo,K(t)上en(Ct)) Fig.3.States and event traces. We make the following assumptions to simplify the technical setting.There are no regular function calls in either clients or objects.Therefore x:=f(E)can only be executed in client code to call object methods,and return E always returns from object methods to clients.Each object method takes only one argument and each method body ends with a return command.Object methods never execute the print(E)command and therefore do not generate external events.The command C in await(B)(C)cannot contain await,print,and method calls and returns.It cannot contain loops either so that it always terminates. Operational semantics.The operational semantics rules shown in Fig.4 consist of three parts, including state transitions made by the whole program,by individual threads,and by clients or object methods,respectively.We define program states S in Fig.3,where we use two sets of notations to represent states at the concrete and the abstract levels respectively when we study refinement.To ensure that the client code does not touch the object data,in S we separate the data accessed by clients(oc)and by object methods (oo).S also contains a thread pool K mapping thread IDs t to the corresponding method call stacks k.Recall that the only function call allowed in the language is the method invocation made by a client and there are no nested function calls, therefore each k is either empty(o,which means the thread is executing the client code),or contains only one stack frame(sI,x,C),where s is the local store for the local variables of the method,x is the(client)variable recording the return value,and C is the continuation(the remaining client code to be executed after the return of the method). Figure 4(a)shows that the execution of the program W follows the non-deterministic interleaving semantics,which is defined based on thread transitions defined in Fig.4(b).Each transition over program configurations is labelled with a program event t,a triple in the form of(e,Ac,Ao).The event e is generated by thread transitions.As defined in Fig.3,(t,f,n)records the invocation of the method f with the argument n in the thread t,and(t,ret,n)is for a method return with the return value n.(t,obj)and(t,clt)record a regular object step and a regular client step respectively, while(t,obj,abort)and(t,clt,abort)are for aborting of the thread in the object and client code Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018.20:10 Hongjin Liang and Xinyu Feng (ThrdID) t ∈ Nat (Store) s,s ∈ PVar ⇀ Val (Heap) h,h ∈ Nat ⇀ Val (Data) σ,Σ ::= (s,h) (CallStk) κ,k ::= ◦ | (sl ,x,C) (ThrdPool) K ,K ::= {t1 ❀ κ1,. . . ,tn ❀ κn } (PState) S,S ::= (σc ,σo ,K ) (LState) ς,δ ::= (σc ,σo ,κ) (ExecCtxt) E ::= [ ] | E;C (Pre) P ∈ P(Data) (AbsFun) φ ∈ Data ⇀ Data (Event) e ::= (t, f ,n) | (t,ret,n) | (t,obj) | (t,obj,abort) | (t,out,n) | (t,clt) | (t,clt,abort) | (t,term) | (spawn,n) (BIdSet) ∆ ∈ P(ThrdID) (PEvent) ι ::= (e,∆c ,∆o ) (ETrace) E ::= ϵ | e ::E (co-inductive) (PTrace) T ::= ϵ | ι ::T (co-inductive) en(Cˆ) def = ( B if ∃E,C ′ . Cˆ = E[await(B){C ′ }] true otherwise (σo ,κ) |= B iff JBK((σo .s)⊎(κ.sl )) = true ∧ κ , ◦ σc |= B iff JBKσc .s = true btids(let Π in Cˆ 1 ∥ . . . ∥Cˆ n, (σc ,σo ,K )) def = ({t | K (t) = ◦ ∧ ¬(σc |= en(Cˆ t ))}, {t | K (t) , ◦ ∧ ¬((σo ,K (t)) |= en(Cˆ t ))}) Fig. 3. States and event traces. We make the following assumptions to simplify the technical setting. There are no regular function calls in either clients or objects. Therefore x := f (E) can only be executed in client code to call object methods, and return E always returns from object methods to clients. Each object method takes only one argument and each method body ends with a return command. Object methods never execute the print(E) command and therefore do not generate external events. The command C in await(B){C} cannot contain await, print, and method calls and returns. It cannot contain loops either so that it always terminates. Operational semantics. The operational semantics rules shown in Fig. 4 consist of three parts, including state transitions made by the whole program, by individual threads, and by clients or object methods, respectively. We define program states S in Fig. 3, where we use two sets of notations to represent states at the concrete and the abstract levels respectively when we study refinement. To ensure that the client code does not touch the object data, in S we separate the data accessed by clients (σc ) and by object methods (σo ). S also contains a thread pool K mapping thread IDs t to the corresponding method call stacks κ. Recall that the only function call allowed in the language is the method invocation made by a client and there are no nested function calls, therefore each κ is either empty (◦, which means the thread is executing the client code), or contains only one stack frame (sl ,x,C), where sl is the local store for the local variables of the method, x is the (client) variable recording the return value, and C is the continuation (the remaining client code to be executed after the return of the method). Figure 4(a) shows that the execution of the programW follows the non-deterministic interleaving semantics, which is defined based on thread transitions defined in Fig. 4(b). Each transition over program configurations is labelled with a program event ι, a triple in the form of (e,∆c ,∆o ). The event e is generated by thread transitions. As defined in Fig. 3, (t, f ,n) records the invocation of the method f with the argument n in the thread t, and (t,ret,n) is for a method return with the return value n. (t,obj) and (t,clt) record a regular object step and a regular client step respectively, while (t,obj,abort) and (t,clt,abort) are for aborting of the thread in the object and client code Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018