《计算机科学》相关教学资源（参考文献）Technical Report TTIC-TR-2008-1（Local Rely-Guarantee Reasoning）

TEC Technical Report TTIC-TR-2008-1 LOGICAL INST CHICAGO October 2008 Local Rely-Guarantee Reasoning Xinyu Feng Toyota Technological Institute at Chicago feng@tti-c.org

Technical Report TTIC-TR-2008-1 October 2008 Local Rely-Guarantee Reasoning Xinyu Feng Toyota Technological Institute at Chicago feng@tti-c.org

ABSTRACT Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs.However,it is difficult for users to define rely/guarantee conditions,which specify threads'behaviors over the whole program state.Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it possible to hide thread-local resources,but the shared resources still need to be globally known and specified.This greatly limits the reuse of verified program modules. In this paper,we propose LRG,a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concurrency verification.Our logic,for the first time,supports a frame rule over rely/guarantee conditions so that specifications of program modules only need to talk about the resources used locally,and the verified modules can be reused in different threads without redoing the proof.Moreover,we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system.The support of information hiding not only improves the modularity of Rely-Guarantee reasoning,but also enables the sharing of dynamically allocated resources,which requires adjustment of rely/guarantee conditions

ABSTRACT Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads’ behaviors over the whole program state. Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it possible to hide thread-local resources, but the shared resources still need to be globally known and specified. This greatly limits the reuse of verified program modules. In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concurrency verification. Our logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of program modules only need to talk about the resources used locally, and the verified modules can be reused in different threads without redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the sharing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions

Local Rely-Guarantee Reasoning Xinyu Feng Toyota Technological Institute at Chicago Chicago,IL 60637,U.S.A. feng@tti-c.org Abstract its the reuse of verified program modules in different applica- Rely-Guarantee reasoning is a well-known method for verification tions with different shared resources of shared-variable concurrent programs.However,it is difficult for Since the shared resources need to be globally known,it is dif- users to define rely/guarantee conditions,which specify threads' ficult to support the sharing of dynamically allocated resources, behaviors over the whole program state.Recent efforts to combine which are not known until they are allocated. Separation Logic with Rely-Guarantee reasoning have made it pos- Some resources might be shared only by a subset of threads, sible to hide thread-local resources,but the shared resources still but there is no way to hide them from the rest of threads in the need to be globally known and specified.This greatly limits the system. reuse of verified program modules. In this paper,we propose LRG,a new Rely-Guarantee-based These problems are part of the reasons why Jones(2003)calls for logic that brings local reasoning and information hiding to concur- a more compositional approach to concurrency. rency verification.Our logic,for the first time,supports a frame Recent works on SAGL (Feng et al.2007)and RGSep(Vafeiadis rule over rely/guarantee conditions so that specifications of pro- and Parkinson 2007)have tried to combine the Rely-Guarantee rea- gram modules only need to talk about the resources used locally, soning with Separation Logic(Ishtiaq and O'Hearn 2001:Reynolds and the verified modules can be reused in different threads with- 2002)for better composionality.They split the whole state into out redoing the proof.Moreover,we introduce a new hiding rule to thread-private and shared parts.The partition of resources enforced hide the resources shared by a subset of threads from the rest in the by Separation Logic ensures that each thread cannot touch the pri- system.The support of information hiding not only improves the vate parts of others.The rely and guarantee conditions now only modularity of Rely-Guarantee reasoning,but also enables the shar- need to specify the part that is indeed shared.These combinations, ing of dynamically allocated resources,which requires adjustment however,only address the first problem mentioned above.Since of rely/guarantee conditions. they also require the shared resources to be globally known,the last three problems remain unsolved. 1.Introduction In this paper,we propose a new program logic,LRG,for Local With the development and wide use of multi-core processors,con- Rely-Guarantee reasoning.By addressing all these open problems, currency has become a crucial element in software systems.How our logic makes local reasoning and information hiding a reality ever,the correctness of concurrent programs is notoriously difficult in concurrency verification.Our work is based on previous works to verify because of the non-deterministic interleaving of running on Rely-Guarantee reasoning and Separation Logic,and SAGL and threads and the exponential size of state spaces.Compositionality RGSep in particular,but makes the following new contributions: is of particular importance for scalable concurrency verification. As an extension of Separation Logic,we introduce the sepa- Rely-Guarantee reasoning (Jones 1983)is a well-known method rating conjunction of rely/guarantee conditions.Unlike asser- for verification of shared-variable concurrent programs.It lets each tions in Separation Logic,rely/guarantee conditions are binary thread specify its expectation (the rely condition)of state transi- relations of program states and they specify state transitions. tions made by its environment,and its guarantee to the environment The new separating conjunction allows us to formalize two sub- about transitions made by itself.Since the rely condition specifies transitions conducted over disjoint resources,which is the basis all possible behaviors that might interfere with the thread,we do to bring in all the nice ideas developed in Separation Logic for not need to consider the exponential size of possible interleavings local reasoning and modularity. during the verifications.However,the rely/guarantee conditions are difficult to formulate in practice,because they need to specify the Our logic,for the first time,supports a frame rule over rely and global program state and these global conditions need to be checked guarantee conditions so that the sharing of resources no longer during the execution of the whole thread.Specifically,the compo- needs to be globally known.Specifications of program modules sionality and applicability of Rely-Guarantee reasoning are greatly only need to talk about the resource used locally.therefore the limited by the following problems: verified modules can be reused in different contexts without redoing the proof. The whole program state is viewed as shared resource and need We propose a new rule for hiding the shared resources from to be specified in the rely/guarantee conditions,even if a part the environment.It allows the local sharing of resources among of the state might be privately owned by a single thread.The a subset of threads without exposing them to others in the thread-private resource has to be exposed in the specifications. system.In particular,using the hiding rule we can derive a As part of the specifications of program modules,the rely and more general rule for parallel composition such that a thread's guarantee conditions need to specify all the shared resources, private resource can be shared by its children without being even if the module accesses only part of them locally.This lim- visible by its siblings.The hiding rule also gives us a way to

Local Rely-Guarantee Reasoning Xinyu Feng Toyota Technological Institute at Chicago Chicago, IL 60637, U.S.A. feng@tti-c.org Abstract Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads’ behaviors over the whole program state. Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it pos￾sible to hide thread-local resources, but the shared resources still need to be globally known and specified. This greatly limits the reuse of verified program modules. In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concur￾rency verification. Our logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of pro￾gram modules only need to talk about the resources used locally, and the verified modules can be reused in different threads with￾out redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the shar￾ing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions. 1. Introduction With the development and wide use of multi-core processors, con￾currency has become a crucial element in software systems. How￾ever, the correctness of concurrent programs is notoriously difficult to verify because of the non-deterministic interleaving of running threads and the exponential size of state spaces. Compositionality is of particular importance for scalable concurrency verification. Rely-Guarantee reasoning (Jones 1983) is a well-known method for verification of shared-variable concurrent programs. It lets each thread specify its expectation (the rely condition) of state transi￾tions made by its environment, and its guarantee to the environment about transitions made by itself. Since the rely condition specifies all possible behaviors that might interfere with the thread, we do not need to consider the exponential size of possible interleavings during the verifications. However, the rely/guarantee conditions are difficult to formulate in practice, because they need to specify the global program state and these global conditions need to be checked during the execution of the whole thread. Specifically, the compo￾sionality and applicability of Rely-Guarantee reasoning are greatly limited by the following problems: • The whole program state is viewed as shared resource and need to be specified in the rely/guarantee conditions, even if a part of the state might be privately owned by a single thread. The thread-private resource has to be exposed in the specifications. • As part of the specifications of program modules, the rely and guarantee conditions need to specify all the shared resources, even if the module accesses only part of them locally. This lim￾its the reuse of verified program modules in different applica￾tions with different shared resources. • Since the shared resources need to be globally known, it is dif- ficult to support the sharing of dynamically allocated resources, which are not known until they are allocated. • Some resources might be shared only by a subset of threads, but there is no way to hide them from the rest of threads in the system. These problems are part of the reasons why Jones (2003) calls for a more compositional approach to concurrency. Recent works on SAGL (Feng et al. 2007) and RGSep (Vafeiadis and Parkinson 2007) have tried to combine the Rely-Guarantee rea￾soning with Separation Logic (Ishtiaq and O’Hearn 2001; Reynolds 2002) for better composionality. They split the whole state into thread-private and shared parts. The partition of resources enforced by Separation Logic ensures that each thread cannot touch the pri￾vate parts of others. The rely and guarantee conditions now only need to specify the part that is indeed shared. These combinations, however, only address the first problem mentioned above. Since they also require the shared resources to be globally known, the last three problems remain unsolved. In this paper, we propose a new program logic, LRG, for Local Rely-Guarantee reasoning. By addressing all these open problems, our logic makes local reasoning and information hiding a reality in concurrency verification. Our work is based on previous works on Rely-Guarantee reasoning and Separation Logic, and SAGL and RGSep in particular, but makes the following new contributions: • As an extension of Separation Logic, we introduce the sepa￾rating conjunction of rely/guarantee conditions. Unlike asser￾tions in Separation Logic, rely/guarantee conditions are binary relations of program states and they specify state transitions. The new separating conjunction allows us to formalize two sub￾transitions conducted over disjoint resources, which is the basis to bring in all the nice ideas developed in Separation Logic for local reasoning and modularity. • Our logic, for the first time, supports a frame rule over rely and guarantee conditions so that the sharing of resources no longer needs to be globally known. Specifications of program modules only need to talk about the resource used locally, therefore the verified modules can be reused in different contexts without redoing the proof. • We propose a new rule for hiding the shared resources from the environment. It allows the local sharing of resources among a subset of threads without exposing them to others in the system. In particular, using the hiding rule we can derive a more general rule for parallel composition such that a thread’s private resource can be shared by its children without being visible by its siblings. The hiding rule also gives us a way to 1

