(RelAssn)P,Q,J:=B|emp|E→E|E→E pP+QI PAQ I PVQ 1... G:=(a,) (a,)y(a',)兽(a世a',∑出) where (s,h)w(s',h')(s,hwh'),if s=s' (RelAct)R.G:=PxkQI [P]I D ILGJo I GAG I GVG 1... (s,h),(s,h)=B iff [B]sws true (DAct) D :=PMQ Vr.D DAD ((s,h),(s,h))F emp iff dom(h)=dom(h)= (FullAssn) P,9 P|arem(C).|◇(E).|◆(Ek,.,E1) I Lplo I p*q I pAg I pVq l... (s,h),(s,)卡E1→E2iffh={IE]w[E2lss} (s,h),(s,h)FE1÷E2ifh={[E1lsWs+IE2lsw】 Figure 4.Syntax of the assertion language. SEP*Q iff361,G2.G=G1出G2 A(61EP)A(62EQ) setting.Here P is a relational assertion that specifies the consistency (a)semantics of relational state assertions P and Q relation between the concrete data representation and the abstract (6,6')EPKkQ iff (6EP)A(6'EQ) value.Similarly,R and G lift regular rely and guarantee conditions to the binary setting,which now specify transitions of states at both (s,G)=[P]if(6'=6)A(6=P) the concrete level and the abstract level.The definite action D is a (b)semantics of relational rely/guarantee assertions R and G special form of state transitions used for progress reasoning.The definitions of P,R,G and D are shown in Sec.4.1. (G,(u,),C)=P iff 6P Note LiLi is a logic for concurrent objects II only.We do not ((u,w),C)E arem(C)iff C=C provide logic rules for clients.See Sec.5 for more discussions. To simplify the presentation in this paper,we describe LiLi based (6,(u,w),C)上◇(E)if3n.(Els.s=n)A(n≤w) on the plain Rely-Guarantee Logic [18].Also,to avoid "variables as (6,(u,w),C)=◆(Ek,E)if(IE6.$,IE1l6.s)≤u resources"[27],we assume program variables are either thread-local ((u,w),C)EIplo i f3w.(6,(u,w),C)卡p or read-only.The full version of LiLi (see TR [22])extends the more 6卡pl iff 3u,w,C.(,(u,w),C)Fp advanced Rely-Guarantee-based logic LRG [7]to support dynamic allocation and ownership transfer.It also drops the assumption about Cwc些CifC=skip CifC”=skip program variables. (6,(u,w),C)u(G',(u,r),C)兽(su6',(u+',e+'),CuC) 4.1 Assertions (c)semantics of full assertions p and g We define assertions in Fig.4.The relational state assertions P and O specify the relationship between the concrete state o and the Figure 5.Semantics of assertions abstract state X.Here we use s and h for the store and the heap at the abstract level (see Fig.3).For simplicity,we assume the program variables used in the concrete code are different from those in the (u,w)records the numbers of various tokens and It serves abstract code (e.g.,we use x and X at the concrete and abstract levels as a well-founded metric for our progress reasoning.Informally w respectively).We use the relational state 6 to represent the pair of specifies the upper bound of the number of loop rounds that the states (o,>)as defined in Fig.5. current thread can execute if it is neither blocked nor delayed by its Figure 5(a)defines semantics of state assertions.The boolean environment.The assertion (E)says the number w of O-tokens is expression B holds if it evaluates to true at the combined store no less than E.Therefore ()always holds,and (n+1)implies of s and s.emp describes empty heaps.The assertion EE2 (n)for any n.We postpone the explanation of u and the assertion specifies a singleton heap at the concrete level with the value of (E,...,E1)to Sec.4.3.Below we use as the shorthand for the expression E2 stored at the location E.Its counterpart for (1).We use po to ignore the descriptions in p about the number an abstract level heap is represented as E E2.Semantics of of -tokens.p converts p back to a relational state assertion. separating conjunction P*Q is similar as in separation logic,except Separating conjunction p g has the standard meaning as in that it is now lifted to relational states 6.The disjoint union of two separation logic,which says p and g hold over disjoint parts of relational states is defined at the top of the figure.Semantics of the ((u,w),C)respectively (the formal definition elided here).The assertion p will be defined latter (see Fig.5(c)). disjoint union is defined in Fig.5(c).The disjoint union of the Rely/guarantee assertions R and G specify the transitions over numbers of tokens is the sum of them.The disjoint union of C the relational states 6.Their semantics is defined in Fig.5(b).The and C2 is defined only if at least one of them is skip.Therefore we action P says that the initial relational states satisfy P and the know the following holds (for any P and C): resulting states satisfy Q.We can ignore the index k for now,which is used to stratify actions that may delay the progress of other threads (P A arem(C)A)*(A emp)(P A arem(C)A(2)) and will be explained in Sec.4.3.[P]specifies identity transitions with the initial states satisfying P.Semantics of Go is defined Definite actions.Fig.4 also defines definite actions D,which in Sec.4.3 too (see Fig.10).Below we use P Q as a shorthand can be treated as special forms of rely/guarantee conditions.Their for P o Q.We also use ld for [true],which represents arbitrary semantics is given in Fig.6(a).PO specifies the transitions identity transitions. where the final states satisfy Q if the initial states satisfy P.It is We further instrument the relational state assertions with the different from P x O in that PO does not restrict the transitions specifications of the abstract level code and various tokens.The if initially P does not hold.Consider the following example D. resulting full assertions p and g are defined in Fig.4,whose semantics is given in Fig.5(c).The assertion p is interpreted Dx兰n.(x→n)A(n>0)》(x→n+1) over ((u,w),C).C is the abstract-level code that remains to D.describes the state transitions which increment x if x is positive be refined.It is specified by the assertion arem(C).Since our initially.It is satisfied by any transitions where initially x is not logic verifies linearizability of objects,C is always in the form positive.The conjunction DiA D2 is useful for enumerating definite of atomic commands(C)(ahead of return commands).The pair actions.For instance,when the program uses two locks L1 and L2, 390(RelAssn) P, Q, J ::= B | emp | E 7→ E | E Z⇒ E | TpU | P ∗ Q | P ∧ Q | P ∨ Q | . . . (RelAct) R, G ::= P nk Q | [P] | D | bGc0 | G ∧ G | G ∨ G | . . . (DAct) D ::= P ❀ Q | ∀x. D | D ∧ D (FullAssn) p, q ::= P | arem(C) | ♦(E) | (Ek, . . . , E1) | bpc♦ | p ∗ q | p ∧ q | p ∨ q | . . . Figure 4. Syntax of the assertion language. setting. Here P is a relational assertion that specifies the consistency relation between the concrete data representation and the abstract value. Similarly, R and G lift regular rely and guarantee conditions to the binary setting, which now specify transitions of states at both the concrete level and the abstract level. The definite action D is a special form of state transitions used for progress reasoning. The definitions of P, R, G and D are shown in Sec. 4.1. Note LiLi is a logic for concurrent objects Π only. We do not provide logic rules for clients. See Sec. 5 for more discussions. To simplify the presentation in this paper, we describe LiLi based on the plain Rely-Guarantee Logic [18]. Also, to avoid “variables as resources” [27], we assume program variables are either thread-local or read-only. The full version of LiLi (see TR [22]) extends the more advanced Rely-Guarantee-based logic LRG [7] to support dynamic allocation and ownership transfer. It also drops the assumption about program variables. 4.1 Assertions We define assertions in Fig. 4. The relational state assertions P and Q specify the relationship between the concrete state σ and the abstract state Σ. Here we use s and h for the store and the heap at the abstract level (see Fig. 3). For simplicity, we assume the program variables used in the concrete code are different from those in the abstract code (e.g., we use x and X at the concrete and abstract levels respectively). We use the relational state S to represent the pair of states (σ, Σ), as defined in Fig. 5. Figure 5(a) defines semantics of state assertions. The boolean expression B holds if it evaluates to true at the combined store of s and s. emp describes empty heaps. The assertion E1 7→ E2 specifies a singleton heap at the concrete level with the value of the expression E2 stored at the location E1. Its counterpart for an abstract level heap is represented as E1 Z⇒ E2. Semantics of separating conjunction P ∗Q is similar as in separation logic, except that it is now lifted to relational states S. The disjoint union of two relational states is defined at the top of the figure. Semantics of the assertion TpU will be defined latter (see Fig. 5(c)). Rely/guarantee assertions R and G specify the transitions over the relational states S. Their semantics is defined in Fig. 5(b). The action P nk Q says that the initial relational states satisfy P and the resulting states satisfy Q. We can ignore the index k for now, which is used to stratify actions that may delay the progress of other threads and will be explained in Sec. 4.3. [P] specifies identity transitions with the initial states satisfying P. Semantics of bGc0 is defined in Sec. 4.3 too (see Fig. 10). Below we use P n Q as a shorthand for P n0 Q. We also use Id for [true], which represents arbitrary identity transitions. We further instrument the relational state assertions with the specifications of the abstract level code and various tokens. The resulting full assertions p and q are defined in Fig. 4, whose semantics is given in Fig. 5(c). The assertion p is interpreted over (S,(u, w), C). C is the abstract-level code that remains to be refined. It is specified by the assertion arem(C). Since our logic verifies linearizability of objects, C is always in the form of atomic commands hC 0 i (ahead of return commands). The pair S ::= (σ, Σ) (σ, Σ) ] (σ 0 , Σ0 ) def = (σ ] σ 0 , Σ ] Σ0 ) where (s, h)](s 0 , h0 ) def = (s, h]h 0 ) , if s=s 0 ((s, h), (s, h)) |= B iff JBKs]s = true ((s, h), (s, h)) |= emp iff dom(h) = dom(h) = ∅ ((s, h), (s, h)) |= E1 7→ E2 iff h = {JE1Ks]s ❀ JE2Ks]s} ((s, h), (s, h)) |= E1 Z⇒ E2 iff h = {JE1Ks]s ❀ JE2Ks]s} S |= P ∗ Q iff ∃S1, S2. S = S1 ] S2 ∧(S1 |= P) ∧ (S2 |= Q) (a) semantics of relational state assertions P and Q (S, S0 ) |= P nk Q iff (S |= P) ∧ (S0 |= Q) (S, S0 ) |= [P] iff (S0 = S) ∧ (S |= P) (b) semantics of relational rely/guarantee assertions R and G (S, (u, w), C) |= P iff S |= P (S, (u, w), C) |= arem(C0 ) iff C = C0 (S, (u, w), C) |= ♦(E) iff ∃n. (JEKS.s = n) ∧ (n ≤ w) (S, (u, w), C) |= (Ek, . . . , E1) iff (JEkKS.s, . . . , JE1KS.s) ≤ u (S, (u, w), C) |= bpc♦ iff ∃w0 . (S, (u, w0 ), C) |= p S |= TpU iff ∃u, w, C. (S, (u, w), C) |= p C ] C0 def =  C0 if C = skip C if C0 = skip (S, (u, w), C)](S0 , (u 0 , w0 ), C0 ) def = (S]S0 , (u+u 0 , w+w0 ), C]C0 ) (c) semantics of full assertions p and q Figure 5. Semantics of assertions. (u, w) records the numbers of various tokens  and ♦. It serves as a well-founded metric for our progress reasoning. Informally w specifies the upper bound of the number of loop rounds that the current thread can execute if it is neither blocked nor delayed by its environment. The assertion ♦(E) says the number w of ♦-tokens is no less than E. Therefore ♦(0) always holds, and ♦(n + 1) implies ♦(n) for any n. We postpone the explanation of u and the assertion (Ek, . . . , E1) to Sec. 4.3. Below we use ♦ as the shorthand for ♦(1). We use bpc♦ to ignore the descriptions in p about the number of ♦-tokens. TpU converts p back to a relational state assertion. Separating conjunction p ∗ q has the standard meaning as in separation logic, which says p and q hold over disjoint parts of (S,(u, w), C) respectively (the formal definition elided here). The disjoint union is defined in Fig. 5(c). The disjoint union of the numbers of tokens is the sum of them. The disjoint union of C1 and C2 is defined only if at least one of them is skip. Therefore we know the following holds (for any P and C): (P ∧ arem(C) ∧ ♦) ∗ (♦ ∧ emp) ⇔ (P ∧ arem(C) ∧ ♦(2)) Definite actions. Fig. 4 also defines definite actions D, which can be treated as special forms of rely/guarantee conditions. Their semantics is given in Fig. 6(a). P ❀ Q specifies the transitions where the final states satisfy Q if the initial states satisfy P. It is different from P nQ in that P ❀ Q does not restrict the transitions if initially P does not hold. Consider the following example Dx. Dx def = ∀n. ((x 7→ n) ∧ (n > 0)) ❀ (x 7→ n + 1) Dx describes the state transitions which increment x if x is positive initially. It is satisfied by any transitions where initially x is not positive. The conjunction D1∧D2 is useful for enumerating definite actions. For instance, when the program uses two locks L1 and L2, 390