6.The LRG Logic The FRAME rule allows us to verify C with local specifications. and reuse it in contexts where some extra resource r(i.e..the frame) As in SAGL/RGSep.we also split program states into private and shared parts,but the partition is logical and we do not change our is used.The frame r contains both private and shared parts.Since C does not access it,the validity of r is preserved at the end as long as model of states defined in Fig.4.Our logic ensures that each thread ris stable with respect to R*ld,R for the shared part and ld for the has exclusive access to its private resource.The rely/guarantee private.We also require that R'and G'be fenced by the (precise) conditions only specify transitions over shared resources. invariant /'and that the shared part in the frame satisfy /'Here If a statement C only accesses the private resource,it can be G'is the thread's guaranteed transition over the extra shared part. verified as sequential programs using a set of sequential rules,as Since G'is fenced by I',we know the identity transition made by shown in Fig.12.The judgment for well-formed sequential pro- C over r indeed satisfies G'.This frame rule is more general than grams is in the form of (p)C (g).The rules are mostly standard the two frame rules in Sec.3 for shared and private resources.As Separation Logic rules except that program variables are treated as we will explain later,they can be derived from this rule. resources,following Parkinson et al.(2006).Note that,to prove If C knows that the part of the shared resources specified by R', Ip)C (gl,C cannot contain atomic statements and parallel compo- G'and I'is actually not accessed by the outside world,it can leave sitions. this part unspecified by applying the HIDE rule.The HIDE rule is sim- ilar to its prototype shown in Sec.3.Note that we do not use two 6.1 Rules for Concurrency Verification assertions for private and shared resources respectively and use the invariant to determine their boundary instead,therefore changing If the statement C shares resources with its environment,we need the invariant from /*/to introduces an implicit conversion of to consider its interaction with the environment and verify it using resources from shared to private.This conversion is explicit in the the set of rules for concurrency,shown in Fig.13.The judgment prototyping rule in Sec.3.The advantage of not using two asser- for well-formed statements C in a concurrent setting is in the form tions is that we can easily share information in the specifications for of R;G;/Ip)Cgl.R and G are rely/guarantee conditions. private and shared resources.As usual,the hiding rule also requires They are fenced by the invariant I.p and g are pre-and post- R and G be fenced by the precise invariant / conditions.R.G and only specify shared resources,but p and q here specify the whole state.Unlike SAGL/RGSep,we do not As mentioned in Sec.3.a thread cannot abuse the freedom distinguish private and shared resources syntactically in assertions provided by the HIDE rule by hiding the resources that are indeed Instead,their boundary can be determined by the invariant / shared.The inappropriate hiding can be detected at the time of par- allel compositions.From the PAR rule we can see that the private re- The ENv rule allows us to convert the judgment (p)Clgl into source p of Ci needs to be composed linearly using the separating the concurrent form.If C only accesses the private resources and conjunction with both the private (p2)and the shared (r)resources is "well-behaved"sequentially,it is well-behaved in a concurrent used by C2.If CI cheats by converting part of r into p using the setting where there is no resource sharing.Here the rely/guarantee HIDE rule,the linearity would be broken and the precondition after conditions are Emp and the invariant is emp,showing the shared parallel composition would be unsatisfiable. resource is empty.This rule itself is not very useful since it does not allow resource sharing.but a more interesting rule can be derived The p-Ex rule introduces existential quantification over specifi- from this rule and the frame rule shown below. cations.The conjunction rule (P-coN)is sound in LRG.The P-DIS rule is a standard disjunction rule.The consequence rule(cso)al- The AroMic rule first requires that the state contain the resource lows adaptations of different part of the specifications. used to evaluate B (as explained in Sec.5,B=B is no longer a tautology when variables are treated as resources).Since the It is important to note that,like RGSep,we do not have concur- execution of C cannot be interrupted by the environment,we can rency rules for primitive statements,therefore they either only ac- treat the whole state as private resource and verify C using the cess the private resource or access the shared part inside the atomic block (where the shared resource has been converted into private). sequential rules.Outside of the atomic block,p and g need to be stable with respect to R*ld,R for the shared resource and ld for the 6.2 Derived Rules private (i.e.,the environment does not touch the private resource) The transition p g consists of sub-transitions over shared and In Fig.14,we show several useful rules that can be derived from private resources.The one over shared needs to satisfy G.and the the basic set of rules.The ENV-SHARE rule is similar to the ENv rule private one can be arbitrary (i.e.,True).The rule also requires that in Fig.13,but allows resource sharing with the environment.It is the shared resource be well-formed with respect to the invariant derived from the ENV rule and the FRAME rule. (i.e..pvg=I*true).and that R/G be fenced by 1.To have a concise presentation,we use Sta(r,rR)as a short hand for The rules FR-PRIVATE and FR-SHARE are frame rules for private Sta(r,R)A Sta(r'R).and IR,G)for (IDR)A(IG).Similar and shared resources respectively,similar to those shown in Sec.3 representations are used in the remaining part of the paper. They are derived from the FRAME rule.To get FR-PRIVATE,we simply instantiate R'and G'with Emp and /with emp in the FRAME rule The P-SEo rule for sequential composition is the same as in The FR-SHARE rule is similar to the FRAME rule,except r contains standard Rely-Guarantee reasoning and does not need explanation only shared resource. In the rules P-WHILE and P-IF,we require that the resource needed to evaluate B be available in p but disjoint with the shared resource in The PAR-HIDE rule is a generalization of the PAR rule.The parent 1,i.e.,it is in the private part.Therefore,the validity of B would not thread has private resource p*p2*m and shares the resource r be affected by the environment. with its environments.P and p2 are distributed to CI and C2 respectively as their private resources.m and r are shared by them The PAR rule is similar to the one in RGSep shown in Sec.2.3 The guarantees about the use of m by the two processes are G and The parent thread distribute pi and p2 to the children CI and C2 G2 respectively,which are fenced by I'.Since m is private resource respectively as their private resources.The resource r is shared by of the parent thread,the sharing between children threads does not them.We require that r,ri and r2 imply /i.e.,the shared resource need to be exposed to the environments.Thus R,GI and G2 only is well-formed.Also R needs to be fenced by 1. specify transitions over the resource specified by r.They are fenced6. The LRG Logic As in SAGL/RGSep, we also split program states into private and shared parts, but the partition is logical and we do not change our model of states defined in Fig. 4. Our logic ensures that each thread has exclusive access to its private resource. The rely/guarantee conditions only specify transitions over shared resources. If a statement C only accesses the private resource, it can be verified as sequential programs using a set of sequential rules, as shown in Fig. 12. The judgment for well-formed sequential pro￾grams is in the form of {p} C {q}. The rules are mostly standard Separation Logic rules except that program variables are treated as resources, following Parkinson et al. (2006). Note that, to prove {p} C {q}, C cannot contain atomic statements and parallel compo￾sitions. 6.1 Rules for Concurrency Verification If the statement C shares resources with its environment, we need to consider its interaction with the environment and verify it using the set of rules for concurrency, shown in Fig. 13. The judgment for well-formed statements C in a concurrent setting is in the form of R; G; I  {p} C {q}. R and G are rely/guarantee conditions. They are fenced by the invariant I. p and q are pre- and post￾conditions. R, G and I only specify shared resources, but p and q here specify the whole state. Unlike SAGL/RGSep, we do not distinguish private and shared resources syntactically in assertions. Instead, their boundary can be determined by the invariant I. The env rule allows us to convert the judgment {p} C {q} into the concurrent form. If C only accesses the private resources and is “well-behaved” sequentially, it is well-behaved in a concurrent setting where there is no resource sharing. Here the rely/guarantee conditions are Emp and the invariant is emp, showing the shared resource is empty. This rule itself is not very useful since it does not allow resource sharing, but a more interesting rule can be derived from this rule and the frame rule shown below. The atomic rule first requires that the state contain the resource used to evaluate B (as explained in Sec. 5, B = B is no longer a tautology when variables are treated as resources). Since the execution of C cannot be interrupted by the environment, we can treat the whole state as private resource and verify C using the sequential rules. Outside of the atomic block, p and q need to be stable with respect to R∗ Id, R for the shared resource and Id for the private (i.e., the environment does not touch the private resource). The transition p  q consists of sub-transitions over shared and private resources. The one over shared needs to satisfy G, and the private one can be arbitrary (i.e., True). The rule also requires that the shared resource be well-formed with respect to the invariant (i.e., p ∨ q ⇒ I ∗ true), and that R/G be fenced by I. To have a concise presentation, we use Sta({r,r },R) as a short hand for Sta(r,R) ∧ Sta(r ,R), and I  {R,G} for (I  R) ∧ (I  G). Similar representations are used in the remaining part of the paper. The p-seq rule for sequential composition is the same as in standard Rely-Guarantee reasoning and does not need explanation. In the rules p-while and p-if, we require that the resource needed to evaluate B be available in p but disjoint with the shared resource in I, i.e., it is in the private part. Therefore, the validity of B would not be affected by the environment. The par rule is similar to the one in RGSep shown in Sec. 2.3. The parent thread distribute p1 and p2 to the children C1 and C2 respectively as their private resources. The resource r is shared by them. We require that r, r1 and r2 imply I, i.e., the shared resource is well-formed. Also R needs to be fenced by I. The frame rule allows us to verify C with local specifications, and reuse it in contexts where some extra resource r (i.e., the frame) is used. The frame r contains both private and shared parts. Since C does not access it, the validity of r is preserved at the end as long as r is stable with respect to R ∗Id, R for the shared part and Id for the private. We also require that R and G be fenced by the (precise) invariant I , and that the shared part in the frame satisfy I . Here G is the thread’s guaranteed transition over the extra shared part. Since G is fenced by I , we know the identity transition made by C over r indeed satisfies G . This frame rule is more general than the two frame rules in Sec. 3 for shared and private resources. As we will explain later, they can be derived from this rule. If C knows that the part of the shared resources specified by R , G and I is actually not accessed by the outside world, it can leave this part unspecified by applying the hide rule. The hide rule is sim￾ilar to its prototype shown in Sec. 3. Note that we do not use two assertions for private and shared resources respectively and use the invariant to determine their boundary instead, therefore changing the invariant from I ∗ I to I introduces an implicit conversion of resources from shared to private. This conversion is explicit in the prototyping rule in Sec. 3. The advantage of not using two asser￾tions is that we can easily share information in the specifications for private and shared resources. As usual, the hiding rule also requires R and G be fenced by the precise invariant I. As mentioned in Sec. 3, a thread cannot abuse the freedom provided by the hide rule by hiding the resources that are indeed shared. The inappropriate hiding can be detected at the time of par￾allel compositions. From the par rule we can see that the private re￾source p1 of C1 needs to be composed linearly using the separating conjunction with both the private (p2) and the shared (r) resources used by C2. If C1 cheats by converting part of r into p1 using the hide rule, the linearity would be broken and the precondition after parallel composition would be unsatisfiable. The p-ex rule introduces existential quantification over specifi- cations. The conjunction rule (p-conj) is sound in LRG. The p-disj rule is a standard disjunction rule. The consequence rule (csq) al￾lows adaptations of different part of the specifications. It is important to note that, like RGSep, we do not have concur￾rency rules for primitive statements, therefore they either only ac￾cess the private resource or access the shared part inside the atomic block (where the shared resource has been converted into private). 6.2 Derived Rules In Fig. 14, we show several useful rules that can be derived from the basic set of rules. The env-share rule is similar to the env rule in Fig. 13, but allows resource sharing with the environment. It is derived from the env rule and the frame rule. The rules fr-private and fr-share are frame rules for private and shared resources respectively, similar to those shown in Sec. 3. They are derived from the frame rule. To get fr-private, we simply instantiate R and G with Emp and I with emp in the frame rule. The fr-share rule is similar to the frame rule, except r contains only shared resource. The par-hide rule is a generalization of the par rule. The parent thread has private resource p1 ∗ p2 ∗ m and shares the resource r with its environments. p1 and p2 are distributed to C1 and C2 respectively as their private resources. m and r are shared by them. The guarantees about the use of m by the two processes are G 1 and G 2 respectively, which are fenced by I . Since m is private resource of the parent thread, the sharing between children threads does not need to be exposed to the environments. Thus R, G1 and G2 only specify transitions over the resource specified by r. They are fenced 8