[E1,ply[E2,q] 上：{t一(h,E1)*p)linself{t一(end,E2)*q} ·(LINSELF) (LINSELF-END F:{t一(end,E)linself{t一(end,E)} [E1.ply[E2,91 h{E一，B)*p)trylin(E)E一(，E)*p)⊕(E一(emd,E2)*g(任R) SpecExact(p) p→p (TRY-END) ·(COMMIT) Ft{E一(end,E')trylin(E)HE一(end,E')} Ft ip'true}commit(p)p' 上t{p}C{q} (FRAME】 (p)(}(SPEc-CoN) F:{t一(end,E)}E[return E]{t-(end,E》 (RET) 上t{p*r}C{q*r} :{p⊕p'Cg⊕g} Ht (p}C(g}(px q)=G*True [l,G,I上t{p}(C){g pVg÷I*true Sta({p,q},R+ld)IR (ATOM) (ATOM-R) [,G,IF:{p}C){q} R,G,IF {p}(CHa} Figure 10.Selected Inference Rules trylin(E)command introduces speculations about the thread E. Rely and guarantee assertions specify transitions over Here When we have enough knowledge p about the situation of the ab- we follow the syntax of LRG [8].with a new assertion R R2 stract objects and operations,the commit(p)step keeps only the specifying speculative behaviors of the environment.The semantics subset of speculations consistent with p and drops the rest.Here p is given in Fig.9.We will show the use of the assertions in the is a logical assertion about the state >which is explained below. examples of Sec.6. 4.2 Assertions 4.3 Inference Rules Syntax of assertions is shown in Fig.7.Following rely-guarantee The rules of our logic are shown in Fig.10.Rules on the top half are style reasoning,assertions are either single state assertions p and g for sequential Hoare-style reasoning.They are proposed to verify or binary rely/guarantee conditions R and G.Note here states refer code C in the atomic block(C).The judgment is parameterized to the relational states X. with the id t of the current thread. We use standard separation logic assertions such as true,E1= For the linself command,if the abstract operation of the cur- E2,emp and E E2 to specify the memory o.As shown in rent thread has not been done,this command will finish it.Here Fig.8,their semantics is almost standard,but for E=E2 to hold [E1,p]E2,g]in the LINSELF rule describes the behavior of y. over o we require the domain of o contains only the free variables which transforms abstract objects satisfying p to new ones satisfy- in Ei and E2.Here we use E to evaluate E with the extra ing q.E and E2 are the argument and return value respectively. requirement that o contains the exact resource to do the evaluation. The definition is given in Fig.9.The LINSELF-END rule says linself New assertions are introduced to specify A.E specifies has no effects if we know the abstract operation has been finished the abstract object 0 in A,with no speculations of U (abstract The LIN rule and LIN-END rule are similar and omitted here. operations).while E1(,E2)(and E1(end,E2))specifies The TRY rule says that if the thread E has not finished the the singleton speculation of U.Semantics of separating conjunction abstract operation y,it can do speculation using trylin(E).The p*q is similar as in separation logic,except that it is now lifted resulting state contains both cases,one says does not progress to assertions over the relational states Note that the underlying at this point and the other says it does.If the current thread has “disjoint union”over△for separating conjunction should not be already finished the abstract operation,trylin(E)would have no confused with the normal disjoint union operator over sets.The effects,as shown in the TRY-END rule.We omit the TRYSELF rule former (denoted as A1*A2 in Fig.8)describes the split of pending and TRYSELF-END rule for the current thread,which are similar. thread pools and/or abstract objects.For example,the left side A in The above two pairs of rules require us to know for sure either the following equation specifies two speculations of threads ti and the abstract operation has been finished or not.If we want to t2(we assume the abstract object part is empty and omitted here) support uncertainty in the pre-condition,we could first consider and it can be split into two sets A and A2 on the right side,each different cases and then apply the SPEC-CONJ rule,which is like of which describes the speculations of a single thread. the conjunction rule in traditional Hoare logic. {t1Y1□} The COMMIT rule allows us to commit to a specific speculation and drop the rest.commit(p)keeps only the speculations satisfy- 1t2T2 {t2T2,t2T幻} ing p.We require p to describe an exact set of speculations,as de- fined by SpecExact(p)in Fig.8.For example,the following p is The most interesting new assertion is p g,where p and q speculation-exact,while p2 is not: specify two different speculations.It is this assertion that reflects uncertainty about the abstract level.However,the readers should ph兰t一(，n)⊕t一(end,n) not confuse with disjunction.It is more like conjunction since it 2兰t一(，n)vt一(end,n' says A contains both speculations satisfying p and those satisfying In all of our examples in Sec.6,the assertion p in commit(p) g.As an example,the above equation could be formulated at the describes a singleton speculation,so SpecExact(p)trivially holds. assertion level using*and⊕： Before the current thread returns,it must know its abstract (t1一Y1*t2一Y2)⊕(t1一Y1*t2一Y2) operation has been done,as required in the RET rule.We also have t1→Y1*(t2→Y2⊕t2一T%) a standard FRAME rule as in separation logic for local reasoning. 465[E1, p]γ[E2, q] t {t (γ,E1) ∗ p}linself{t (end, E2) ∗ q} (LINSELF) t {t (end, E)}linself{t (end, E)} (LINSELF-END) [E1, p]γ[E2, q] t {E (γ,E1) ∗ p}trylin(E){(E (γ,E1) ∗ p) ⊕ (E (end, E2) ∗ q)} (TRY) t {E (end, E )}trylin(E){E (end, E )} (TRY-END) SpecExact(p) p ⇒ p t {p ⊕ true}commit(p){p } (COMMIT) t {t (end, E)}E[ return E ]{t (end, E)} (RET) t {p}C{q} t {p ∗ r}C{q ∗ r} (FRAME) t {p}C{q} t {p }C{q } t {p ⊕ p }C{q ⊕ q } (SPEC-CONJ) t {p}C{q} (p q) ⇒ G ∗ True I G p ∨ q ⇒ I ∗ true [I], G, I t {p}C{q} (ATOM) [I], G, I t {p}C{q} Sta({p, q}, R ∗ Id) I R R, G, I t {p}C{q} (ATOM-R) Figure 10. Selected Inference Rules trylin(E) command introduces speculations about the thread E. When we have enough knowledge p about the situation of the ab￾stract objects and operations, the commit(p) step keeps only the subset of speculations consistent with p and drops the rest. Here p is a logical assertion about the state Σ, which is explained below. 4.2 Assertions Syntax of assertions is shown in Fig. 7. Following rely-guarantee style reasoning, assertions are either single state assertions p and q or binary rely/guarantee conditions R and G. Note here states refer to the relational states Σ. We use standard separation logic assertions such as true, E1 = E2, emp and E1 → E2 to specify the memory σ. As shown in Fig. 8, their semantics is almost standard, but for E1 = E2 to hold over σ we require the domain of σ contains only the free variables in E1 and E2. Here we use {{E}}σ to evaluate E with the extra requirement that σ contains the exact resource to do the evaluation. New assertions are introduced to specify Δ. x ⇒ E specifies the abstract object θ in Δ, with no speculations of U (abstract operations), while E1 (γ,E2) (and E1 (end, E2)) specifies the singleton speculation of U. Semantics of separating conjunction p ∗ q is similar as in separation logic, except that it is now lifted to assertions over the relational states Σ. Note that the underlying “disjoint union” over Δ for separating conjunction should not be confused with the normal disjoint union operator over sets. The former (denoted as Δ1 ∗Δ2 in Fig. 8) describes the split of pending thread pools and/or abstract objects. For example, the left side Δ in the following equation specifies two speculations of threads t1 and t2 (we assume the abstract object part is empty and omitted here), and it can be split into two sets Δ1 and Δ2 on the right side, each of which describes the speculations of a single thread. t1 Υ1 t2 Υ2 , t1 Υ1 t2 Υ 2  = { t1 Υ1 } ∗ { t2 Υ2 , t2 Υ 2 } The most interesting new assertion is p ⊕ q, where p and q specify two different speculations. It is this assertion that reflects uncertainty about the abstract level. However, the readers should not confuse ⊕ with disjunction. It is more like conjunction since it says Δ contains both speculations satisfying p and those satisfying q. As an example, the above equation could be formulated at the assertion level using ∗ and ⊕: (t1 Υ1 ∗ t2 Υ2) ⊕ (t1 Υ1 ∗ t2 Υ 2) ⇔ t1 Υ1 ∗ (t2 Υ2 ⊕ t2 Υ 2) Rely and guarantee assertions specify transitions over Σ. Here we follow the syntax of LRG [8], with a new assertion R1 ⊕ R2 specifying speculative behaviors of the environment. The semantics is given in Fig. 9. We will show the use of the assertions in the examples of Sec. 6. 4.3 Inference Rules The rules of our logic are shown in Fig. 10. Rules on the top half are for sequential Hoare-style reasoning. They are proposed to verify code C in the atomic block C. The judgment is parameterized with the id t of the current thread. For the linself command, if the abstract operation γ of the cur￾rent thread has not been done, this command will finish it. Here [E1, p]γ[E2, q] in the LINSELF rule describes the behavior of γ, which transforms abstract objects satisfying p to new ones satisfy￾ing q. E1 and E2 are the argument and return value respectively. The definition is given in Fig. 9. The LINSELF-END rule says linself has no effects if we know the abstract operation has been finished. The LIN rule and LIN-END rule are similar and omitted here. The TRY rule says that if the thread E has not finished the abstract operation γ, it can do speculation using trylin(E). The resulting state contains both cases, one says γ does not progress at this point and the other says it does. If the current thread has already finished the abstract operation, trylin(E) would have no effects, as shown in the TRY-END rule. We omit the TRYSELF rule and TRYSELF-END rule for the current thread, which are similar. The above two pairs of rules require us to know for sure either the abstract operation has been finished or not. If we want to support uncertainty in the pre-condition, we could first consider different cases and then apply the SPEC-CONJ rule, which is like the conjunction rule in traditional Hoare logic. The COMMIT rule allows us to commit to a specific speculation and drop the rest. commit(p) keeps only the speculations satisfy￾ing p. We require p to describe an exact set of speculations, as de- fined by SpecExact(p) in Fig. 8. For example, the following p1 is speculation-exact, while p2 is not: p1 def = t (γ,n) ⊕ t (end, n ) p2 def = t (γ,n) ∨ t (end, n ) In all of our examples in Sec. 6, the assertion p in commit(p) describes a singleton speculation, so SpecExact(p) trivially holds. Before the current thread returns, it must know its abstract operation has been done, as required in the RET rule. We also have a standard FRAME rule as in separation logic for local reasoning. 465