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 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. 1. Introduction With the development and wide use of multi-core processors, concurrency has become a crucial element in software systems. However, 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 transitions 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 composionality 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 limits the reuse of verified program modules in different applications 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 reasoning 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 private 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 separating conjunction of rely/guarantee conditions. Unlike assertions 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 subtransitions 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 distinction of them either syntactically in assertions (as in SAGL and RGSep) or semantically in program states and operational semantics (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 technical 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 reasoning, 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 guarantee conditions. The rely condition R specifies the thread’s expectations 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 specification of a thread is a quadruple (p,R,G,q), where p and q are preand post-conditions. A thread satisfies its specification if, given an initial state satisfying p and an environment whose behaviors satisfy 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 collaborate 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 precondition 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 requires 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 programs (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 wellformedness 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 producer (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 numbers in the node to newly allocated memory cells. The code Cgcd in Line 14 refers to the program in Fig. 2, where two threads collaborate 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 arbitrarily. 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