Progress of Concurrent Objects with Partial Methods(Extended Version) 21 (RelAssn)P.Q.J ::B I emp EE I E EI p]I P*I PAQ I PVQ I... (FullAssn)p.q ::P I arem(C)I (E)(Ek,....E1)I p*q I pq l... (RelAct)R.G ::PkQ [P]LGJo I D I GAG I GVG .. (DAct)D :PQ Vx.D I DAD :=(a,) u=(nk,.,n1） w E Nat Enabled(P)p (D)DA(Enabled(D)xtrue) Enabled(Vx.D)x.Enabled(D) D'≤Dif(Enabled(D)→Enabled(D) Enabled(DADz)Enabled(1)VEnabled(D2) Λ(0→2D) Fig.9.Assertions and models. LiLi does not have await commands.There while-loops are the only commands that affect progress.Now we have to reason about await in object code,which may affect progress as well.It is interesting to see that await can be reasoned about similarly as while-loops. We also have await(B)(C)as partial specifications.Since we want termination-preserving refinement,we do not have to guarantee progress of the concrete object methods when the partial specification is disabled. As an extension of LiLi,our logic borrows LiLi's key ideas and most of the logic rules.Due to the space limit,the full details of the logic are given in Appendix B.Below we only show the major extensions. 7.1 Assertions The assertions,shown in Fig.9,are the same as those in LiLi.P and O are assertions over relational states which are pairs of concrete and abstract object states (see Fig.9).We use relational assertions because our logic establishes refinement between the concrete object implementation and the abstract specification.As in separation logic,we use EE and EE to specify memory cells at the concrete and abstract level respectively.emp specifies empty states,and the separating conjunction P *O specifies two disjoint parts of which satisfy P and O respectively. The full assertions p and g specify triples in the form of(,(u,w),C).In addition to the relational state the assertions also describe the numbers (u,w)of available tokens,and the high-level (abstract)method code C that remains to be refined by the low-level (concrete)code.The assertion arem(C)specifies such high-level code in the triple. Tokens and multi-level delaying actions.As explained above,LiLi uses tokens as resources to prevent infinitely many execution steps and infinitely many delaying actions.It requires that each round of a while-loop consumes a 0-token,and each delaying action consumes a -token.LiLi also stratify delaying actions into multiple levels.The delay caused by high-level actions may lead to executions of more low-level ones (and non-delaying actions),but not vice versa.Therefore we use w to represent the number of 0-tokens,and use the vector u for the numbers of the k-level -tokens, as defined in Fig.9.They are described by the assertions (E)and(Ek,...,E1)respectively. Rely/guarantee conditions and definite actions.The rely/guarantee conditions R and G specify stratified transitions between relational states,i.e.,they are assertions over(,',k),where k is the level of stratified delaying actions.P kO specifies a level-k delaying transition from P to Q. The subscript k can be omitted when k =0.[P]specifies identity transitions with the initial states satisfying P.[GJo can be satisfied only by level-0 transitions in G.Definite actions D is a special form of rely/guarantee condition.PO specifies a transition where the final state satisfies O if the initial state satisfies P. Vol.1.No.1,Article.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods (Extended Version) :21 (RelAssn) P,Q,J ::= B | emp | E 7→ E | E Z⇒ E | TpU | P ∗ Q | P ∧ Q | P ∨ Q | . . . (FullAssn) p,q ::= P | arem(C) | ♦(E) | (Ek ,. . . ,E1) | p ∗ q | p ∧ q | . . . (RelAct) R,G ::= P nk Q | [P] | ⌊G⌋0 | D | G ∧ G | G ∨ G | . . . (DAct) D ::= P ❀ Q | ∀x. D | D ∧ D S :: = (σ,Σ) u ::= (nk ,. . . ,n1) w ∈ Nat Enabled(P ❀ Q) def = P Enabled(∀x. D) def = ∃x. Enabled(D) Enabled(D1 ∧ D2) def = Enabled(D1) ∨ Enabled(D2) ⟨D⟩ def = D ∧ (Enabled(D) n true) D′ 6 D iff (Enabled(D′ ) ⇒ Enabled(D)) ∧ (D ⇒ D′ ) Fig. 9. Assertions and models. • LiLi does not have await commands. There while-loops are the only commands that affect progress. Now we have to reason about await in object code, which may affect progress as well. It is interesting to see that await can be reasoned about similarly as while-loops. • We also have await(B){C} as partial specifications. Since we want termination-preserving refinement, we do not have to guarantee progress of the concrete object methods when the partial specification is disabled. As an extension of LiLi, our logic borrows LiLi’s key ideas and most of the logic rules. Due to the space limit, the full details of the logic are given in Appendix B. Below we only show the major extensions. 7.1 Assertions The assertions, shown in Fig. 9, are the same as those in LiLi. P and Q are assertions over relational states S, which are pairs of concrete and abstract object states (see Fig. 9). We use relational assertions because our logic establishes refinement between the concrete object implementation and the abstract specification. As in separation logic, we use E 7→ E and E Z⇒ E to specify memory cells at the concrete and abstract level respectively. emp specifies empty states, and the separating conjunction P ∗ Q specifies two disjoint parts of S, which satisfy P and Q respectively. The full assertions p and q specify triples in the form of (S, (u,w),C). In addition to the relational state S, the assertions also describe the numbers (u,w) of available tokens, and the high-level (abstract) method code C that remains to be refined by the low-level (concrete) code. The assertion arem(C) specifies such high-level code in the triple. Tokens and multi-level delaying actions. As explained above, LiLi uses tokens as resources to prevent infinitely many execution steps and infinitely many delaying actions. It requires that each round of a while-loop consumes a ♦-token, and each delaying action consumes a -token. LiLi also stratify delaying actions into multiple levels. The delay caused by high-level actions may lead to executions of more low-level ones (and non-delaying actions), but not vice versa. Therefore we use w to represent the number of ♦-tokens, and use the vector u for the numbers of the k-level -tokens, as defined in Fig. 9. They are described by the assertions ♦(E) and (Ek ,. . . ,E1) respectively. Rely/guarantee conditions and definite actions. The rely/guarantee conditions R and G specify stratified transitions between relational states, i.e., they are assertions over (S,S′ ,k), where k is the level of stratified delaying actions. P nk Q specifies a level-k delaying transition from P to Q. The subscript k can be omitted when k = 0. [P] specifies identity transitions with the initial states satisfying P. ⌊G⌋0 can be satisfied only by level-0 transitions in G. Definite actions D is a special form of rely/guarantee condition. P ❀ Q specifies a transition where the final state satisfies Q if the initial state satisfies P. , Vol. 1, No. 1, Article . Publication date: January 2018
:22 Hongjin Liang and Xinyu Feng As in LiLi,all assertions are implicitly parameterized with a thread ID t. 7.2 Logic Rules Figure 10 shows the key logic rules.As the top rule of the logic,the oBJ rule says that,to verify II satisfies its specification I with the object invariant P,one needs to specify the rely/guarantee conditions R and G,and the definite actions D,and then prove that each individual object method implementation refines its specification.Here I must be an atomic partial specification. For each method,we take the object invariant P and the annotated preconditions P and P'(in II and r)as preconditions.We also assign -tokens in the precondition((Ek,...,E1))to constrain the number of delaying actions executed in the method.arem(C')says that the high-level code which remains to be refined at this point is C.At the end we need to re-establish the object invariant P. and show that there is no more high-level code that needs to be refined (i.e.,arem(skip)),which means the method body indeed refines the specification C'. The object invariant P should also ensure that the annotated pre-conditions P and p'are either both true or both false.That is,whenever P holds,it is either safe to call the methods at both the concrete and abstract levels,or unsafe to do so at both levels.The other side conditions in the rule are the same as those in LiLi and irrelevant to our extensions,so we omit the explanations here. The WHL rule.The rule for while-loops is almost the same as the wHL rule in LiLi,with the changes highlighted in gray boxes.We verify the loop body with a precondition p',which needs to be derived from the loop invariant p and the loop condition B.In two cases we must ensure that there are no infinite loops: the definite action D is enabled (see Fig.9 for the definition of Enabled(D)).Then the loop must terminate to guarantee that the definite action D definitely occurs. the current thread is not blocked.Here we need to find a condition O that ensures the current thread can make progress without waiting for actions of other threads. The second premise of the rule says,in either of the two cases above we must consume a o-token for each round of the loop,as p'has one less token than p A B. On the other hand,if the current thread is blocked (O does not hold)and it is not in the middle of a definite action,the loop can run an indefinite number of rounds to wait for the environment actions.It does not have to consume tokens.However,we must ensure the thread cannot be blocked forever,i.e.,O cannot be always false.This is achieved by the definite-progress condition introduced in LiLi.We show a generalized definition in Def.7.1,with the changes highlighted in gray boxes. Definition 7.1(Definite Progress).(R.G:D(Q,Bn))iff the following hold for any t: (1)eitherOt,orBh,or there exists t'such that t'#t and Enabled(D); (2)for any t'#t and 'if (,,0)R:A((D)v((-Bh)Bh)).then f()<f(); (3)for any',if(e,G',o)卡RVGt,then f(G)≤f(©). Here f is a function that maps the relational states to some metrics over which there is a well-founded order < The definite progress condition(R,G:D(O,B))tries to ensure O is eventually always true, unless Bh is eventually always false.It requires the following conditions to hold: (1)Either O holds,which means that the low-level code is no longer blocked;or the high-level specification await(B)(C')is disabled,so that the low-level code does not have to progress to refine the high-level code;or one of the definite actions in D that the current thread t .Vol.1,No.1,Article.Publication date:January 2018
:22 Hongjin Liang and Xinyu Feng As in LiLi, all assertions are implicitly parameterized with a thread ID t. 7.2 Logic Rules Figure 10 shows the key logic rules. As the top rule of the logic, the obj rule says that, to verify Π satisfies its specification Γ with the object invariant P, one needs to specify the rely/guarantee conditions R and G, and the definite actions D, and then prove that each individual object method implementation refines its specification. Here Γ must be an atomic partial specification. For each method, we take the object invariant P and the annotated preconditions P and P ′ (in Π and Γ) as preconditions. We also assign -tokens in the precondition ((Ek ,. . . ,E1)) to constrain the number of delaying actions executed in the method. arem(C ′ ) says that the high-level code which remains to be refined at this point is C ′ . At the end we need to re-establish the object invariant P, and show that there is no more high-level code that needs to be refined (i.e., arem(skip)), which means the method body indeed refines the specification C ′ . The object invariant P should also ensure that the annotated pre-conditions P and P ′ are either both true or both false. That is, whenever P holds, it is either safe to call the methods at both the concrete and abstract levels, or unsafe to do so at both levels. The other side conditions in the rule are the same as those in LiLi and irrelevant to our extensions, so we omit the explanations here. The whl rule. The rule for while-loops is almost the same as the whl rule in LiLi, with the changes highlighted in gray boxes. We verify the loop body with a precondition p ′ , which needs to be derived from the loop invariant p and the loop condition B. In two cases we must ensure that there are no infinite loops: • the definite action D is enabled (see Fig. 9 for the definition of Enabled(D)). Then the loop must terminate to guarantee that the definite action D definitely occurs. • the current thread is not blocked. Here we need to find a condition Q that ensures the current thread can make progress without waiting for actions of other threads. The second premise of the rule says, in either of the two cases above we must consume a ♦-token for each round of the loop, as p ′ has one less token than p ∧ B. On the other hand, if the current thread is blocked (Q does not hold) and it is not in the middle of a definite action, the loop can run an indefinite number of rounds to wait for the environment actions. It does not have to consume tokens. However, we must ensure the thread cannot be blocked forever, i.e., Q cannot be always false. This is achieved by the definite-progress condition introduced in LiLi. We show a generalized definition in Def. 7.1, with the changes highlighted in gray boxes. Definition 7.1 (Definite Progress). S |= (R,G : D f −→(Q,Bh )) iff the following hold for any t: (1) either S |= Qt , or S |= ¬Bh, or there exists t ′ such that t ′ , t and S |= Enabled(Dt ′ ); (2) for any t ′ , t and S′ , if (S,S′ ,0) |= Rt ∧ (⟨Dt ′⟩ ∨((¬Bh ) n Bh )) , then ft (S′ ) < ft (S); (3) for any S′ , if (S,S′ ,0) |= Rt ∨ Gt , then ft (S′ ) ≤ ft (S). Here f is a function that maps the relational states S to some metrics over which there is a well-founded order <. The definite progress condition (R,G : D f −→(Q,Bh )) tries to ensure Q is eventually always true, unless Bh is eventually always false. It requires the following conditions to hold: (1) Either Q holds, which means that the low-level code is no longer blocked; or the high-level specification await(Bh ){C ′ } is disabled, so that the low-level code does not have to progress to refine the high-level code; or one of the definite actions in D that the current thread t , Vol. 1, No. 1, Article . Publication date: January 2018
Progress of Concurrent Objects with Partial Methods(Extended Version) 23 for all f∈dom():Π(f)=(p,x,C)Tf)=(p',y,C')P→(pAp）V(-P∧p') D,R,G(PA ()A (x =y)A arem(C)A(Ek,...,E1))CP A arem(skip)) t,t'.t≠t'→Gt→Rt wffAct(R,D)P→Enabled(D) D,R,GH(P]II r (OBJ)】 pAB→p'pABA(Enabled(D)VQ)→p'*(Aemp) D,R.G H Ip')Cip) pAB→arem(await(B')HC')StaU,RvG) J→(RG:D(Q,B) D'≤D wffAct(R,D) (WHL) D,R,G(p]while (B)(CHp A-B) p A Enabled(D)=B D,Id,Gp A B)(C)q Sta(p,ql,R) D'≤D wffAct(R.D')p3B'.C'.arem(await(B)(C)A(R:D'(B.B)) (AWAIT-W) D,R.G Fwfair (p)await(B)(CHq) p A Enabled(D)=B D,Id,G(p A BKC)q) Sta((p.ql.R) D'sD wffAct(R.D)p3B'C'.arem(await(B')(C)A(R:D'(B.B)) (AWAIT-S) D.R,G Fsfair (plawait(B)(CHg) Fig.10.The key extensions of inference rules. waits for is enabled in some thread t'.Here D can be viewed as a set of n definite actions in the form of D:A...ADn parameterized with thread IDs. (2)There is a well-founded metric f that becomes strictly smaller whenever(a)an environment thread t'executes a definite action in D,or(b)an environment action has turned the high- level command from disabled to enabled.Case(a)requires that the number of definite actions waited by the current thread must be strictly decreasing.Therefore eventually there are no enabled definite actions.By condition(1)we know eventually either O or-B is true.Case(b) further requires that the high-level command cannot be infinitely often disabled and then enabled during the loop.Therefore either Bh is eventually always true or it is eventually always false.In the former case we know O must be eventually always true by the above condition (1).In the latter the loop does not have to terminate because the execution is well-blocked (see Fig.6). (3)The value of f over program states cannot be increased by any level-0 actions (i.e.,non- delaying actions). Note that the last two conditions do not prevent delaying actions(level-k actions where k >0)from increasing the value of f,but such an increase can only occur a finite number of times because each delaying action consumes a-token.The effects of delaying actions are shown in the AroM rule, which is the same as in LiLi.Since the way delaying action is handled is orthogonal to our extension for partial methods,we omit the rule here. To ensure the definite progress condition always holds,we need to find an invariant J which is preserved by any program step(by the current thread or by the environment),and require thatJ implies definite progress,given the currently remaining high-level command await(B')(C').Note that to simplify the presentation we treat arem(skip)as arem(await(true){skip))so that it can be reasoned about in the same way. Vol.1.No.1,Article.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods (Extended Version) :23 for all f ∈ dom(Π) : Π(f ) = (P,x,C) Γ(f ) = (P ′ ,y,C ′ ) P ⇒ (P ∧ P ′ ) ∨ (¬P ∧ ¬P ′ ) D,R,G ⊢ {P ∧ (P ∧ P ′ ) ∧ (x = y) ∧ arem(C ′ ) ∧ (Ek ,. . . ,E1)}C {P ∧ arem(skip)} ∀t,t ′ . t , t ′ =⇒ Gt ⇒ Rt ′ wffAct(R,D) P ⇒ ¬Enabled(D) D,R,G ⊢ {P}Π : Γ (obj) p∧B ⇒ p ′ p∧B∧(Enabled(D)∨Q) ⇒ p ′ ∗(♦∧emp) D,R,G ⊢ {p ′ }C{p} p ∧ B ⇒ J ∧ arem(await(B ′ ){C ′ }) Sta(J,R ∨ G) J ⇒ (R,G : D′ f −−→(Q,B ′ )) D′ 6 D wffAct(R,D′ ) D,R,G ⊢ {p}while (B){C}{p ∧ ¬B} (whl) p ∧ Enabled(D) ⇒ B D,Id,G ⊢ {p ∧ B}⟨C⟩{q} Sta({p,q},R) D′ 6 D wffAct(R,D′ ) p ⇒ ∃B ′ ,C ′ . arem(await(B ′ ){C ′ }) ∧ (R : D′◦ f −→(B,B ′ )) D,R,G ⊢wfair {p}await(B){C}{q} (await-w) p ∧ Enabled(D) ⇒ B D,Id,G ⊢ {p ∧ B}⟨C⟩{q} Sta({p,q},R) D′ 6 D wffAct(R,D′ ) p ⇒ ∃B ′ ,C ′ . arem(await(B ′ ){C ′ }) ∧ (R : D′• f −→(B,B ′ )) D,R,G ⊢sfair {p}await(B){C}{q} (await-s) Fig. 10. The key extensions of inference rules. waits for is enabled in some thread t ′ . Here D can be viewed as a set of n definite actions in the form of D1 ∧ . . . ∧ Dn parameterized with thread IDs. (2) There is a well-founded metric f that becomes strictly smaller whenever (a) an environment thread t ′ executes a definite action in D, or (b) an environment action has turned the highlevel command from disabled to enabled. Case (a) requires that the number of definite actions waited by the current thread must be strictly decreasing. Therefore eventually there are no enabled definite actions. By condition (1) we know eventually either Q or ¬Bh is true. Case (b) further requires that the high-level command cannot be infinitely often disabled and then enabled during the loop. Therefore either Bh is eventually always true or it is eventually always false. In the former case we know Q must be eventually always true by the above condition (1). In the latter the loop does not have to terminate because the execution is well-blocked (see Fig. 6). (3) The value of f over program states cannot be increased by any level-0 actions (i.e., nondelaying actions). Note that the last two conditions do not prevent delaying actions (level-k actions where k > 0) from increasing the value of f , but such an increase can only occur a finite number of times because each delaying action consumes a -token. The effects of delaying actions are shown in the atom rule, which is the same as in LiLi. Since the way delaying action is handled is orthogonal to our extension for partial methods, we omit the rule here. To ensure the definite progress condition always holds, we need to find an invariant J which is preserved by any program step (by the current thread or by the environment), and require that J implies definite progress, given the currently remaining high-level command await(B ′ ){C ′ }. Note that to simplify the presentation we treat arem(skip) as arem(await(true){skip}) so that it can be reasoned about in the same way. , Vol. 1, No. 1, Article . Publication date: January 2018
:24 Hongjin Liang and Xinyu Feng The WHL rule also allows us to use D',a subset of D,to prove definite progress,which is useful to simplify the proofs.See the definition of D'sD in Fig.9.D'also needs to satisfy wffAct(R,D'). This premise is taken from LiLi and we do not explain it here. Since we have highlighted the changes over the wHL rule in LiLi,we can see that the wHL rule in LiLi is a specialization of ours when the high-level code is always in the form of await(true)(C'). Rules for await commands.Our logic introduces two new rules,AwArr-w and AwAIT-s,to verify await commands in the object implementation under weakly fair and strongly fair scheduling.We use the subscripts of the judgment to distinguish the scheduling. Naturally the AwArr-w rule combines the AToM rule in LiLi and the WHL rule.If await(B)(C)is enabled,we can simply treat C as an atomic block(C)and apply the AroM rule of LiLi to verify it. In this case we do not need to consider the interference and take ld as the rely condition (where ld is a shorthand notation for [true],which specifies arbitrary identity transitions). Similar to the wHL rule,if the definite action D is enabled,then await(B)(C)must be enabled at this point(see the first premise of the AwArr-w rule).This is because we require that,when enabled,the definite action D must be fulfilled regardless of environment behaviors.Therefore the current thread cannot be blocked. Finally,we require that,even if the command is blocked,it must be eventually enabled unless the corresponding high-level specification is blocked too.So if we view the enabling condition B the same as the condition O we use in the wHL rule,we require the same definite progress condition, except that things are simpler here because await(B)(C)finishes in one step once enabled,unlike loops which take multiple steps to finish even if O holds.Therefore we do not need the invariant J used in the wHL rule,and we do not need to consider actions in G in the definite progress condition. We can use a simpler condition(R:D'o(B,B'))defined below,which simply instantiates G with Id and Q with Bin (R.G:D(Q.B))(see Def.7.1). Definition 7.2(Definite Progress for Await). 。G卡(R:Do(B,Bh》ifGF(R,ld:D-(B,Bh》. .(R:D(BI,Bh))iff the following hold for any t: (1)either =B,or Bh,or there exists t'such that t'#t and Enabled(D); (2)for any t'≠t and',if(G,G',0)FRA(《De〉V(-Bh)xBh),then f(G)<f(©)： (3)for any G',if (,,0)Rt A((-B)(-B)),thenf(')(). The AWArr-s rule for strongly fair scheduling looks almost the same as the Awarr-w rule,with a slightly different definite progress condition(R:D'(B,B)),which is also shown in Def.7.2 with the difference highlighted in the gray box.The key difference here is that the low-level enabling condition B(represented as Br in Def.7.2)does not have to be stable once it becomes true.Under strongly fair scheduling we know the await block will be executed as long as it is enabled infinitely often.Therefore in condition(3)we only need to ensure that f does not increase if the enabling condition B remains false,but we allow f to increase whenever we see B holds. The WHL rule,AWArr-w rule and AWArr-s rule are the only new command rules we introduce to reason about partial methods and blocking primitives.All the other command rules are taken directly from LiLi,which are omitted here. Vol.1,No.1,Article.Publication date:January 2018
:24 Hongjin Liang and Xinyu Feng The whl rule also allows us to use D′ , a subset of D, to prove definite progress, which is useful to simplify the proofs. See the definition of D′ 6 D in Fig. 9. D′ also needs to satisfy wffAct(R,D′ ). This premise is taken from LiLi and we do not explain it here. Since we have highlighted the changes over the whl rule in LiLi, we can see that the whl rule in LiLi is a specialization of ours when the high-level code is always in the form of await(true){C ′ }. Rules for await commands. Our logic introduces two new rules, await-w and await-s, to verify await commands in the object implementation under weakly fair and strongly fair scheduling. We use the subscripts of the judgment to distinguish the scheduling. Naturally the await-w rule combines the atom rule in LiLi and the whl rule. If await(B){C} is enabled, we can simply treat C as an atomic block ⟨C⟩ and apply the atom rule of LiLi to verify it. In this case we do not need to consider the interference and take Id as the rely condition (where Id is a shorthand notation for [true], which specifies arbitrary identity transitions). Similar to the whl rule, if the definite action D is enabled, then await(B){C} must be enabled at this point (see the first premise of the await-w rule). This is because we require that, when enabled, the definite action D must be fulfilled regardless of environment behaviors. Therefore the current thread cannot be blocked. Finally, we require that, even if the command is blocked, it must be eventually enabled unless the corresponding high-level specification is blocked too. So if we view the enabling condition B the same as the condition Q we use in the whl rule, we require the same definite progress condition, except that things are simpler here because await(B){C} finishes in one step once enabled, unlike loops which take multiple steps to finish even if Q holds. Therefore we do not need the invariant J used in the whl rule, and we do not need to consider actions in G in the definite progress condition. We can use a simpler condition (R : D′◦ f −→(B,B ′ )) defined below, which simply instantiates G with Id and Q with B in (R,G : D′ f −→(Q,B ′ )) (see Def. 7.1). Definition 7.2 (Definite Progress for Await). • S |= (R : D◦ f −→(Bl ,Bh )) iff S |= (R,Id: D f −→(Bl ,Bh )). • S |= (R : D• f −→(Bl ,Bh )) iff the following hold for any t: (1) either S |= Bl , or S |= ¬Bh, or there exists t ′ such that t ′ , t and S |= Enabled(Dt ′ ); (2) for any t ′ , t and S′ , if (S,S′ ,0) |= Rt ∧ (⟨Dt ′⟩ ∨ ((¬Bh ) n Bh )), then ft (S′ ) < ft (S); (3) for any S′ , if (S,S′ ,0) |= Rt ∧((¬Bl ) n (¬Bl )) , then ft (S′ ) ≤ ft (S). The await-s rule for strongly fair scheduling looks almost the same as the await-w rule, with a slightly different definite progress condition (R : D′• f −→(B,B ′ )), which is also shown in Def. 7.2 with the difference highlighted in the gray box. The key difference here is that the low-level enabling condition B (represented as Bl in Def. 7.2) does not have to be stable once it becomes true. Under strongly fair scheduling we know the await block will be executed as long as it is enabled infinitely often. Therefore in condition (3) we only need to ensure that f does not increase if the enabling condition Bl remains false, but we allow f to increase whenever we see Bl holds. The whl rule, await-w rule and await-s rule are the only new command rules we introduce to reason about partial methods and blocking primitives. All the other command rules are taken directly from LiLi, which are omitted here. , Vol. 1, No. 1, Article . Publication date: January 2018
Progress of Concurrent Objects with Partial Methods(Extended Version) 25 7.3 Soundness of the Logic The two AwArr rules actually give us two program logics,for strongly fair and weakly fair scheduling respectively.To distinguish them,we use D,R,G(P)II:I to represent the verification using the logic for x-scheduling(xE [sfair,wfair)),where the corresponding AwArr rule is used. Theorem 7.3 shows that our logic is sound in that it guarantees linearizability and partial deadlock freedom(PDF)of concurrent objects.It also ensures partial starvation freedom(PSF)if the rely/guarantee conditions specify only level-0 actions,as required by R=[RJo and G=LGJo. That is,none of the object actions of a thread could delay the progress of other threads.With the specialized R and G.we can derive the progress of each single thread,which gives us PSF. THEOREM 7.3 (SOUNDNESS).If D.R.Gx (P]II:T and P,then (1)both IIT and PDF()hold:and (2)ifR→LRJo andG→lGo,then PSF()holds.. where xe{sfair,,wfair,andp→p些Yo,Σ.(p(a)=z)→(o,)Fp. Proofs of the theorem are in Appendix B.We first prove the logic establishes the progress-aware contextual refinements,and then apply the Abstraction Theorem 6.2 to ensure linearizability and the progress properties.The proof structure is similar to the one for LiLi. 8 EXAMPLES We have applied the program logic to verify ticket locks [Mellor-Crummey and Scott 1991],test-and- set locks [Herlihy and Shavit 2008],bounded partial queues with two locks [Herlihy and Shavit 2008] (where the locks are implemented using the specification(2.3))and Treiber stacks [Treiber 1986] with partial pop methods.Perhaps interestingly,we also use our logic to prove that,for the atomic partial specification I for locks,the wrapping ofr(as the object implementation)respects I itself as the atomic specification under the designated fairness conditions,ie(D.R.G)T) holds for certain D,R,G and P,and for different combinations of fairness x and progress Prog. This result validates our wrappers and program logic.It shows Prog(wr())holds,ieeach wrapper itself satisfies the corresponding progress property.Below we show the proofs for test- and-set locks,ticket locks,and simple locks implemented using await which guarantee PSF under weak fairness.The proofs of other examples are given in Appendix C. 8.1 Test-and-Set Locks In Fig.11,we verify PDF of the test-and-set locks using our logic with the atomic partial specifica- tions L_ACQ'and L_REL defined in(2.3).To distinguish the variables at the two levels,below we use capital letters (e.g.,L)in the specifications and small letters(e.g.,1)in the implementations. As we explained in Sec.3,the method L_rel and the specification L_REL have annotated pre- conditions (1 cid)and (L cid),respectively.That is,it is not allowed to call L_rel (or L_REL) when the thread does not hold the lock.The annotated precondition for L_acq and L_ACQ'is true. In Fig.11,we define the assertion lock as the object invariant P used in the oBJ rule.Then the method L_acq is verified with the precondition lock,and L_rel is verified with the precondition lockA(1=cid)which is reduced to lockedByeid,as shown in Fig.11. To verify L_acq,we make the following key observations.When the cas at line 3 succeeds, L_ACQ'must be enabled and can be executed correspondingly.And at the time when the cas fails, L_ACQ'must be disabled.The progress of L_acq relies on that the environment thread holding the lock could eventually release the lock,i.e.,turning the current thread's L_ACQ'from disabled to enabled.But such an action is not "definite",since the client thread may never call the L_rel Vol.1.No.1,Article.Publication date:January 2018
Progress of Concurrent Objects with Partial Methods (Extended Version) :25 7.3 Soundness of the Logic The two await rules actually give us two program logics, for strongly fair and weakly fair scheduling respectively. To distinguish them, we use D,R,G ⊢χ {P}Π : Γ to represent the verification using the logic for χ-scheduling (χ ∈ {sfair,wfair}), where the corresponding await rule is used. Theorem 7.3 shows that our logic is sound in that it guarantees linearizability and partial deadlock freedom (PDF) of concurrent objects. It also ensures partial starvation freedom (PSF) if the rely/guarantee conditions specify only level-0 actions, as required by R ⇒ ⌊R⌋0 and G ⇒ ⌊G⌋0. That is, none of the object actions of a thread could delay the progress of other threads. With the specialized R and G, we can derive the progress of each single thread, which gives us PSF. Theorem 7.3 (Soundness). If D,R,G ⊢χ {P}Π : Γ and φ ⇒ P, then (1) both Π ≼ lin φ Γ and PDFχ φ,Γ (Π) hold; and (2) if R ⇒ ⌊R⌋0 and G ⇒ ⌊G⌋0, then PSFχ φ,Γ (Π) holds. where χ ∈ {sfair,wfair}, and φ ⇒P def = ∀σ,Σ. (φ(σ )=Σ) =⇒ (σ,Σ) |=P. Proofs of the theorem are in Appendix B. We first prove the logic establishes the progress-aware contextual refinements, and then apply the Abstraction Theorem 6.2 to ensure linearizability and the progress properties. The proof structure is similar to the one for LiLi. 8 EXAMPLES We have applied the program logic to verify ticket locks [Mellor-Crummey and Scott 1991], test-andset locks [Herlihy and Shavit 2008], bounded partial queues with two locks [Herlihy and Shavit 2008] (where the locks are implemented using the specification (2.3)) and Treiber stacks [Treiber 1986] with partial pop methods. Perhaps interestingly, we also use our logic to prove that, for the atomic partial specification Γ for locks, the wrapping of Γ (as the object implementation) respects Γ itself as the atomic specification under the designated fairness conditions, i.e., D,R,G ⊢ {P}wr χ Prog (Γ) : Γ holds for certain D, R, G and P, and for different combinations of fairness χ and progress Prog. This result validates our wrappers and program logic. It shows Progχ φ,Γ (wr χ Prog (Γ)) holds, i.e., each wrapper itself satisfies the corresponding progress property. Below we show the proofs for testand-set locks, ticket locks, and simple locks implemented using await which guarantee PSF under weak fairness. The proofs of other examples are given in Appendix C. 8.1 Test-and-Set Locks In Fig. 11, we verify PDF of the test-and-set locks using our logic with the atomic partial specifications L_ACQ' and L_REL defined in (2.3). To distinguish the variables at the two levels, below we use capital letters (e.g., L) in the specifications and small letters (e.g., l) in the implementations. As we explained in Sec. 3, the method L_rel and the specification L_REL have annotated preconditions (l = cid) and (L = cid), respectively. That is, it is not allowed to call L_rel (or L_REL) when the thread does not hold the lock. The annotated precondition for L_acq and L_ACQ' is true. In Fig. 11, we define the assertion lock as the object invariant P used in the obj rule. Then the method L_acq is verified with the precondition lock, and L_rel is verified with the precondition lock ∧ (l = cid) which is reduced to lockedBycid, as shown in Fig. 11. To verify L_acq, we make the following key observations. When the cas at line 3 succeeds, L_ACQ' must be enabled and can be executed correspondingly. And at the time when the cas fails, L_ACQ' must be disabled. The progress of L_acq relies on that the environment thread holding the lock could eventually release the lock, i.e., turning the current thread’s L_ACQ' from disabled to enabled. But such an action is not “definite”, since the client thread may never call the L_rel , Vol. 1, No. 1, Article . Publication date: January 2018