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 in1 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