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 threadprivate 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 guarantee conditions are all actions. Similar to the separating conjunction 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 support 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 resources, 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 inappropriate 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 consecutive 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 systemwide 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]] respectively. [[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