Progress of Concurrent Objects with Partial Methods 209 (MName) f9… (PVar)x,y,z· (Expr） =x|n|E+E|. (BExp)B ::true l false I E=E B .. (Stmt) :=x:=Ex:=[E]I[E]:E I print(E)x :cons(E,....E)|dispose(E) 1 skip x:=f(E)|return E I C;C if (B)Celse C I while (B)(C) 1 await(B)(C) (ODecl) II,r : 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. 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: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. Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018