change the rely and guarantee conditions,so that the sharing of atomic operation satisfies the guarantee,and the precondition at dynamically allocated resources can be supported. each step is stable with respect to the rely condition. In addition to these extensions,our work also greatly simplifies The stability means,if the current state satisfies the precondi- SAGL and RGSep.We split program states conceptually into tion p and the current thread is preempted by its environment,p thread-private and shared parts,but do not need explicit distinc- still holds when the current thread resumes its execution in a new tion of them either syntactically in assertions (as in SAGL and state as long as the transition made by the environment satisfies RGSep)or semantically in program states and operational se- its rely condition R.The stability check is essential to ensure the mantics (as in RGSep).This gives us a simpler semantic model non-interference between the thread and its environment,but it re- and makes the logic more flexible to use. quires R to capture all possible behaviors of the environment,which Treating variables as resources (Parkinson et al.2006).our makes R(and G)difficult to define and limits the compositionality work is very general and the same ideas work for traditional of the Rely-Guarantee reasoning. Rely-Guarantee-based logics where only variables are used and heaps are not dealt with. 2.2 Separation Logic and Concurrency Verification Our logic can also be viewed as an extension of the Concurrent Separation Logic (Ishtiag and O'Hearn 2001:Reynolds 2002)is an Separation Logic (O'Hearn 2007)with the more expressive extension of Hoare Logic with effective reasoning about memory Rely-Guarantee-based specifications,but without sacrificing its aliasing.The separating conjunction p*p'in the assertion language compositionality specifies program states that can be split into two disjoint parts In the rest of this paper,we first give an overview of the tech- satisfying p and p'respectively.Because of the separation,update nical background,and use an example to explain the problems and of the part satisfying p does not affect the validity of p'over challenges in Sec.2.Then,before diving into the formal technical the other part.The frame rule,as shown below (with some side development,we explain informally our approaches in Sec.3.We conditions elided),supports local reasoning of program modules: present the programming language in Sec.4,the assertion language in Sec.5 and the LRG logic in Sec.6.As an example,in Sec.7 we PIClal show how the program presented in Sec.2 can be verified in our {p*rC{g*r】 logic.We discuss related work and conclude in Sec.8. The specifications p and g for C need to only talk about states 2 Background and Challenges accessed locally by C.When C is composed with other modules in different contexts,different r can be added in the specification In this section,we give an overview of Rely-Guarantee reason- by applying the frame rule,without redoing the proof. ing,Concurrent Separation Logic,and recent works on combining O'Hearn has proposed Concurrent Separation Logic (CSL), them (Feng et al.2007:Vafeiadis and Parkinson 2007).Then we use an example to show the problems with existing approaches. which applies Separation Logic to reason about concurrent pro- grams (O'Hearn 2007).Unlike Rely-Guarantee reasoning,CSL 2.1 Rely-Guarantee Reasoning ensures non-interference by enforcing the separation of resources accessible by different threads.The parallel composition rule in In Rely-Guarantee reasoning,each thread views the set of all other CSL is as follows: threads in the system as its environment.The interface between the thread and its environment is specified using a pair of rely and guar- APIlC1tg1)ip2]C21g21 antee conditions.The rely condition R specifies the thread's expec- {P1*p2C1‖C2{q1*q2l tations of state transitions made by its environment.The guarantee G specifies the state transitions made by the thread itself.R and G Verification of each sequential thread in CSL is the same as in are predicates over a pair of states,i.e..the initial one before the Separation Logic.The frame rule is also sound in CSL.CSL also transition and the resulting one after the transition.The specifica- allows threads to share resources,but only in conditional critical tion of a thread is a quadruple (p,R,G,g),where p and g are pre- regions that can be entered by only one thread at a time.The well- and post-conditions.A thread satisfies its specification if,given an formedness of shared resources is specified using invariants,which initial state satisfying p and an environment whose behaviors sat- need to be satisfied when threads exit critical regions. isfy R.each atomic transition made by the thread satisfies G and the state at the end satisfies g. 2.3 Combinations of the Two Approaches Parallel Composition.To ensure two parallel threads can collab The rely and guarantee conditions in Rely-Guarantee reasoning orate without interference,we need to check that their interfaces specify state transitions,which are expressive and are suitable to are compatible in the sense that the rely condition of each thread reason about fine-grained concurrent programs.On the other hand, is implied by the guarantee of the other.Below is the rule for the the method views the whole state as a shared resource among parallel composition Cll C2: threads,which makes it less compositional.CSL has very nice CI sat (p,RVG2,G141)C2 sat(p,RVG1,G2.92) compositionality.but the limited expressiveness of invariants for C1l C2 sat (p,R,GI VG2,q1Ag2) shared resources makes it unsuitable for fine-grained concurrency. It shows that,to verify CIl C2,we can verify the children CI SAGL (Feng et al.2007)and RGSep (Vafeiadis and Parkinson and C2 separately.The rely condition of each child captures the 2007)have tried to combine merits of both approaches.They split behavior of both its parent's environment(R)and its sibling(Gi or the whole state into thread-private and shared parts.Specifications G2).It is easy to check that the rely and guarantee conditions for of threads are in the form of ((p,r).R,G,(g,r)).where p and g CI and C2 are compatible,i.e..G(RVG1)and G2(RVG2) are pre-and post-conditions specifying the private resources of the thread,while r and r'for the shared part.Their rules for parallel Stability.Each thread is verified with respect to its specification in a similar way as the verification of sequential programs in Hoare Logic,except that we also need to ensure the behavior of every IRGSep uses p*r instead of (p.r)

change the rely and guarantee conditions, so that the sharing of dynamically allocated resources can be supported. • In addition to these extensions, our work also greatly simplifies SAGL and RGSep. We split program states conceptually into thread-private and shared parts, but do not need explicit distinc￾tion of them either syntactically in assertions (as in SAGL and RGSep) or semantically in program states and operational se￾mantics (as in RGSep). This gives us a simpler semantic model and makes the logic more flexible to use. • Treating variables as resources (Parkinson et al. 2006), our work is very general and the same ideas work for traditional Rely-Guarantee-based logics where only variables are used and heaps are not dealt with. • Our logic can also be viewed as an extension of the Concurrent Separation Logic (O’Hearn 2007) with the more expressive Rely-Guarantee-based specifications, but without sacrificing its compositionality. In the rest of this paper, we first give an overview of the tech￾nical background, and use an example to explain the problems and challenges in Sec. 2. Then, before diving into the formal technical development, we explain informally our approaches in Sec. 3. We present the programming language in Sec. 4, the assertion language in Sec. 5 and the LRG logic in Sec. 6. As an example, in Sec. 7 we show how the program presented in Sec. 2 can be verified in our logic. We discuss related work and conclude in Sec. 8. 2. Background and Challenges In this section, we give an overview of Rely-Guarantee reason￾ing, Concurrent Separation Logic, and recent works on combining them (Feng et al. 2007; Vafeiadis and Parkinson 2007). Then we use an example to show the problems with existing approaches. 2.1 Rely-Guarantee Reasoning In Rely-Guarantee reasoning, each thread views the set of all other threads in the system as its environment. The interface between the thread and its environment is specified using a pair of rely and guar￾antee conditions. The rely condition R specifies the thread’s expec￾tations of state transitions made by its environment. The guarantee G specifies the state transitions made by the thread itself. R and G are predicates over a pair of states, i.e., the initial one before the transition and the resulting one after the transition. The specifica￾tion of a thread is a quadruple (p,R,G,q), where p and q are pre￾and post-conditions. A thread satisfies its specification if, given an initial state satisfying p and an environment whose behaviors sat￾isfy R, each atomic transition made by the thread satisfies G and the state at the end satisfies q. Parallel Composition. To ensure two parallel threads can collab￾orate without interference, we need to check that their interfaces are compatible in the sense that the rely condition of each thread is implied by the guarantee of the other. Below is the rule for the parallel composition C1 C2: C1 sat (p,R∨G2,G1,q1) C2 sat (p,R∨G1,G2,q2) C1 C2 sat (p,R,G1 ∨G2,q1 ∧q2) It shows that, to verify C1 C2, we can verify the children C1 and C2 separately. The rely condition of each child captures the behavior of both its parent’s environment (R) and its sibling (G1 or G2). It is easy to check that the rely and guarantee conditions for C1 and C2 are compatible, i.e., G1 ⇒ (R∨G1) and G2 ⇒ (R∨G2). Stability. Each thread is verified with respect to its specification in a similar way as the verification of sequential programs in Hoare Logic, except that we also need to ensure the behavior of every atomic operation satisfies the guarantee, and the precondition at each step is stable with respect to the rely condition. The stability means, if the current state satisfies the precondi￾tion p and the current thread is preempted by its environment, p still holds when the current thread resumes its execution in a new state as long as the transition made by the environment satisfies its rely condition R. The stability check is essential to ensure the non-interference between the thread and its environment, but it re￾quires R to capture all possible behaviors of the environment, which makes R (and G) difficult to define and limits the compositionality of the Rely-Guarantee reasoning. 2.2 Separation Logic and Concurrency Verification Separation Logic (Ishtiaq and O’Hearn 2001; Reynolds 2002) is an extension of Hoare Logic with effective reasoning about memory aliasing. The separating conjunction p∗ p in the assertion language specifies program states that can be split into two disjoint parts satisfying p and p respectively. Because of the separation, update of the part satisfying p does not affect the validity of p over the other part. The frame rule, as shown below (with some side conditions elided), supports local reasoning of program modules: {p}C{q} {p ∗ r}C{q ∗ r} The specifications p and q for C need to only talk about states accessed locally by C. When C is composed with other modules in different contexts, different r can be added in the specification by applying the frame rule, without redoing the proof. O’Hearn has proposed Concurrent Separation Logic (CSL), which applies Separation Logic to reason about concurrent pro￾grams (O’Hearn 2007). Unlike Rely-Guarantee reasoning, CSL ensures non-interference by enforcing the separation of resources accessible by different threads. The parallel composition rule in CSL is as follows: {p1}C1{q1} {p2}C2{q2} {p1 ∗ p2}C1 C2{q1 ∗ q2} Verification of each sequential thread in CSL is the same as in Separation Logic. The frame rule is also sound in CSL. CSL also allows threads to share resources, but only in conditional critical regions that can be entered by only one thread at a time. The well￾formedness of shared resources is specified using invariants, which need to be satisfied when threads exit critical regions. 2.3 Combinations of the Two Approaches The rely and guarantee conditions in Rely-Guarantee reasoning specify state transitions, which are expressive and are suitable to reason about fine-grained concurrent programs. On the other hand, the method views the whole state as a shared resource among threads, which makes it less compositional. CSL has very nice compositionality, but the limited expressiveness of invariants for shared resources makes it unsuitable for fine-grained concurrency. SAGL (Feng et al. 2007) and RGSep (Vafeiadis and Parkinson 2007) have tried to combine merits of both approaches. They split the whole state into thread-private and shared parts. Specifications of threads are in the form of ((p,r),R,G,(q,r )), where p and q are pre- and post-conditions specifying the private resources of the thread, while r and r for the shared part.1 Their rules for parallel 1 RGSep uses p ∗ r instead of (p,r). 2

nd:=0: Line 14 refers to the program in Fig.2.where two threads collabo- 2 while (nd=0)do rate to compute the GCD of numbers pointed to by x. 1k=0: This is a very simple program,but there is no clean and modular 4 while(1k≠1)do /∥acquire lock way to verify it using existing logics described in the previous (1k =[lhead]:if (lk=1)then [lhead]:=0; sections for the following reasons: 6 7 nd:=[lhead+1]: ∥first node 1.Cged shown in Fig.2 is a fine-grained concurrent program-two threads share the memory without using locks.The correctness if(nd≠O)then 9 tmp:=[nd+2]:[lhead+]:tmp //del.node of the code is based on the fact that each thread preserves the 10 value at the memory location where the other may update;and that all updates decreases the values and preserves the GCD. 11 ([lhead]:=1); ∥release lock It is difficult to verify the code using CSL because the invariant 12 13 tmp:=[nd];tmp':=[nd+1];x:=cons(tmp,tmp); of shared resources cannot express preservation and decrease of 14 Cged values without heavy use of auxiliary variables 2.The functionality of Cecd is self-contained.We want to verify it once and reuse it in different contexts.However,both original Figure 1.GCD of Nodes on List Rely-Guarantee reasoning and recent extensions described in Sec.2.3 require the shared resource be globally known.As a result,when Cecd is verified.the rely and guarantee conditions (t11=[x]): (t21:=[x+1]) (t12:=[x+1])5 (t22:=[x]): have to specify the shared list even if it is not accessed by Cged. 2 3 while(t11≠t12)dol while(t21≠t22)do negating the very advantage of sequential Separation Logic. 4 if(t11 t12)then if(t21 t22)then 3.The memory block pointed to by x is shared locally by the two 5 t11:=t11-t12 t21:=t21-t22 threads in Cged.but not used elsewhere.We should be able to 6 ([x]:=t11): ([x+1]:=t21 hide it and make it invisible outside when we specify the rely and guarantee conditions for the thread in Fig.1.This is not 8 (t12:=[x+1]8 (t22:=[x] supported by existing work on Rely-Guarantee reasoning. 9 4.Even if we give up the third requirement and are willing to expose the local sharing inside Cged in the global rely and Figure 2.Concurrent GCD guarantee conditions,we cannot do so because the memory block pointed to by x is dynamically allocated,whose location is unknown at the beginning composition are as follows: Among these problems,the first one is with CSL,while the rest are CI sat ((pi,r),RVG2,G1,(gi,r1)) with Rely-Guarantee reasoning,including SAGL and RGSep. C2 sat ((p2,r),RVG1,G2.(92,r2)) Polymorphic Interpretations of Rely/Guarantee Conditions?It CIllC2 sat ((p1 +p2.r).R.GI VG2.(91*q2.r1Ar2) is important to note that using a polymorphic interpretation of The partition of resources enforced by the separating conjunction rely and guarantee conditions does not automatically solve these ensures that each thread cannot touch the private parts of others. problems.For instance,we may want to interpret the validity of the The rely and guarantee conditions now only need to specify the rely condition R over state transitions from o to o'in a way such part that is indeed shared. that the following property holds: 2.4 Problems and Challenges If (,')=R.Lo",and o'Lo",then (,')ER. Here we use orLo"to mean o and o"are disjoint,and use To see the problems with all these approaches,we first look at a simple program shown in Figs.I and 2.The program removes to mean the merge of disjoint states.Their formal definitions are a node from a shared linked list and then computes the greatest shown in Sec.5.Although this interpretation takes care of the part common divisor (GCD)of the two numbers stored in the node. of state that is not explicitly specified in R,it does not support local specification and cannot address the second problem mentioned head above.Suppose we have verified Cged with a local specification of nxt R that does not mention the shared list,the interpretation requires that the list be preserved by the environment,which is too strong an assumption and cannot be matched with the actual rely condition The shared data structure is shown above.The global constant for the first 13 lines of code (and the consequence rule cannot be Thead points to two memory cells.The first one contains a binary applied,which only allows strengthening of the rely condition). mutex,which enforces mutual exclusive accesses to the linked list As a second try,let's consider a very weak interpretation that pointed to by the pointer stored in the second memory cell. satishies the following property: We use“(C)”to mean C is executed atomically.“x:=[E] f(c,c)=R,c⊥c",andr'⊥r",then(σyc",c'世c")=R ("[E]:=E")loads values from (stores values into)memory at the location E."cons(E1,...,En)"allocates n memory cells with initial It says the part of the state unspecified in R might be changed arbi- values E1,...,En.The thread shown in Fig.I can be viewed as a trarily.This interpretation,however,is too weak for the guarantee consumer of a producer-consumer style program,where the pro- condition G.So we probably need a different interpretation for G ducer (not shown here)generates random numbers and puts them e.g.,the first one.Using different interpretations for R and G makes onto the list.Code from line I to line 12 acquires the lock,removes the logic complicated.A more serious problem with this approach a node from the list and then releases the lock.Line 13 copies num is that it does not allow the hiding of locally shared resources.In the bers in the node to newly allocated memory cells.The code Cged in parallel composition rule shown in Sec.2.1,if we do not specify in

1 nd := 0; 2 while (nd = 0) do { 3 lk := 0; 4 while (lk 1) do { // acquire lock 5 lk := [lhead]; if (lk = 1) then [lhead] := 0; 6 } 7 nd := [lhead+1]; // first node 8 if (nd 0) then { 9 tmp := [nd+2]; [lhead+1] := tmp //del. node 10 } 11 [lhead] := 1 ; // release lock 12 } 13 tmp := [nd]; tmp := [nd+1]; x := cons(tmp,tmp ); 14 Cgcd Figure 1. GCD of Nodes on List 1 t11 := [x] ; t21 := [x+1] ; 2 t12 := [x+1] ; t22 := [x] ; 3 while (t11 t12) do{ while (t21 t22) do{ 4 if(t11 > t12) then { if(t21 > t22) then { 5 t11 := t11−t12; t21 := t21−t22; 6 [x] := t11 ; [x+1] := t21 ; 7 } } 8 t12 := [x+1] ; t22 := [x] ; 9 } } Figure 2. Concurrent GCD composition are as follows: C1 sat ((p1,r),R∨G2,G1,(q1,r1)) C2 sat ((p2,r),R∨G1,G2,(q2,r2)) C1 C2 sat ((p1 ∗ p2,r),R,G1 ∨G2,(q1 ∗ q2,r1 ∧r2) The partition of resources enforced by the separating conjunction ensures that each thread cannot touch the private parts of others. The rely and guarantee conditions now only need to specify the part that is indeed shared. 2.4 Problems and Challenges To see the problems with all these approaches, we first look at a simple program shown in Figs. 1 and 2. The program removes a node from a shared linked list and then computes the greatest common divisor (GCD) of the two numbers stored in the node. ... lhead 0/1 list nxt nxt The shared data structure is shown above. The global constant lhead points to two memory cells. The first one contains a binary mutex, which enforces mutual exclusive accesses to the linked list pointed to by the pointer stored in the second memory cell. We use “C ” to mean C is executed atomically. “x := [E]” (“[E] := E ”) loads values from (stores values into) memory at the location E. “cons(E1,...,En)” allocates n memory cells with initial values E1,...,En. The thread shown in Fig. 1 can be viewed as a consumer of a producer-consumer style program, where the pro￾ducer (not shown here) generates random numbers and puts them onto the list. Code from line 1 to line 12 acquires the lock, removes a node from the list and then releases the lock. Line 13 copies num￾bers in the node to newly allocated memory cells. The code Cgcd in Line 14 refers to the program in Fig. 2, where two threads collabo￾rate to compute the GCD of numbers pointed to by x. This is a very simple program, but there is no clean and modular way to verify it using existing logics described in the previous sections for the following reasons: 1. Cgcd shown in Fig. 2 is a fine-grained concurrent program – two threads share the memory without using locks. The correctness of the code is based on the fact that each thread preserves the value at the memory location where the other may update; and that all updates decreases the values and preserves the GCD. It is difficult to verify the code using CSL because the invariant of shared resources cannot express preservation and decrease of values without heavy use of auxiliary variables. 2. The functionality of Cgcd is self-contained. We want to verify it once and reuse it in different contexts. However, both original Rely-Guarantee reasoning and recent extensions described in Sec. 2.3 require the shared resource be globally known. As a result, when Cgcd is verified, the rely and guarantee conditions have to specify the shared list even if it is not accessed by Cgcd, negating the very advantage of sequential Separation Logic. 3. The memory block pointed to by x is shared locally by the two threads in Cgcd, but not used elsewhere. We should be able to hide it and make it invisible outside when we specify the rely and guarantee conditions for the thread in Fig. 1. This is not supported by existing work on Rely-Guarantee reasoning. 4. Even if we give up the third requirement and are willing to expose the local sharing inside Cgcd in the global rely and guarantee conditions, we cannot do so because the memory block pointed to by x is dynamically allocated, whose location is unknown at the beginning. Among these problems, the first one is with CSL, while the rest are with Rely-Guarantee reasoning, including SAGL and RGSep. Polymorphic Interpretations of Rely/Guarantee Conditions? It is important to note that using a polymorphic interpretation of rely and guarantee conditions does not automatically solve these problems. For instance, we may want to interpret the validity of the rely condition R over state transitions from σ to σ in a way such that the following property holds: If (σ,σ ) |= R, σ⊥σ, and σ ⊥σ, then (σσ,σ σ) |= R. Here we use σ⊥σ to mean σ and σ are disjoint, and use σσ to mean the merge of disjoint states. Their formal definitions are shown in Sec. 5. Although this interpretation takes care of the part of state that is not explicitly specified in R, it does not support local specification and cannot address the second problem mentioned above. Suppose we have verified Cgcd with a local specification of R that does not mention the shared list, the interpretation requires that the list be preserved by the environment, which is too strong an assumption and cannot be matched with the actual rely condition for the first 13 lines of code (and the consequence rule cannot be applied, which only allows strengthening of the rely condition). As a second try, let’s consider a very weak interpretation that satisfies the following property: If (σ,σ ) |= R, σ⊥σ, and σ ⊥σ, then (σσ,σ σ) |= R. It says the part of the state unspecified in R might be changed arbi￾trarily. This interpretation, however, is too weak for the guarantee condition G. So we probably need a different interpretation for G, e.g., the first one. Using different interpretations for R and G makes the logic complicated. A more serious problem with this approach is that it does not allow the hiding of locally shared resources. In the parallel composition rule shown in Sec. 2.1, if we do not specify in 3

R the resource locally shared by Ci and C2,the new rely condition (Expr)E ::=xX n E+E E-E... RVG2 for Cl is then too weak to be useful.The variation of the rule in Sec.2.3 has the same problem. (Bexp)B ::true l falseE=EE E .. (Stmts)C ::=x:=E:=[E]E]:=E I skip 3.Our Approach x:=cons(E,....E)|dispose(E)C:C As in SAGL and RGSep,we also split program states into thread- I if B then C else C|while B do C I C1 ll C2 private and shared parts.Each thread has exclusive access of its atomic(B)(C) own private resources.Rely/guarantee conditions only specify the shared part.But we try to borrow more ideas from Separation Logic Figure 3.The Language to address the remaining compositionality problems. We first introduce the separating conjunction over actions,i.e., binary relations of states specifying state transitions.Rely and guar- (Store)s∈Par一imlu antee conditions are all actions.Similar to the separating conjunc- tion p*p'in Separation Logic,R+R'(or G*G')means the two (LvMap)i∈LVar一fin Int sub-actions R and R'(or G and G')occur over disjoint parts of (Heap)h∈Nat一iaIt states.A formal definition will be given in Sec.5. (State)o E Storex LvMapx Heap We can now extend the frame rule in Separation Logic to sup- (Trans）R,G∈P(State x State) port local rely and guarantee conditions: R.G((p,r)C(q,r)m stable with respect to R' Figure 4.Program States R*R',G*G'(p,r*m)C[(g.r'sm) Following SAGL and RGSep,here we specify private and shared The hiding rule is particularly interesting when C is a parallel resources separately in pre-and post-conditions (but not in our composition (CIl C2).It allows us to derive a more general rule formal development).We use R,G(p.r))C(g.r)]to represent for parallel composition such that the children threads may share the old judgment C sat ((p,r).R,G,(g.r))described in Sec.2.3 resources that appear to the outside world as private resources The frame rule says we can verify C with the local specification of the parent thread.This also solves the last problem described ((p,r),R,G,(g.r)).When C is executed in different contexts with in Sec.2.4.Sharing of dynamically allocated resources usually the extra shared resource specified by m,we know C satisfies follows the pattern of Co:(CI II C2).like the example in Sec.2.4 the "bigger"specification without redoing the proof.The stability New resources are allocated by Co and then shared by CI and C2. check that causes compositionality problems in Rely-Guarantee Since they are unknown at the beginning of Co,we cannot specify reasoning,as explained in Sec.2.1,is no longer an issue here them in the global R and G.Our new rule allows us to leave them because we can prove r*m is stable with respect to R*R'if r unspecified in the R and G outside of Cil C2. is stable with respect to R and m is stable with respect to R'(we actually need some subtle constraints to prove this,which will be Note that the rules shown in this section are used to illustrate our explained in Sec.5). basic ideas in a semi-formal way.The actual ones in the LRG logic are presented in Sec.6 and are in different forms.In particular,we The simpler frame rule for private resources,as shown below,is do not need the pairs(p,r)as pre-and post-conditions. supported in SAGL and RGSep and is sound in our logic too. R,G{p,r)C(4,)} 4. The Language R,G上{(p*m,r)lC(q*m,r)刃 The syntax of the language is defined in Fig.3.We use x and X Since the rely/guarantee conditions specify only the shared re- to represent program variables (PVar)and logical variables (LVar) sources.they do not need to be changed with the extension of the respectively.The expressions E and B are pure.The statement private predicates. x:=[E]([E]:=E')loads values from (stores the value E'into) To allow the hiding of the local sharing of resources by a subset memory at the location E.x:=cons(E1,...,En)allocates n consec- of threads,we introduce a new hiding rule: utive fresh memory cells and initializes them with E.....En.The starting address is picked nondeterministically and assigned to x. R*R',G*G'((p.r*m))C((g.r'*m')][side-conditions omitted] dispose(E)frees the memory cell at the location E. R.GF(p*m,r)C((g*m',r') The atomic block atomic(B)(C)executes C atomically if B This rule says if the resource specified by m and m'is shared locally holds.Otherwise the current process is blocked until B becomes inside C.and transitions over the resource is specified by R'and G. true.As pointed out by Vafeiadis and Parkinson(2007).it can be we can treat it as private and hide R'and G'in the rely/guarantee used to model synchronizations at different levels,such as a system- conditions so that it is invisible from the outside world.Although wide lock or atomicity guaranteed by transactional memory.The this rule only converts part of the shared resource into private use of atomic(true)(C)can also be viewed as annotations of atomic and does not hide its existence in the pre-and post-conditions,it machine instructions for fine-grained concurrency (Parkinson et al. does hide the resource from other threads because rely/guarantee 2007).The other statements in Fig.3 have standard meanings. conditions are the interface between threads. Figure 4 presents the model of program states.The store s is At first glance,this rule seems to allow a thread to arbitrarily a finite partial mapping from program variables to integers;the hide any shared resources so that it can cheat its environment.The logical variable mapping i maps logical variables to integers;and thread,however,cannot abuse this freedom because the inappropri- the heap h maps memory locations (natural numbers)to integers ate hiding will be detected at the point of parallel composition.We The program state or is a triple of (s,i,h).State transitions R and G will explain this in detail in Sec.6. are binary relations of states

R the resource locally shared by C1 and C2, the new rely condition R ∨ G2 for C1 is then too weak to be useful. The variation of the rule in Sec. 2.3 has the same problem. 3. Our Approach As in SAGL and RGSep, we also split program states into thread￾private and shared parts. Each thread has exclusive access of its own private resources. Rely/guarantee conditions only specify the shared part. But we try to borrow more ideas from Separation Logic to address the remaining compositionality problems. We first introduce the separating conjunction over actions, i.e., binary relations of states specifying state transitions. Rely and guar￾antee conditions are all actions. Similar to the separating conjunc￾tion p ∗ p in Separation Logic, R ∗ R (or G ∗ G ) means the two sub-actions R and R (or G and G ) occur over disjoint parts of states. A formal definition will be given in Sec. 5. We can now extend the frame rule in Separation Logic to sup￾port local rely and guarantee conditions: R,G  {(p,r)}C{(q,r )} m stable with respect to R ... R∗R ,G ∗G  {(p,r ∗m)}C{(q,r ∗m)} Following SAGL and RGSep, here we specify private and shared resources separately in pre- and post-conditions (but not in our formal development). We use R,G  {(p,r)}C{(q,r )} to represent the old judgment C sat ((p,r),R,G,(q,r )) described in Sec. 2.3. The frame rule says we can verify C with the local specification ((p,r),R,G,(q,r )). When C is executed in different contexts with the extra shared resource specified by m, we know C satisfies the “bigger” specification without redoing the proof. The stability check that causes compositionality problems in Rely-Guarantee reasoning, as explained in Sec. 2.1, is no longer an issue here because we can prove r ∗ m is stable with respect to R ∗ R if r is stable with respect to R and m is stable with respect to R (we actually need some subtle constraints to prove this, which will be explained in Sec. 5). The simpler frame rule for private resources, as shown below, is supported in SAGL and RGSep and is sound in our logic too. R,G  {(p,r)}C{(q,r )} R,G  {(p ∗m,r)}C{(q ∗m,r )} Since the rely/guarantee conditions specify only the shared re￾sources, they do not need to be changed with the extension of the private predicates. To allow the hiding of the local sharing of resources by a subset of threads, we introduce a new hiding rule: R∗R ,G ∗G  {(p,r ∗m)}C{(q,r ∗m )} [side-conditions omitted] R,G  {(p ∗m,r)}C{(q ∗m ,r )} This rule says if the resource specified by m and m is shared locally inside C, and transitions over the resource is specified by R and G , we can treat it as private and hide R and G in the rely/guarantee conditions so that it is invisible from the outside world. Although this rule only converts part of the shared resource into private and does not hide its existence in the pre- and post-conditions, it does hide the resource from other threads because rely/guarantee conditions are the interface between threads. At first glance, this rule seems to allow a thread to arbitrarily hide any shared resources so that it can cheat its environment. The thread, however, cannot abuse this freedom because the inappropri￾ate hiding will be detected at the point of parallel composition. We will explain this in detail in Sec. 6. (Expr) E ::= x | X | n | E + E | E - E | ... (Bexp) B ::= true | false | E = E | E E | ... (Stmts) C ::= x := E | x := [E] | [E] := E | skip | x := cons(E,...,E) | dispose(E) | C;C | if B then C else C | while B do C | C1 C2 | atomic(B){C} Figure 3. The Language (Store) s ∈ PVar fin Int (LvMap) i ∈ LVar fin Int (Heap) h ∈ Nat fin Int (State) σ ∈ Store×LvMap×Heap (Trans) R,G∈P(State×State) Figure 4. Program States The hiding rule is particularly interesting when C is a parallel composition (C1 C2). It allows us to derive a more general rule for parallel composition such that the children threads may share resources that appear to the outside world as private resources of the parent thread. This also solves the last problem described in Sec. 2.4. Sharing of dynamically allocated resources usually follows the pattern of C0; (C1 C2), like the example in Sec. 2.4. New resources are allocated by C0 and then shared by C1 and C2. Since they are unknown at the beginning of C0, we cannot specify them in the global R and G. Our new rule allows us to leave them unspecified in the R and G outside of C1 C2. Note that the rules shown in this section are used to illustrate our basic ideas in a semi-formal way. The actual ones in the LRG logic are presented in Sec. 6 and are in different forms. In particular, we do not need the pairs (p,r) as pre- and post-conditions. 4. The Language The syntax of the language is defined in Fig. 3. We use x and X to represent program variables (PVar) and logical variables (LVar) respectively. The expressions E and B are pure. The statement x := [E] ([E] := E ) loads values from (stores the value E into) memory at the location E. x := cons(E1,...,En) allocates n consec￾utive fresh memory cells and initializes them with E1,..., En. The starting address is picked nondeterministically and assigned to x. dispose(E) frees the memory cell at the location E. The atomic block atomic(B){C} executes C atomically if B holds. Otherwise the current process is blocked until B becomes true. As pointed out by Vafeiadis and Parkinson (2007), it can be used to model synchronizations at different levels, such as a system￾wide lock or atomicity guaranteed by transactional memory. The use of atomic(true){C} can also be viewed as annotations of atomic machine instructions for fine-grained concurrency (Parkinson et al. 2007). The other statements in Fig. 3 have standard meanings. Figure 4 presents the model of program states. The store s is a finite partial mapping from program variables to integers; the logical variable mapping i maps logical variables to integers; and the heap h maps memory locations (natural numbers) to integers. The program state σ is a triple of (s,i,h). State transitions R and G are binary relations of states. 4

[E](s,n=nx∈dom(s) [El(s.i)undefined or xg dom(s) (x:=E.(s.i,h))(skip,(six nl.i,h)) (x:=E,(s,i,h))abort 【Elsn=Ch(O=n xe dom() [El(s.i)undefined or [Els.n￥dom(h)orx生dom(s) (x:=[E],(s.ih))(skip,(slxn.i.h)) (x:=[E],(s,i,h))abort [Eil(s.i)=t [E2l(s.i)=n eedom(h) [El(s.i)undefined or [E2l(si)undefined or [El(si)dom(h) ([E]:=E2.(s.i,h))(skip.(s.i.he) ([E]:=E2,(s,i,h))abort [Els.0=tt∈dom(h) [Els,n undefined or【Els.)￥dom(h) (dispose(E),(s,i.h))(skip.(s,i,h)) (dispose(E),(s,i,h))abort {化，，f+k-1}ndom(h)=0[E1ls)=m [Ekl(s,n=kx∈dom(s) (x=cons(E1,,Ek,(s,i,h)(skip,(sx,i,h世{化+n1,.,C+k-14万 [Ejls.)undefined(l≤j≤k).or x dom(s) (x :cons(E1.....E),(s,i,h))abort Figure 5.Operational Semantics-Primitive Statements [Bl(o.s.o.i)=tt [Bl(G.s.c.i)=ff [Blo.s.i)undefined (if B then Ci else C2,)(C1.) (if B then CI else C2.)(C2,) (if B then CI else C2.)abort [Bl(o.s.o.i)=tt [Bl(o.s.o.i)=ff [Blo.s..i)undefined (while B do C,)(C;while B do C.o) (while B do C.)(skip,) (while B do C.)abort (C1,)(Ci, (C1,)abort (C1:C2,0)(C1:C2,0万 (C1:C2,0)abort (skip;C,)(C.) (C1,)(C1,) (C2,)(C2,） (C1.)abort or (C2.)~abort (C1IC2,r)(CC2,) (CIlI C2.)(CIllC3.) (CIl C2,)abort [Bl =tt (C.)(skip,') [Blo=tt (C.o)abort (skip ll skip,)(skip,) (atomic(B)(Cl,)(skip.o') (atomic(B)Clo)abort (c,）∈R (C,)(C',) (C.o)abort (C.o)R(C.o) (C,8(C, (C.)abort Figure 6.Operational Semantics-Other Statements The semantics of E and B are defined by [E]and [B]respec- state o,we have (C.)abort.In the third case,the program gets tively.[E]is a partial function of type stuck,although o satisfies the safety requirements.Then (C,) is undefined.The third case occurs when C is skip,or it begins with Store×LvMap一lnt. an atomic statement atomic(B)C')such that B does not hold over [B]is a partial function of type or C does not terminate.The skip statement plays two roles here:a statement that has no computation effects or a flag to show Store×LvMap一{tt,ffl. the end of execution._is the transitive-reflexive closure of the Their definitions are straightforward and are omitted here.We treat single step transition relation. program variables as resources,following Parkinson et al.(2006). The semantic functions are undefined if variables in E and B are not assigned values in s and i. The single step execution of a process is modeled as a binary relation: We use R to represent the possible transitions made by the -÷-∈P(Stmts×State)X(Stmtsx S1ate)U{abort) environment.Then the binary relationas defined in Fig.6 represents one step of state transitions made either by the current It is formally defined in Figs.5 and 6.Given a statement C and a process or by its environment characterized by R.Our treatment state o,we have three cases.First,C can execute one step.We have of the atomic block atomic(B)C)follows Vafeiadis and Parkinson a new state o'and a remaining statement C'.In this case,we have (2007):execution of the statement C appears to finish in one step (C,)(C,).If it is not safe to execute the next statement in the and cannot be interrupted by the environment

[[E]](s,i) = n x ∈ dom(s) (x := E,(s,i,h)) (skip,(s{x n},i,h)) [[E]](s,i) undefined or x  dom(s) (x := E,(s,i,h)) abort [[E]](s,i) =  h() = n x ∈ dom(s) (x := [E],(s,i,h)) (skip,(s{x n},i,h)) [[E]](s,i) undefined or [[E]](s,i)  dom(h) or x  dom(s) (x := [E],(s,i,h)) abort [[E1]](s,i) =  [[E2]](s,i) = n  ∈ dom(h) ([E1] := E2,(s,i,h)) (skip,(s,i,h{ n})) [[E1]](s,i) undefined or [[E2]](s,i) undefined or [[E1]](s,i)  dom(h) ([E1] := E2,(s,i,h)) abort [[E]](s,i) =   ∈ dom(h) (dispose(E),(s,i,h)) (skip,(s,i,h \ {})) [[E]](s,i) undefined or [[E]](s,i)  dom(h) (dispose(E),(s,i,h)) abort {,...,+k−1} ∩dom(h) = ∅ [[E1]](s,i) = n1 [[Ek]](s,i) = nk x ∈ dom(s) (x := cons(E1,...,Ek ),(s,i,h)) (skip,(s{x },i,h { n1,...,+k−1 nk})) [[Ej]](s,i) undefined (1 ≤ j ≤ k) or x  dom(s) (x := cons(E1,...,Ek),(s,i,h)) abort Figure 5. Operational Semantics — Primitive Statements [[B]](σ.s,σ.i) = tt (if B then C1 else C2,σ) (C1,σ) [[B]](σ.s,σ.i) = ff (if B then C1 else C2,σ) (C2,σ) [[B]](σ.s,σ.i) undefined (if B then C1 else C2,σ) abort [[B]](σ.s,σ.i) = tt (while B do C,σ) (C;while B do C,σ) [[B]](σ.s,σ.i) = ff (while B do C,σ) (skip,σ) [[B]](σ.s,σ.i) undefined (while B do C,σ) abort (C1,σ) (C 1,σ ) (C1;C2,σ) (C 1;C2,σ ) (C1,σ) abort (C1;C2,σ) abort (skip;C,σ) (C,σ) (C1,σ) (C 1,σ ) (C1 C2,σ) (C 1 C2,σ ) (C2,σ) (C 2,σ ) (C1 C2,σ) (C1 C 2,σ ) (C1,σ) abort or (C2,σ) abort (C1 C2,σ) abort (skip skip,σ) (skip,σ) [[B]]σ = tt (C,σ) ∗ (skip,σ ) (atomic(B){C},σ) (skip,σ ) [[B]]σ = tt (C,σ) ∗ abort (atomic(B){C},σ) abort (σ,σ ) ∈ R (C,σ) R −→ (C,σ ) (C,σ) (C ,σ ) (C,σ) R −→ (C ,σ ) (C,σ) abort (C,σ) R −→ abort Figure 6. Operational Semantics — Other Statements The semantics of E and B are defined by [[E]] and [[B]] respec￾tively. [[E]] is a partial function of type Store×LvMap Int. [[B]] is a partial function of type Store×LvMap {tt,ff}. Their definitions are straightforward and are omitted here. We treat program variables as resources, following Parkinson et al. (2006). The semantic functions are undefined if variables in E and B are not assigned values in s and i. The single step execution of a process is modeled as a binary relation: ∈ P((Stmts×State)×((Stmts×State)∪ {abort})) It is formally defined in Figs. 5 and 6. Given a statement C and a state σ, we have three cases. First, C can execute one step. We have a new state σ and a remaining statement C . In this case, we have (C,σ) (C ,σ ). If it is not safe to execute the next statement in the state σ, we have (C,σ) abort. In the third case, the program gets stuck, although σ satisfies the safety requirements. Then (C,σ) is undefined. The third case occurs when C is skip, or it begins with an atomic statement atomic(B){C } such that B does not hold over σ or C does not terminate. The skip statement plays two roles here: a statement that has no computation effects or a flag to show the end of execution. ∗ is the transitive-reflexive closure of the single step transition relation. We use R to represent the possible transitions made by the environment. Then the binary relation R −→ , as defined in Fig. 6, represents one step of state transitions made either by the current process or by its environment characterized by R. Our treatment of the atomic block atomic(B){C} follows Vafeiadis and Parkinson (2007): execution of the statement C appears to finish in one step and cannot be interrupted by the environment. 5

(PVarList)O=●|x,O (Assertion)p.q,r,I::=B I empn I emps I Own(x) (s,i,h)卡aB i证[Bl(s)=t IEHE|p*qlp-®gI (s,i,h)=st emps iff s=0 (Action)a,R,G:=p×g|[pla*a|3X.a|a→d (s,i,h)卡emph iff h=0 I aval... (s,i,h)上Own(x) iff dom(s={x对 (s,i,h)FsaE1→Eif Figure 7.The Assertion Language there exist e and n such that [El(s.i)=t.[E2l(s.)=n, dom(h)=t)and h(t)=n 5.The Assertion Language The assertion language is shown in Fig.7.We use the Separation f1g 些dom(f)dom(g)=0 Logic assertions to specify program states.Following Parkinson (s,i,h)(s',i',h') et al.(2006).we treat program variables as resources,but do not (sus',i,huh')if sLs',hlh',i=i' use fractional permissions,which are orthogonal to our technical undefined otherwise development. iff there exist o and or2 such that Semantics of some assertions are shown in Fig.8.The boolean FsL pl*p2 1世o2=T,o1卡sLp1 and o2卡sp2 expression B holds over a state only if it evaluates to true.It is important to note that,with program variables as resources, r卡sp®q iff there exist o'and o"such that the boolean expression E=E does not always hold.It holds if r"=c世cr','Fs p and o"卡q and only if the store contains the variables needed to evaluate E. The assertions empn and emps specify empty heaps and stores x1,...,,p 5 (Own(x1)*Own(n))A p respectively.Own(x)means the ownership of the variable x.E emp emp A emp E2 specifies a singleton heap with E2 stored at the location E1 It also requires that the store contain variables used to evaluate Ei and E2.The separating conjunction p*q means p and g hold Figure 8.Semantics of Selected Separation Logic Assertions over disjoint part of state.Here we use fLg to mean the two finite partial mappings f and g have disjoint domains.The union of two disjoint states o and o2 is defined as oo2.The septraction p-q,introduced by Vafeiadis and Parkinson (2007).means the (c,)Fp×q iff o.i=o'.i,oFst p and o'Fs q state can be extended with a state satisfying p and the extended (c,)=[p] iff o=o'and o Fstp state satisfies g.The assertions Op and emp are syntactic sugars (o,o')=a*a f whose definitions are also shown in Fig.8.O contains a set of program variables,as defined in Fig.7.We omit other assertions there exist 1,2.and o2 such that i=o. here,which are standard separation logic assertions. o102=o.(01.01)F a.and (o2.02)Fa' ((s,i,h),(s',i,h')3X.a iff As in Separation Logic,the precision of assertions is defined there exist n and i'such that i'=in below.Informally,a predicate p is precise if and only if for any and ((s,i',h),(s',i,h'))a state there is at most one sub-state satisfying p. (or,σ)=a→d iff if (o,')F a,then (o,)=a Definition 5.1 (Precise Assertions)An assertion p is precise,i.e., (o,o')=ava' iff (,o')=aor(,')=a precise(p)holds,if and only if for all s,i,h,s1.s2.h.h2.if ss. s2∈s,h1∈h,h2∈h,(s1,i,h1)FsL p and(s2,i,h2)Fsup,then s1=52 and h=h2. Emp些 empemp Trued true xtrue ld [true] al def (()1(')Hal 5.1 Actions We use actions a to specify state transitions.As shown in Fig.7. Figure 9.Semantics of Actions rely/guarantee conditions of threads are actions.Semantics of ac- tions are defined in Fig.9.The action p means the initial state of the transition satisfies p and the resulting state satisfies g.[p] specifies an identity transition with the states satisfying p.a*a' p→pq→4 means the actions a and a'start from disjoint states and the result- (p*p)×(q*q)台(p×q)*(p'<) p×g→p'× ing states are also disjoint.Emp.True and ld are defined using these primitive actions,which represent empty transitions,arbitrary tran- sitions and arbitrary identity transitions respectively.We use Tal to (pVp)×q台(p×qI)V(p'×q) [p→p×p p]→ld represent the set of transitions satisfying a,and use (o,)a and (o.)la]interchangeably in this paper. p(qvq)(pxq)v(pxq) [empl台Emp a→True In Fig.10,we show some selected proof rules for actions,which are sound with respect to the semantics of actions.Many proof a1→4a2→d a*Emp台a a*d台d*d rules for Separation Logic assertions can also be ported for actions a1*2→41*a5 and are omitted here.Examples of actions are shown below.The following lemma shows the monotonicity of the action a*ld: Figure 10.Selected Proof Rules for Actions

(PVarList) O ::= • | x,O (Assertion) p,q,r,I ::= B | emph | emps | Own(x) | E → E | p ∗ q | p−q | ... (Action) a,R,G ::= p  q | [p] | a ∗ a | ∃X.a | a ⇒ a | a∨a | ... Figure 7. The Assertion Language 5. The Assertion Language The assertion language is shown in Fig. 7. We use the Separation Logic assertions to specify program states. Following Parkinson et al. (2006), we treat program variables as resources, but do not use fractional permissions, which are orthogonal to our technical development. Semantics of some assertions are shown in Fig. 8. The boolean expression B holds over a state only if it evaluates to true. It is important to note that, with program variables as resources, the boolean expression E = E does not always hold. It holds if and only if the store contains the variables needed to evaluate E. The assertions emph and emps specify empty heaps and stores respectively. Own(x) means the ownership of the variable x. E1 → E2 specifies a singleton heap with E2 stored at the location E1. It also requires that the store contain variables used to evaluate E1 and E2. The separating conjunction p ∗ q means p and q hold over disjoint part of state. Here we use f ⊥g to mean the two finite partial mappings f and g have disjoint domains. The union of two disjoint states σ1 and σ2 is defined as σ1  σ2. The septraction p −q, introduced by Vafeiadis and Parkinson (2007), means the state can be extended with a state satisfying p and the extended state satisfies q. The assertions O p and emp are syntactic sugars, whose definitions are also shown in Fig. 8. O contains a set of program variables, as defined in Fig. 7. We omit other assertions here, which are standard separation logic assertions. As in Separation Logic, the precision of assertions is defined below. Informally, a predicate p is precise if and only if for any state there is at most one sub-state satisfying p. Definition 5.1 (Precise Assertions) An assertion p is precise, i.e., precise(p) holds, if and only if for all s, i, h, s1, s2, h1, h2, if s1 ⊆ s, s2 ⊆ s, h1 ⊆ h, h2 ⊆ h, (s1,i,h1) |=sl p and (s2,i,h2) |=sl p, then s1 = s2 and h1 = h2. 5.1 Actions We use actions a to specify state transitions. As shown in Fig. 7, rely/guarantee conditions of threads are actions. Semantics of ac￾tions are defined in Fig. 9. The action p  q means the initial state of the transition satisfies p and the resulting state satisfies q. [p] specifies an identity transition with the states satisfying p. a ∗ a means the actions a and a start from disjoint states and the result￾ing states are also disjoint. Emp, True and Id are defined using these primitive actions, which represent empty transitions, arbitrary tran￾sitions and arbitrary identity transitions respectively. We use [[a]] to represent the set of transitions satisfying a, and use (σ,σ ) |= a and (σ,σ ) ∈ [[a]] interchangeably in this paper. In Fig. 10, we show some selected proof rules for actions, which are sound with respect to the semantics of actions. Many proof rules for Separation Logic assertions can also be ported for actions and are omitted here. Examples of actions are shown below. The following lemma shows the monotonicity of the action a ∗ Id: (s,i,h) |=sl B iff [[B]](s,i) = tt (s,i,h) |=sl emps iff s = ∅ (s,i,h) |=sl emph iff h = ∅ (s,i,h) |=sl Own(x) iff dom(s) = {x} (s,i,h) |=sl E1 → E2 iff there exist  and n such that [[E1]](s,i) = ,[[E2]](s,i) = n, dom(h) = {} and h() = n f ⊥g def = dom(f)∩dom(g) = ∅ (s,i,h)(s ,i  ,h ) def = (s∪ s ,i,h∪h ) if s⊥s , h⊥h , i = i  undefined otherwise σ |=sl p1 ∗ p2 iff there exist σ1 and σ2 such that σ1 σ2 = σ,σ1 |=sl p1 and σ2 |=sl p2 σ |=sl p−q iff there exist σ and σ such that σ = σσ ,σ |=sl p and σ |=sl q x1,..., xn,• p def = (Own(x1) ∗···∗Own(xn))∧ p emp def = emps ∧emph Figure 8. Semantics of Selected Separation Logic Assertions (σ,σ ) |= p  q iff σ.i = σ .i, σ |=sl p and σ |=sl q (σ,σ ) |= [p] iff σ = σ and σ |=sl p (σ,σ ) |= a ∗ a iff there exist σ1, σ2, σ 1 and σ 2 such that σ1 σ2 = σ, σ 1 σ 2 = σ ,(σ1,σ 1) |= a, and (σ2,σ 2) |= a ((s,i,h),(s ,i,h )) |= ∃X.a iff there exist n and i  such that i  = i{X n}, and ((s,i  ,h),(s ,i  ,h )) |= a (σ,σ ) |= a ⇒ a iff if (σ,σ ) |= a, then (σ,σ ) |= a (σ,σ ) |= a∨a iff (σ,σ ) |= a or (σ,σ ) |= a ... Emp def = emp  emp True def = true  true Id def = [true] [[a]] def = {(σ,σ ) | (σ,σ ) |= a} Figure 9. Semantics of Actions (p ∗ p )  (q ∗ q ) ⇔ (p  q) ∗ (p  q ) p ⇒ p q ⇒ q p  q ⇒ p  q (p∨ p )  q ⇔ (p  q)∨(p  q) [p] ⇒ p  p [p] ⇒ Id p  (q∨q ) ⇔ (p  q)∨(p  q ) [emp] ⇔ Emp a ⇒ True a1 ⇒ a 1 a2 ⇒ a 2 a1 ∗ a2 ⇒ a 1 ∗ a 2 a ∗Emp ⇔ a a ∗ a ⇔ a ∗ a Figure 10. Selected Proof Rules for Actions 6

Lemma 5.2 If (1,02)=a*ld.o=1o',and o2=o2', then (12)=a*ld. Ioa Ipa' Ipa Ipa IP西 IP(I×ID Ipava I*I'pa*a 5.2 Stability Figure 11.Selected Rules for Fence (Assuming precise()) Next we introduce the concept of stability of an assertion p with respect to an action a. 5.3 Invariant-Fenced Actions Definition 5.3(Stability)We say p is stable with respect to the The following definition says an action a is fenced by a precise invariant /(represented as IDa)if and only if a holds over identity action a,i.e.,Sta(p,a)holds.if and only if for all o and o',if transitions satisfying [n,and holds over the beginning and end Fst p and (.')=a,then 'Fst p. states of transitions satisfying a. Informally,Sta(p,a)means the validity of p is preserved by transitions in Tal.Examples of Sta(p,a)are shown below.Follow- Definition 5.7 (Fence)I a holds iff [n=a.a=(I1)and ing RGSep (Vafeiadis and Parkinson 2007).the following lemma precise(/). shows the encoding of stability using the septraction p. It is natural to ask a to hold over identity transitions so that stutter- Lemma 5.4 The following are true: ing steps of processes would also satisfy it.The second requirement is important to determine the boundary of transitions a and a'in ·Sta(r,pxq)if and only if(p-®r)Aemp)*q→r a*a':the boundary can be uniquely determined if a or a'is fenced ·f(p-®r)*q→r,then Sta(r,pxq: by a precise invariant / ·Sta(r,(p×q)*ld)if and only if(p-&r)*q→r Lemma 5.8 If (i2.')=a*a',i Fst I and I a,then there exist unique of and o2 such that '=2.(1.)F a and The separating conjunction a*a'over actions allows us to com- (c2,2)Fd. pose disjoint transitions into one.Naturally,we want the following property about stability to hold: From Lemma 5.8 we can derive the following frame property of If Sta(p,a)and Sta(p',a'),then Sta(p*p',a*a'). the action a*ld. As explained in Sec.3.this property is important to support local reasoning.Unfortunately,it is not true in general,as shown in the Corollary 5.9 If (.)=a*ld.1 FsL I and Ia,then there following example.The example also shows that we cannot get this exists such that'=2 and (1.)E [al. property even with precise p and p'. Figure 11 shows some selected proof rules for the fencing rela- Example5.5 Let a d(G→mlv(G→m)x(G→m+1). tion.The following lemma shows that the property about stability p些G→m,dg(G→2lv(G→m)x(G1→n1+1》.and discussed in the previous section holds given an action fenced by a psh→2，and suppose(1≠2，we can prove Sta(p.dand precise invariant. Sta(p',a').but Sta(p*p',a+a')does not hold. Here is a counterexample.Let the heap h be m.2n). Lemma 5.10 If Sta(p,a),Sta(p',d'),p=I and Ia,we have and h'be n+1,2 n2+1).Then,for any s,s'and i, Sta(p*p'a*a'). we have (s.i,h)Fst p*p'and ((s,i,h),(s',i,h'))F a*a',but (s',i,h)=s p*p'does not hold. Below we give two examples to show invariant fenced actions. In particular,Example 5.12 shows that asking in /a to be precise To establish the property,we seem to need some concept of does not prevent the action a from changing the size of the resource. "precise actions",similar to the requirement of precise assertions in Separation Logic.However,precision alone cannot address our problem.The following example shows that even if we have Example5.11LetI=(1→-*62→-，a1=[61→X*2→Y门， 2=(E1→X*2HYAX>Y)×(E1→X-Y*2→Y),and Sta(p1.(r))and Sta(p2.(r2))for precise pi.r..p2.r2 a3=(C1→X*2→Y)AX<Y)∝(e1→X*2→Y-X).We andr.we do not necessarily have Sta(pi*p2.(r()). have I a,I (ai va).I (a1 v a3).and I (a va va3),but not Io a2 or Io a3. Example5.6 Letp些G→1，n些2一m,g2→m+l p2些1，n些p1,些（→m+l,and suppose(≠h.w Example 5.12 We define List(C.n)as a linked list pointed to by know Sta(pi.(r))and Sta(p2.(r2))are vacuously true. with length n: but Sta(p1*p2,(r1×r)*(r2×r)is false. List(,t0)些t=0Aemp List(C.n+l)些(emp.At≠0A(化-.*(+1Hf)》*List('C,m) The problem is,p and a may specify different resources even if Sta(p,a)holds.To address this issue,we introduce invariant-fenced Let I 3n.List(t,n),and a =(List(t,m)Ams n)(List(t,n)).We actions and use an invariant to identify the specified resource. can prove that /p a holds

Lemma 5.2 If (σ1,σ2) |= a ∗ Id, σ 1 = σ1 σ , and σ 2 = σ2 σ , then (σ 1,σ 2) |= a ∗ Id. 5.2 Stability Next we introduce the concept of stability of an assertion p with respect to an action a. Definition 5.3 (Stability) We say p is stable with respect to the action a, i.e., Sta(p,a) holds, if and only if for all σ and σ , if σ |=sl p and (σ,σ ) |= a, then σ |=sl p. Informally, Sta(p,a) means the validity of p is preserved by transitions in [[a]]. Examples of Sta(p,a) are shown below. Follow￾ing RGSep (Vafeiadis and Parkinson 2007), the following lemma shows the encoding of stability using the septraction p−q. Lemma 5.4 The following are true: • Sta(r, p  q) if and only if ((p−r)∧emp) ∗ q ⇒ r; • If (p−r) ∗ q ⇒ r, then Sta(r, p  q); • Sta(r,(p  q) ∗ Id) if and only if (p−r) ∗ q ⇒ r. The separating conjunction a∗a over actions allows us to com￾pose disjoint transitions into one. Naturally, we want the following property about stability to hold: If Sta(p,a) and Sta(p ,a ), then Sta(p ∗ p ,a ∗ a ). As explained in Sec. 3, this property is important to support local reasoning. Unfortunately, it is not true in general, as shown in the following example. The example also shows that we cannot get this property even with precise p and p . Example 5.5 Let a def = ([1 → n1])∨((2 → n2)  (2 → n2+1)), p def = 1 → n1, a def = ([2 → n2])∨((1 → n1)  (1 → n1+1)), and p def = 2 → n2, and suppose 1 2, we can prove Sta(p,a) and Sta(p ,a ), but Sta(p ∗ p ,a ∗ a ) does not hold. Here is a counterexample. Let the heap h be {1 n1, 2 n2}, and h be {1 n1+1, 2 n2 +1}. Then, for any s, s and i, we have (s,i,h) |=sl p ∗ p and ((s,i,h),(s ,i,h )) |= a ∗ a , but (s ,i,h ) |=sl p ∗ p does not hold.  To establish the property, we seem to need some concept of “precise actions”, similar to the requirement of precise assertions in Separation Logic. However, precision alone cannot address our problem. The following example shows that even if we have Sta(p1,(r1  r 1)) and Sta(p2,(r2  r 2)) for precise p1,r1,r 1, p2,r2 and r 2, we do not necessarily have Sta(p1 ∗ p2,(r1  r 1)∗(r2  r 2)). Example 5.6 Let p1 def = 1 → n1,r1 def = 2 → n2,r 1 def = 2 →n2+1, p2 def = r1, r2 def = p1, r 2 def = 1 → n1+1, and suppose 1 2. We know Sta(p1,(r1  r 1)) and Sta(p2,(r2  r 2)) are vacuously true, but Sta(p1 ∗ p2,(r1  r 1) ∗ (r2  r 2)) is false.  The problem is, p and a may specify different resources even if Sta(p,a) holds. To address this issue, we introduce invariant-fenced actions and use an invariant to identify the specified resource. I [I] I (I  I) I a I a I a∨a I a I a I ∗ I a ∗ a Figure 11. Selected Rules for Fence (Assuming precise(I)) 5.3 Invariant-Fenced Actions The following definition says an action a is fenced by a precise invariant I (represented as I a) if and only if a holds over identity transitions satisfying [I], and I holds over the beginning and end states of transitions satisfying a. Definition 5.7 (Fence) I  a holds iff [I] ⇒ a, a ⇒ (I  I) and precise(I). It is natural to ask a to hold over identity transitions so that stutter￾ing steps of processes would also satisfy it. The second requirement is important to determine the boundary of transitions a and a in a ∗ a : the boundary can be uniquely determined if a or a is fenced by a precise invariant I. Lemma 5.8 If (σ1 σ2,σ ) |= a ∗ a , σ1 |=sl I and I a, then there exist unique σ 1 and σ 2 such that σ = σ 1 σ 2, (σ1,σ 1) |= a and (σ2,σ 2) |= a . From Lemma 5.8 we can derive the following frame property of the action a ∗ Id. Corollary 5.9 If (σ1σ2,σ )|= a ∗ Id, σ1 |=sl I and Ia, then there exists σ 1 such that σ = σ 1 σ2 and (σ1,σ 1) ∈ [[a]]. Figure 11 shows some selected proof rules for the fencing rela￾tion. The following lemma shows that the property about stability discussed in the previous section holds given an action fenced by a precise invariant. Lemma 5.10 If Sta(p,a), Sta(p ,a ), p ⇒ I and I  a, we have Sta(p ∗ p ,a ∗ a ). Below we give two examples to show invariant fenced actions. In particular, Example 5.12 shows that asking I in Ia to be precise does not prevent the action a from changing the size of the resource. Example 5.11 Let I = 1 → ∗ 2 → , a1 = [1 → X ∗ 2 → Y], a2 = ((1 → X ∗ 2 → Y)∧X > Y)  (1 → X −Y ∗ 2 → Y), and a3 = ((1 → X ∗ 2 → Y)∧X < Y)  (1 → X ∗ 2 → Y − X). We have I  a1, I  (a1 ∨a2), I  (a1 ∨a3), and I  (a1 ∨a2 ∨a3), but not I a2 or I a3.  Example 5.12 We define List(,n) as a linked list pointed to by  with length n: List(,0) def =  = 0∧emp List(,n+1) def = (emps ∧ 0∧( → ∗ +1 →  )) ∗List( ,n) Let I = ∃n. List(,n), and a = (List(,m)∧m ≤ n)  (List(,n)). We can prove that I a holds.  7

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 fenced

6. 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