Progress of Concurrent Objects with Partial Methods（Extended Version）

6 Hongjin Liang and Xinyu Feng behavior of any client program using II can also be observed when the client uses II'instead.Then, when verifying a client of II,we can soundly replace II with its abstraction II'. There has been much work(e.g.,[Filipovic et al.2009;Gotsman and Yang 2012;Liang et al.2013]) studying abstraction theorems,which relate linearizability and progress properties with contextual refinements.It has been proved that linearizability of II is equivalent to a contextual refinement between II and its atomic specification I,where the observable behaviors are finite traces of I/O events.When taking progress properties into account,the corresponding contextual refinement should be sensitive to termination or divergence(non-termination).For instance,deadlock-freedom or starvation-freedom of linearizable objects is shown equivalent to a contextual refinement which observes(possibly infinite)full traces of I/O events in fair executions.Then,a client which diverges with II in a fair execution must also have a diverging execution when using the abstraction II' Deadlock-free and starvation-free objects could be distinguished by different abstractions.The abstraction for starvation-free objects is the atomic specification I,while for deadlock-free ones the abstraction has to be non-atomic [Liang and Feng 2016]. The counter implementation inc_tkL()in Fig.1(d)is a progress-aware contextual refinement of the atomic counter INC in Fig.1(e),but inc()in Fig.1(b)is not.To see the difference,consider the client program(2.2).Under fair scheduling,the client calling inc()may generate an empty I/O event trace because it may not print out 1.However,the empty trace cannot be generated when replacing inc()with inc_tkL()or INC(),because the resulting program must print out 1. 2.2 Problems and Our Solutions The existing progress properties and the corresponding contextual refinement are proposed for concurrent objects with total methods only,i.e.,methods that should always return when executed sequentially.They do not apply to objects with partial methods,such as the lock objects in Fig.1(a) and(c),which intend to block at certain situations.We have outlined the key challenges in rea- soning about progress properties of objects with partial methods in Sec.1.We give more detailed explanations here. 2.2.1 Atomic Specifications Need to Be Partial.The specifications defined in(2.1)can characterize the atomic behaviors of lock objects,but they fail to specify that L_ACQ should be partial in the sense that it should be blocked when the lock is unavailable. To address the problem,we introduce the atomic partial specification I,where each method specification is in the form of await(B)(C).For the lock objects,we can define the atomic partial specification I as follows. L_ACQ'(){await (1 =0){1 cid } L_REL()[1:=0;3 (2.3) The await block naturally specifies the atomicity of method functionality,just like the traditional atomic specification(C)(which can be viewed as syntactic sugar for await(true)(C)),therefore r may serve as a specification for linearizable objects.It also shows the fact that the object method is partial,with explicit specification of the enabling condition B.Below we use the atomic partial specification as the starting point to characterize the progress of objects. 2.2.2 Deadlock-Freedom and Starvation-Freedom Do Not Apply.We need new progress properties for objects with partial methods.Consider the following client program(2.4)using the test-and-set lock in Fig.1(a).One of the method calls never finishes. L_acq();II L_acq(); (2.4) It shows that the test-and-set lock object does not satisfy the traditional deadlock-freedom or starvation-freedom property we just presented.Neither does the ticket lock object in Fig.1(c). .Vol.1,No.1,Article.Publication date:January 2018

:6 Hongjin Liang and Xinyu Feng behavior of any client program using Π can also be observed when the client uses Π ′ instead. Then, when verifying a client of Π, we can soundly replace Π with its abstraction Π ′ . There has been much work (e.g., [Filipović et al. 2009; Gotsman and Yang 2012; Liang et al. 2013]) studying abstraction theorems, which relate linearizability and progress properties with contextual refinements. It has been proved that linearizability of Π is equivalent to a contextual refinement between Π and its atomic specification Γ, where the observable behaviors are finite traces of I/O events. When taking progress properties into account, the corresponding contextual refinement should be sensitive to termination or divergence (non-termination). For instance, deadlock-freedom or starvation-freedom of linearizable objects is shown equivalent to a contextual refinement which observes (possibly infinite) full traces of I/O events in fair executions. Then, a client which diverges with Π in a fair execution must also have a diverging execution when using the abstraction Π ′ . Deadlock-free and starvation-free objects could be distinguished by different abstractions. The abstraction for starvation-free objects is the atomic specification Γ, while for deadlock-free ones the abstraction has to be non-atomic [Liang and Feng 2016]. The counter implementation inc_tkL() in Fig. 1(d) is a progress-aware contextual refinement of the atomic counter INC in Fig. 1(e), but inc() in Fig. 1(b) is not. To see the difference, consider the client program (2.2). Under fair scheduling, the client calling inc() may generate an empty I/O event trace because it may not print out 1. However, the empty trace cannot be generated when replacing inc() with inc_tkL() or INC(), because the resulting program must print out 1. 2.2 Problems and Our Solutions The existing progress properties and the corresponding contextual refinement are proposed for concurrent objects with total methods only, i.e., methods that should always return when executed sequentially. They do not apply to objects with partial methods, such as the lock objects in Fig. 1(a) and (c), which intend to block at certain situations. We have outlined the key challenges in rea￾soning about progress properties of objects with partial methods in Sec. 1. We give more detailed explanations here. 2.2.1 Atomic Specifications Need to Be Partial. The specifications defined in (2.1) can characterize the atomic behaviors of lock objects, but they fail to specify that L_ACQ should be partial in the sense that it should be blocked when the lock is unavailable. To address the problem, we introduce the atomic partial specification Γ, where each method specification is in the form of await(B){C}. For the lock objects, we can define the atomic partial specification Γ as follows. L_ACQ'(){ await (l = 0) { l := cid }; } L_REL(){ l := 0; } (2.3) The await block naturally specifies the atomicity of method functionality, just like the traditional atomic specification ⟨C⟩ (which can be viewed as syntactic sugar for await(true){C}), therefore Γ may serve as a specification for linearizable objects. It also shows the fact that the object method is partial, with explicit specification of the enabling condition B. Below we use the atomic partial specification as the starting point to characterize the progress of objects. 2.2.2 Deadlock-Freedom and Starvation-Freedom Do Not Apply. We need new progress properties for objects with partial methods. Consider the following client program (2.4) using the test-and-set lock in Fig. 1(a). One of the method calls never finishes. L_acq(); || L_acq(); (2.4) It shows that the test-and-set lock object does not satisfy the traditional deadlock-freedom or starvation-freedom property we just presented. Neither does the ticket lock object in Fig. 1(c). , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) 7 Table 1.Client(2.5)with different locks."Yes"means it must print out 1."No"otherwise. spec.(2.3)ticket locks (Fig.1(c)) test-and-set locks(Fig.1(a)) Strong Fairness Yes Yes No Weak Fairness No Yes No The problem is that L_acq intends to block when the lock is not available.The non-termination in the above example(2.4)is just the intention of a correct lock implementation;otherwise the lock cannot guarantee mutual exclusion. Our solution.We define two new progress properties for objects with partial methods,which we call partial starvation-freedom(PSF)and partial deadlock-freedom(PDF).PSF requires that in each fair execution trace by any client with the object II,either each method invocation eventually returns (as required in starvation-freedom),or each pending method invocation must be continuously disabled.The latter case intuitively says that this non-termination is caused by the"bad"client,e.g., by inappropriate invocations of the methods.Similarly,PDF requires that in each fair execution trace by any client with the object II,either there always exists a method invocation that eventually returns(as in deadlock-freedom),or each pending method invocation must be continuously disabled. But how do we formally say that a method is disabled?When we informally say this,we actually refer to the enabling condition B in await(B)(C)in the object's atomic partial specification I. However,we may not be able to infer such a condition from the concrete implementation II. To address this problem,our definitions of PSFr(II)and PDFr(II)are parameterized with the specification I(the actual definitions take more parameters,as shown in Sec.5). We can prove the lock objects in Fig.1(a)and(c)satisfy PDF and PSF respectively.We can also show that starvation-freedom and deadlock-freedom are special cases of our PSF and PDF respectively,by instantiating the parameter I with specifications in the form of await(true)(C). 2.2.3 Atomic Partial Specifications Are Insufficient for Progress-Aware Abstractions.Although the atomic partial specification I describes the atomic functionality and the enabling condition of each method,it is insufficient to serve as a progress-aware abstraction for the following reasons. First,the progress of the await command itself is affected by the fairness of scheduling,such as strong fairness and weak fairness. Strong fairness:Every thread which is infinitely often enabled will execute infinitely often. Then,await(B)(C)is not executed only if B is continuously false after some point in the execution trace. Weak fairness:Every thread which is eventually always enabled will execute infinitely often. Then,await(B)(C)may not be executed when B is infinitely often false.This fairness notion is weaker than strong fairness. As a result,the choice of fair scheduling will affect the behaviors of a program or a specification with await commands.To see this,we consider the following client program(2.5). [_]ace;[_]REL;print(1);II while(true){[_lace;[_]REL; (2.5) where and represent holes to be filled with method calls of lock acquire and release, respectively.Table 1 shows the behaviors of the client with different locks.If the client calls the abstract specifications in(2.3),it must execute print(1)under strongly fair scheduling,but may not do so under weakly fair scheduling.This is because the call of L_ACQ'could be infinitely often enabled and infinitely often disabled in an execution,making its termination sensitive to the fairness of scheduling. Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :7 Table 1. Client (2.5) with different locks. “Yes” means it must print out 1, “No” otherwise. spec. (2.3) ticket locks (Fig. 1(c)) test-and-set locks (Fig. 1(a)) Strong Fairness Yes Yes No Weak Fairness No Yes No The problem is that L_acq intends to block when the lock is not available. The non-termination in the above example (2.4) is just the intention of a correct lock implementation; otherwise the lock cannot guarantee mutual exclusion. Our solution. We define two new progress properties for objects with partial methods, which we call partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). PSF requires that in each fair execution trace by any client with the object Π, either each method invocation eventually returns (as required in starvation-freedom), or each pending method invocation must be continuously disabled. The latter case intuitively says that this non-termination is caused by the “bad” client, e.g., by inappropriate invocations of the methods. Similarly, PDF requires that in each fair execution trace by any client with the object Π, either there always exists a method invocation that eventually returns (as in deadlock-freedom), or each pending method invocation must be continuously disabled. But how do we formally say that a method is disabled? When we informally say this, we actually refer to the enabling condition B in await(B){C} in the object’s atomic partial specification Γ. However, we may not be able to infer such a condition from the concrete implementation Π. To address this problem, our definitions of PSFΓ (Π) and PDFΓ (Π) are parameterized with the specification Γ (the actual definitions take more parameters, as shown in Sec. 5). We can prove the lock objects in Fig. 1(a) and (c) satisfy PDF and PSF respectively. We can also show that starvation-freedom and deadlock-freedom are special cases of our PSF and PDF respectively, by instantiating the parameter Γ with specifications in the form of await(true){C}. 2.2.3 Atomic Partial Specifications Are Insufficient for Progress-Aware Abstractions. Although the atomic partial specification Γ describes the atomic functionality and the enabling condition of each method, it is insufficient to serve as a progress-aware abstraction for the following reasons. First, the progress of the await command itself is affected by the fairness of scheduling, such as strong fairness and weak fairness. • Strong fairness: Every thread which is infinitely often enabled will execute infinitely often. Then, await(B){C} is not executed only if B is continuously false after some point in the execution trace. • Weak fairness: Every thread which is eventually always enabled will execute infinitely often. Then, await(B){C} may not be executed when B is infinitely often false. This fairness notion is weaker than strong fairness. As a result, the choice of fair scheduling will affect the behaviors of a program or a specification with await commands. To see this, we consider the following client program (2.5). [ _ ]acq; [ _ ]rel; print(1); || while(true){ [ _ ]acq; [ _ ]rel; } (2.5) where [ _ ]acq and [ _ ]rel represent holes to be filled with method calls of lock acquire and release, respectively. Table 1 shows the behaviors of the client with different locks. If the client calls the abstract specifications in (2.3), it must execute print(1) under strongly fair scheduling, but may not do so under weakly fair scheduling. This is because the call of L_ACQ' could be infinitely often enabled and infinitely often disabled in an execution, making its termination sensitive to the fairness of scheduling. , Vol. 1, No. 1, Article . Publication date: January 2018

8 Hongjin Liang and Xinyu Feng Table 2.Wrappers for atomic specifications. PSF PDF Strong Fairness wr(await(B)(C)) wrF(await(B)(C]) Weak Fairness wr(await(B)(C)) wrp(await(B)(C)) Also note that the two fairness notions coincide when the program does not contain blocking operations.Therefore,regardless of strongly or weakly fair scheduling,the client(2.5)using ticket locks always executes print(1),but it may not do so if using test-and-set locks instead(see Table 1) As a result,for the same object implementation,we may need different abstractions under different scheduling.As shown in Table 1,the specification(2.3)cannot serve as the specification of the test-and-set locks under both strong fairness and weak fairness. Second,even under the same scheduling,different implementations demonstrate different progress, therefore need different abstractions.As shown in Table 1,the different lock implementations have different behaviors,even under the same scheduling. For the above two reasons,we need different abstractions for different combinations of fairness and progress.For PSF and PDF under strong and weak fairness respectively,we may need four different abstractions.Can we systematically generate all of them? Our solution.We define code wrappers over the basic blocking primitive await(B)(C)to generate the abstractions.The code wrappers are syntactic transformations that transform await(B)(C)into possibly non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement.As shown in Table 2,the four wrappers correspond to all combinations of fairness and progress.The definitions are shown in Sec.6.Here we only give some high-level intuitions using the lock objects as examples. First,we observe that the lock specification(2.3)can already serve as an abstraction for ticket locks under strong fairness.or for test-and-set locks under weak fairness.In general,the wrapper wr can be an identity function,i.e.,the atomic partial specifications are already proper abstractions for PSF objects(not only for locks)under strong fairness.But wr is subtle.The atomic partial specifications are insufficient as abstractions for general PDF objects under weak fairness,which we will explain in detail in Sec.6. Second,as we have seen from Table 1,the lock specification(2.3)does not work for PSF locks under weak fairness nor for PDF locks under strong fairness.Then the role of the wrapper wr (or wr)is to generate the same PSF(or PDF)behaviors even though the fairness of scheduling is weaker (or stronger). To guarantee PSF,the idea is to create some kind of "fairness"on termination,ie.,every method call can get the chance to terminate.Given weakly fair scheduling,this requires the enabling condition of the abstraction to continuously remain true.As a result,a possible way to define wr(LACQ)is to keep a queue of threads requesting the lock,and a thread can acquire the lock only when it is at the head of the queue. To support PDF under strongly fair scheduling,we have to allow non-termination even if the enabling condition is infinitely often true.For the client(2.5),the call of L_ACQ'in the specifica- tion(23)under strongly fair scheduling always terminates.Then wr needs to incorporate with some kind of delaying mechanisms,so that the termination of L_ACQ'of the left thread could be delayed every time when the right thread succeeds in acquiring the lock. Vol.1,No.1,Article.Publication date:January 2018

:8 Hongjin Liang and Xinyu Feng Table 2. Wrappers for atomic specifications. PSF PDF Strong Fairness wrsfair PSF (await(B){C}) wrsfair PDF (await(B){C}) Weak Fairness wrwfair PSF (await(B){C}) wrwfair PDF (await(B){C}) Also note that the two fairness notions coincide when the program does not contain blocking operations. Therefore, regardless of strongly or weakly fair scheduling, the client (2.5) using ticket locks always executes print(1), but it may not do so if using test-and-set locks instead (see Table 1). As a result, for the same object implementation, we may need different abstractions under different scheduling. As shown in Table 1, the specification (2.3) cannot serve as the specification of the test-and-set locks under both strong fairness and weak fairness. Second, even under the same scheduling, different implementations demonstrate different progress, therefore need different abstractions. As shown in Table 1, the different lock implementations have different behaviors, even under the same scheduling. For the above two reasons, we need different abstractions for different combinations of fairness and progress. For PSF and PDF under strong and weak fairness respectively, we may need four different abstractions. Can we systematically generate all of them? Our solution. We define code wrappers over the basic blocking primitive await(B){C} to generate the abstractions. The code wrappers are syntactic transformations that transform await(B){C} into possibly non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement. As shown in Table 2, the four wrappers correspond to all combinations of fairness and progress. The definitions are shown in Sec. 6. Here we only give some high-level intuitions using the lock objects as examples. First, we observe that the lock specification (2.3) can already serve as an abstraction for ticket locks under strong fairness, or for test-and-set locks under weak fairness. In general, the wrapper wrsfair PSF can be an identity function, i.e., the atomic partial specifications are already proper abstractions for PSF objects (not only for locks) under strong fairness. But wrwfair PDF is subtle. The atomic partial specifications are insufficient as abstractions for general PDF objects under weak fairness, which we will explain in detail in Sec. 6. Second, as we have seen from Table 1, the lock specification (2.3) does not work for PSF locks under weak fairness nor for PDF locks under strong fairness. Then the role of the wrapper wrwfair PSF (or wrsfair PDF) is to generate the same PSF (or PDF) behaviors even though the fairness of scheduling is weaker (or stronger). To guarantee PSF, the idea is to create some kind of “fairness” on termination, i.e., every method call can get the chance to terminate. Given weakly fair scheduling, this requires the enabling condition of the abstraction to continuously remain true. As a result, a possible way to define wrwfair PSF (L_ACQ’) is to keep a queue of threads requesting the lock, and a thread can acquire the lock only when it is at the head of the queue. To support PDF under strongly fair scheduling, we have to allow non-termination even if the enabling condition is infinitely often true. For the client (2.5), the call of L_ACQ' in the specifica￾tion (2.3) under strongly fair scheduling always terminates. Then wrsfair PDF needs to incorporate with some kind of delaying mechanisms, so that the termination of L_ACQ' of the left thread could be delayed every time when the right thread succeeds in acquiring the lock. , Vol. 1, No. 1, Article . Publication date: January 2018

Progress of Concurrent Objects with Partial Methods(Extended Version) 9 (MName) f9… (PVar)x,y,z... (Expr） E =x|n|E+E|. (BExp)B ::true l false I E=E B .. (Stmt) C :=x:=Ex:=[E]I[E]:E I print(E)x :cons(E,....E)|dispose(E) skip x:=f(E)|return E I C;C if (B)C else C I while (B)(C) 1 await(B)(C) (ODecl) Π，T= f(,x1.C1).....fn(Pn.xn.Cn) (Prog) W = let II in Cill...lCn (Thrd)C:=C end Fig.2.Syntax of the programming language. 2.2.4 Other Results.We also have the following new results in addition to the new progress properties and code wrappers. Abstraction theorem.We prove the abstraction theorem,saying that our new progress properties PSF and PDF(together with linearizability)are equivalent to contextual refinements where the abstractions are generated by the corresponding wrappers.On the one hand,the theorem justifies the abstractions generated by our wrappers,showing that they are refined by linearizable and PSF (or PDF)object implementations.On the other hand,it also justifies our formulation of PSF and PDF by showing that they imply progress-aware contextual refinements. The abstraction theorem also allows us to verify safety and progress properties of whole programs (consisting of clients and objects)in a modular way-after proving linearizability and PSF(or PDF) of an object II with respect to its atomic partial specification I,we can replace II with the abstraction generated by applying the corresponding wrapper over T,and then reason about properties of the whole program at the high abstraction level. Program logic.Finally we design a program logic as the proof method for verifying PSF and PDF objects.It ensures linearizability and PSF (or PDF)of an object II with respect to its atomic partial specification I.The logic is a generalization of our previous program logic LiLi for starvation-free and deadlock-free objects [Liang and Feng 2016],plus new inference rules for the await statement under strong and weak fairness.We will explain the details in Sec.7. 3 THE LANGUAGE Figure 2 shows the syntax of the language.A program W consists of an object declaration II and n parallel threads C as clients sharing the object.To simplify the language,we assume there is only one object in each program.Each II maps method names fi to annotated method implementations (P,xi,Ci),where xi and Ci are the formal parameter and the method body respectively,and the assertion Pi is an annotated precondition over the object state to ensure the safe execution of the method.It is defined in Fig.3 and is used in the operational semantics explained below.A thread C is either a command C,or an end flag marking termination of the thread.The commands include the standard ones used in separation logic,where x:=[E]and [E]:=E'read and write the heap at the location E respectively,and x:=cons(E,...,E)and dispose(E)allocate and free memory cells respectively.In addition,we have method call (x:=f(E))and return (return E)commands. The print(E)command generates externally observable events,which are used to define trace refinements in Sec.4.The await(B)(C)command is the only blocking primitive in the language.It blocks the current thread if B does not hold,otherwise C is executed atomically together with the testing of B. Vol.1.No.1,Article.Publication date:January 2018

Progress of Concurrent Objects with Partial Methods (Extended Version) :9 (MName) f ,д . . . (PVar) x,y,z . . . (Expr) E ::= x | n | E + E | . . . (BExp) B ::= true | false | E = E | ¬B | . . . (Stmt) C ::= x := E | x := [E] | [E] := E | print(E) | x := cons(E,. . . ,E) | dispose(E) | skip | x := f (E) | return E | C;C | if (B) C else C | while (B){C} | await(B){C} (ODecl) Π, Γ ::= {f1 ❀ (P1,x1,C1),. . . , fn ❀ (Pn,xn,Cn )} (Prog) W ::= let Π in Cˆ 1 ∥ . . . ∥Cˆ n (Thrd) Cˆ ::= C | end Fig. 2. Syntax of the programming language. 2.2.4 Other Results. We also have the following new results in addition to the new progress properties and code wrappers. Abstraction theorem. We prove the abstraction theorem, saying that our new progress properties PSF and PDF (together with linearizability) are equivalent to contextual refinements where the abstractions are generated by the corresponding wrappers. On the one hand, the theorem justifies the abstractions generated by our wrappers, showing that they are refined by linearizable and PSF (or PDF) object implementations. On the other hand, it also justifies our formulation of PSF and PDF by showing that they imply progress-aware contextual refinements. The abstraction theorem also allows us to verify safety and progress properties of whole programs (consisting of clients and objects) in a modular way — after proving linearizability and PSF (or PDF) of an object Π with respect to its atomic partial specification Γ, we can replace Π with the abstraction generated by applying the corresponding wrapper over Γ, and then reason about properties of the whole program at the high abstraction level. Program logic. Finally we design a program logic as the proof method for verifying PSF and PDF objects. It ensures linearizability and PSF (or PDF) of an object Π with respect to its atomic partial specification Γ. The logic is a generalization of our previous program logic LiLi for starvation-free and deadlock-free objects [Liang and Feng 2016], plus new inference rules for the await statement under strong and weak fairness. We will explain the details in Sec. 7. 3 THE LANGUAGE Figure 2 shows the syntax of the language. A program W consists of an object declaration Π and n parallel threads Cˆ as clients sharing the object. To simplify the language, we assume there is only one object in each program. Each Π maps method names fi to annotated method implementations (Pi ,xi ,Ci ), where xi and Ci are the formal parameter and the method body respectively, and the assertion Pi is an annotated precondition over the object state to ensure the safe execution of the method. It is defined in Fig. 3 and is used in the operational semantics explained below. A thread Cˆ is either a command C, or an end flag marking termination of the thread. The commands include the standard ones used in separation logic, where x := [E] and [E] := E ′ read and write the heap at the location E respectively, and x := cons(E,. . . ,E) and dispose(E) allocate and free memory cells respectively. In addition, we have method call (x := f (E)) and return (return E) commands. The print(E) command generates externally observable events, which are used to define trace refinements in Sec. 4. The await(B){C} command is the only blocking primitive in the language. It blocks the current thread if B does not hold, otherwise C is executed atomically together with the testing of B. , Vol. 1, No. 1, Article . Publication date: January 2018

:10 Hongjin Liang and Xinyu Feng (ThrdID) t 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) p E Data-Data (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)△ E(ThrdID) (PEven)t=(e,△c,△o) (ETrace) ::=eIe:8 (co-inductive) (PTrace)T :=EI::T (co-inductive) en(©s/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 Vol.1,No.1,Article.Publication date:January 2018

: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 , Vol. 1, No. 1, Article . Publication date: January 2018