Deny-Guarantee Reasoning Mike Dodds',Xinyu Feng2,Matthew Parkinson,and Viktor Vafeiadis3 1 University of Cambridge,UK 2 Toyota Technological Institute at Chicago,USA 3 Microsoft Research Cambridge,UK Abstract.Rely-guarantee is a well-established approach to reasoning about con- current programs that use parallel composition.However,parallel composition is not how concurrency is structured in real systems.Instead,threads are started by 'fork'and collected with 'join'commands.This style of concurrency cannot be reasoned about using rely-guarantee,as the life-time of a thread can be scoped dynamically.With parallel composition the scope is static. In this paper,we introduce deny-guarantee reasoning,a reformulation of rely- guarantee that enables reasoning about dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recombined,in a similar way that separation logic splits and joins heaps.To allow this splitting,we use deny and guarantee permissions:a deny permission spec- ifies that the environment cannot do an action,and guarantee permission allow us to do an action.We illustrate the use of our proof system with examples,and show that it can encode all the original rely-guarantee proofs.We also present the semantics and soundness of the deny-guarantee method. 1 Introduction Rely-guarantee [10]is a well-established compositional proof method for reasoning about concurrent programs that use parallel composition.Parallel composition provides a structured form of concurrency:the lifetime of each thread is statically scoped,and therefore interference between threads is also statically known.In real systems,how- ever,concurrency is not structured like this.Instead,threads are started by a 'fork'and collected with'join'commands.The lifetime of such a thread is dynamically scoped in a similar way to the lifetime of heap-allocated data. In this paper,we introduce deny-guarantee reasoning,a reformulation of rely-guar- antee that enables reasoning about such dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recom- bined,in a similar way that separation logic splits and joins heaps. In rely-guarantee,interference is described using two binary relations:the rely,R, and the guarantee,G.Specifications of programs consist of a precondition,a post- condition and an interference specification.This setup is sufficient to reason about lexically-scoped parallel composition,but not about dynamically-scoped threads.With dynamically-scoped threads,the interference at the end of the program may be quite different from the interference at the beginning of the program,because during execu- tion other threads may have been forked or joined.Therefore,just as in Hoare logic
Deny-Guarantee Reasoning Mike Dodds1 , Xinyu Feng2 , Matthew Parkinson1 , and Viktor Vafeiadis3 1 University of Cambridge, UK 2 Toyota Technological Institute at Chicago, USA 3 Microsoft Research Cambridge, UK Abstract. Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by ‘fork’ and collected with ‘join’ commands. This style of concurrency cannot be reasoned about using rely-guarantee, as the life-time of a thread can be scoped dynamically. With parallel composition the scope is static. In this paper, we introduce deny-guarantee reasoning, a reformulation of relyguarantee that enables reasoning about dynamically scoped concurrency. We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs. We also present the semantics and soundness of the deny-guarantee method. 1 Introduction Rely-guarantee [10] is a well-established compositional proof method for reasoning about concurrent programs that use parallel composition. Parallel composition provides a structured form of concurrency: the lifetime of each thread is statically scoped, and therefore interference between threads is also statically known. In real systems, however, concurrency is not structured like this. Instead, threads are started by a ‘fork’ and collected with ‘join’ commands. The lifetime of such a thread is dynamically scoped in a similar way to the lifetime of heap-allocated data. In this paper, we introduce deny-guarantee reasoning, a reformulation of rely-guarantee that enables reasoning about such dynamically scoped concurrency. We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. In rely-guarantee, interference is described using two binary relations: the rely, R, and the guarantee, G. Specifications of programs consist of a precondition, a postcondition and an interference specification. This setup is sufficient to reason about lexically-scoped parallel composition, but not about dynamically-scoped threads. With dynamically-scoped threads, the interference at the end of the program may be quite different from the interference at the beginning of the program, because during execution other threads may have been forked or joined. Therefore, just as in Hoare logic
a program's precondition and postcondition may differ from each other,so in deny- guarantee logic a thread's pre-interference and post-interference specification may dif- fer from each other Main results The main contributions of this paper are summarized below: -We introduce deny-guarantee logic and apply it to an example(see $3 and $4). -We present an encoding of rely-guarantee into deny-guarantee,and show that every rely-guarantee proof can be translated into a deny-guarantee proof(see $5). -We prove that our proofrules are sound(see $6). -We have formalized our logic and all the proofs in Isabelle [4]. For clarity ofexposition,we shall present deny-guarantee in a very simple setting where the memory consists only ofa pre-allocated set of global variables.Our solution extends easily to a setting including memory allocation and deallocation (see $7). Related work Other work on concurrency verification has generally ignored fork/join, preferring to concentrate on the simpler case of parallel composition.This is true of all of the work on traditional rely-guarantee reasoning [10,11].This is unsurprising,as the development of deny-guarantee depends closely on the abstract characterization of sep- aration logic [3].However,even approaches such as SAGL [5]and RGSep [12]which combine rely-guarantee with separation logic omit fork/join from their languages. There exist already some approaches to concurrency that handle fork.Feng et al.[6] and Hobor et al.[9]both handle fork.However,both omit join with the justification that it can be handled by synchronization between threads.However,this approach is not compositional:it forces us to specify interference globally.Gotsman et al.[7] propose an approach to locks in the heap which includes both fork and join.However, this is achieved by defining an invariant over protected sections of the heap,which makes compositional reasoning about inter-thread interference impossible (see the next section for an example of this).Haack and Hurlin [8]have extended Gotsman et al.'s work to reason about fork and join in Java,where a thread can be joined multiple times. 2 Towards deny-guarantee logic Consider the very simple program given in Fig.1.If we run the program in an empty en- L0:x:=0; L1:t1 :fork(if(x==1)error; vironment,then at the end,we will get x =2 x:=1); This happens because the main thread will L2:t2 :fork(x :2; block at line L3 until thread t1 terminates. if (x==3)error); Hence,the last assignment to x will either be L3:join t1; that of thread t2 or of the main thread,both of L4:x:=2; which write the value 2 into x.We also know L5:join t2; that the error in the forked code on L1 and Fig.1.Illustration of fork/join L2 will never be reached. Now,suppose we want to prove that this program indeed satisfies the postcondition x=2.Unfortunately,this is not possible with existing compositional proof methods
a program’s precondition and postcondition may differ from each other, so in denyguarantee logic a thread’s pre-interference and post-interference specification may differ from each other. Main results The main contributions of this paper are summarized below: – We introduce deny-guarantee logic and apply it to an example (see §3 and §4). – We present an encoding of rely-guarantee into deny-guarantee, and show that every rely-guarantee proof can be translated into a deny-guarantee proof (see §5). – We prove that our proof rules are sound (see §6). – We have formalized our logic and all the proofs in Isabelle [4]. For clarity of exposition, we shall present deny-guarantee in a very simple setting where the memory consists only of a pre-allocated set of global variables. Our solution extends easily to a setting including memory allocation and deallocation (see §7). Related work Other work on concurrency verification has generally ignored fork/join, preferring to concentrate on the simpler case of parallel composition. This is true of all of the work on traditional rely-guarantee reasoning [10, 11]. This is unsurprising, as the development of deny-guarantee depends closely on the abstract characterization of separation logic [3]. However, even approaches such as SAGL [5] and RGSep [12] which combine rely-guarantee with separation logic omit fork/join from their languages. There exist already some approaches to concurrency that handle fork. Feng et al. [6] and Hobor et al. [9] both handle fork. However, both omit join with the justification that it can be handled by synchronization between threads. However, this approach is not compositional: it forces us to specify interference globally. Gotsman et al. [7] propose an approach to locks in the heap which includes both fork and join. However, this is achieved by defining an invariant over protected sections of the heap, which makes compositional reasoning about inter-thread interference impossible (see the next section for an example of this). Haack and Hurlin [8] have extended Gotsman et al.’s work to reason about fork and join in Java, where a thread can be joined multiple times. 2 Towards deny-guarantee logic L0: x := 0; L1: t1 := fork(if(x==1) error; x := 1); L2: t2 := fork(x := 2; if (x==3) error); L3: join t1; L4: x := 2; L5: join t2; Fig. 1. Illustration of fork/join Consider the very simple program given in Fig. 1. If we run the program in an empty environment, then at the end, we will get x = 2. This happens because the main thread will block at line L3 until thread t1 terminates. Hence, the last assignment to x will either be that of thread t2 or of the main thread, both of which write the value 2 into x. We also know that the error in the forked code on L1 and L2 will never be reached. Now, suppose we want to prove that this program indeed satisfies the postcondition x = 2. Unfortunately, this is not possible with existing compositional proof methods
Invariant-based techniques (such as Gotsman et al.[7])cannot handle this case,because they cannot describe interference.Unless we introduce auxiliary state to specify a more complex invariant,we cannot prove the postcondition,as it does not hold throughout the execution of the program. Rely-guarantee can describe interference,but still cannot handle this program.Con- sider the parallel rule: R1.G1H(P1)C1101]GICR2 R2,G2H(P2)C2 (02)G2CR1 RInR2,GIUG2F(PIAP2)C1lC2101A02) In this rule,the interference is described by the rely.R.which describes what the en- vironment can do.and the guarantee.G.which describes what the code is allowed to do.The rely and guarantee do not change throughout the execution of the code,they are'statically scoped'interference,whereas the scope of the interference introduced by fork and join commands is dynamic. Separation logic solves this kind of problem for dynamically allocated memory. also known as the heap.It uses the star operator to partition the heap into heap portions and to pass the portions around dynamically.The star operator on heaps is then lifted to assertions about heaps.In this work,we shall use the star operator to partition the interference between threads,and then lift it to assertions about the interference. Let us assume we have an assertion language which can describe interference.It has a separation-logic-like star operation.We would like to use this star to split and join interference,so that we can use simple rules to deal with fork and join: {P}CP2}. P*Px=fork CiP*Thread(x,.P刃(oRK） P*Thread(E,P产joinE*PT(oN） The FoRk rule simply removes the interference,P1,required by the forked code,C.and returns a token Thread(x,P2)describing the final state of the thread. The JoIN rule,knowing the thread E is dead, {T1*G2*D3*L*x≠1} simply takes over its final state' Now,we will consider how we might t1 =fork (if(x==1)error; x:=1); prove our motivating example.Let us imagine (G2*D3+L*Thread(t1,T1) we have some assertions that both allow us to t2 :fork (x :2; do updates to the state,and forbid the envi- if(x==3)error ) ronment from doing certain updates.We pro- L*Thread(t1.T1)*Thread(t2,G2*D3)} vide the full details in $4,and simply present join t1; the outline (Fig.2)and an informal explana- (T1 *L*Thread(t2.G2 *D3) tion of the permissions here.The first thread X=2; we fork can be verified using the T and x#1, (T1 +L*Thread(t2,G2+D3)*x=2) where 7 allows us to update x to be 1.and join t2 {T1*G2*D3*L*X=2} prevents any other thread updating x to be 1.Next,we use G2 which allows us to up- Fig.2.Proof outline date x to be 2:and D3 which prevents the 1 As in the pthread library,we allow a thread to be joined only once.We could also adapt the work of Haack and Hurlin [8]to our deny-guarantee setting to handle Java-style join
Invariant-based techniques (such as Gotsman et al. [7]) cannot handle this case, because they cannot describe interference. Unless we introduce auxiliary state to specify a more complex invariant, we cannot prove the postcondition, as it does not hold throughout the execution of the program. Rely-guarantee can describe interference, but still cannot handle this program. Consider the parallel rule: R1,G1 ⊢ {P1} C1 {Q1} G1 ⊆ R2 R2,G2 ⊢ {P2} C2 {Q2} G2 ⊆ R1 R1 ∩R2,G1 ∪G2 ⊢ {P1∧P2} C1 k C2 {Q1∧Q2} In this rule, the interference is described by the rely, R, which describes what the environment can do, and the guarantee, G, which describes what the code is allowed to do. The rely and guarantee do not change throughout the execution of the code, they are ‘statically scoped’ interference, whereas the scope of the interference introduced by fork and join commands is dynamic. Separation logic solves this kind of problem for dynamically allocated memory, also known as the heap. It uses the star operator to partition the heap into heap portions and to pass the portions around dynamically. The star operator on heaps is then lifted to assertions about heaps. In this work, we shall use the star operator to partition the interference between threads, and then lift it to assertions about the interference. Let us assume we have an assertion language which can describe interference. It has a separation-logic-like star operation. We would like to use this star to split and join interference, so that we can use simple rules to deal with fork and join: {P1} C {P2} ... {P∗P1} x := fork C {P∗Thread(x,P2)} () ... {P∗Thread(E,P ′ )} join E {P∗P ′ } () The rule simply removes the interference, P1, required by the forked code, C, and returns a token Thread(x,P2) describing the final state of the thread. {T1 ∗G2 ∗ D3 ∗ L ∗x , 1} t1 := fork (if(x==1) error; x := 1); {G2 ∗ D3 ∗ L ∗Thread(t1,T1)} t2 := fork (x := 2; if(x==3) error ); {L ∗Thread(t1,T1) ∗Thread(t2,G2 ∗ D3)} join t1; {T1 ∗ L ∗Thread(t2,G2 ∗ D3)} x := 2; {T1 ∗ L ∗Thread(t2,G2 ∗ D3) ∗x = 2} join t2 {T1 ∗G2 ∗ D3 ∗ L ∗x = 2} Fig. 2. Proof outline The rule, knowing the thread E is dead, simply takes over its final state1 . Now, we will consider how we might prove our motivating example. Let us imagine we have some assertions that both allow us to do updates to the state, and forbid the environment from doing certain updates. We provide the full details in §4, and simply present the outline (Fig. 2) and an informal explanation of the permissions here. The first thread we fork can be verified using the T1 and x , 1, where T1 allows us to update x to be 1, and prevents any other thread updating x to be 1. Next, we use G2 which allows us to update x to be 2; and D3 which prevents the 1 As in the pthread library, we allow a thread to be joined only once. We could also adapt the work of Haack and Hurlin [8] to our deny-guarantee setting to handle Java-style join
environment from updating x to be 3.These two permissions are sufficient to ver- ify the second thread.Finally,L is a leftover permission which prevents any other thread updating x to be any value other than 1 or 2.When we get to the assign- ment,we have TI*L which forbids the environment performing any update except assigning x with 2.Hence,we know that the program will terminate with x=2. Now,we consider how to build a logic to represent the permission on interference used in (me,-env) the proof outline.Let us consider the information contained in a rely-guarantee pair.For each state quar deny change it has one of four possibilities presented （me,enu） (me,一enU) in Fig.3:guar permission,allowed by both the (me,env】 thread and the environment (me,env);I permis- sion,allowed by the thread,and not allowed for Fig.3.Possible interference the environment(me,env);0 permission,not al- lowed by the thread,but allowed by the environment (me,env);and deny permission, not allowed by the thread or the environment(-me,env). To allow inter-thread reasoning about interference,we want to split full permissions 1 into either deny permissions or guar permissions.We also want to further split deny, or guar,permissions into smaller deny or guar permissions respectively.The arrows of Fig.3 show the order of permission strength captured by splitting.If a thread has a deny on a state change,it can give another thread a deny and keep one itself while preserving the fact that the state change is prohibited for itself and the environment.The same holds for guar. To preserve soundness,we cannot allow unrestricted copying of permissions-we must treat them as resources.Following Boyland [2]and Bornat et al.[1]we attach weights to splittable resources.In particular we use fractions in the interval(0,1).For example,we can split an (a+b)deny into an (a)deny and a (b)deny,and similarly for guar permissions.We can also split a full permission I into (a)deny and(b)deny,or (a)guar and (b)guar,where a+b=1. In the following sections we will show how these permissions can be used to build deny-guarantee,a separation logic for interference. Aside Starting with the parallel composition rules of rely-guarantee and of separation logic,you might wonder if we can define our star as(R1,G)*(R2.G2)=(RInR2,GIU G2)provided GI C R2 and G2 C Ri,and otherwise it is undefined.Here we have taken the way rely-guarantee combines the relations,and added it to the definition of * This definition,however,does not work.The star we have defined is not cancella- tive,a condition that is required for proving that separation is sound [3].Cancellativity says that for all x,y and =ifx*y is defined and x*y=x*,then y==.Intuitively,the problem is that n and U lose information about the overlap. 3 The Logic Language The language is defined in Fig.4.This is a standard language with two additional commands for forking a new thread and for joining with an existing thread
environment from updating x to be 3. These two permissions are sufficient to verify the second thread. Finally, L is a leftover permission which prevents any other thread updating x to be any value other than 1 or 2. When we get to the assignment, we have T1 ∗ L which forbids the environment performing any update except assigning x with 2. Hence, we know that the program will terminate with x = 2. 1 0 (me,¬env) (¬me,¬env) (¬me, env) (me, env) guar deny Fig. 3. Possible interference Now, we consider how to build a logic to represent the permission on interference used in the proof outline. Let us consider the information contained in a rely-guarantee pair. For each state change it has one of four possibilities presented in Fig. 3: guar permission, allowed by both the thread and the environment (me,env); 1 permission, allowed by the thread, and not allowed for the environment (me,¬env); 0 permission, not allowed by the thread, but allowed by the environment (¬me,env); and deny permission, not allowed by the thread or the environment (¬me,¬env). To allow inter-thread reasoning about interference, we want to split full permissions 1 into either deny permissions or guar permissions. We also want to further split deny, or guar, permissions into smaller deny or guar permissions respectively. The arrows of Fig. 3 show the order of permission strength captured by splitting. If a thread has a deny on a state change, it can give another thread a deny and keep one itself while preserving the fact that the state change is prohibited for itself and the environment. The same holds for guar. To preserve soundness, we cannot allow unrestricted copying of permissions – we must treat them as resources. Following Boyland [2] and Bornat et al. [1] we attach weights to splittable resources. In particular we use fractions in the interval (0,1). For example, we can split an (a +b)deny into an (a)deny and a (b)deny, and similarly for guar permissions. We can also split a full permission 1 into (a)deny and (b)deny, or (a)guar and (b)guar, where a+b = 1. In the following sections we will show how these permissions can be used to build deny-guarantee, a separation logic for interference. Aside Starting with the parallel composition rules of rely-guarantee and of separation logic, you might wonder if we can define our star as (R1,G1) ∗ (R2,G2) = (R1∩R2,G1 ∪ G2) provided G1 ⊆ R2 and G2 ⊆ R1, and otherwise it is undefined. Here we have taken the way rely-guarantee combines the relations, and added it to the definition of ∗. This definition, however, does not work. The star we have defined is not cancellative, a condition that is required for proving that separation is sound [3]. Cancellativity says that for all x, y and z, if x ∗ y is defined and x ∗ y = x ∗ z, then y = z. Intuitively, the problem is that ∩ and ∪ lose information about the overlap. 3 The Logic Language The language is defined in Fig. 4. This is a standard language with two additional commands for forking a new thread and for joining with an existing thread
(Expr)E::=x n E+EE-E .. (BExp)B ::true false=E#E... (Stmts)C::=x:=E I skip C;C l if B then C else C I while B do Cx:=fork C l join E Fig.4.The Language Informally,the x:=fork C command allocates an unused thread identifier t,creates a new thread with thread identifier t and body C,and makes it run in parallel with the rest of the program.Finally,it returns the thread identifier t by storing it in x.The command join E blocks until thread E terminates;it fails if E is not a valid thread identifier. For simplicity,we assume each primitive operation is atomic.The formal operational semantics is presented in $6. Deny-Guarantee Permissions The main component of our logic is the set of deny- guarantee permissions,PermDG.A deny-guarantee permission is a function that maps each action altering a single variable2 to a certain deny-guarantee fraction: Vars c {xy,2,…} n E Vals def z States der Vars→Vals a∈ Actions def {o[x→ml,r[x→t]loe States A n≠l) f∈FractionDG {(deny,π)lπ∈(0,1)}U{(guar,π)lπ∈(0,1)}U{0,1 pr∈PermDG der Actions→FractionDG We sometimes write deny-guarantee fractions in FractionDG in shorthand,with d for (deny,π)，andπgfor(guar,π). The fractions represent a permission or a prohibition to perform a certain action. The first two kinds of fractions are symmetric:(deny,)says that nobody can do the action;(guar,)says that everybody can do the action.The last two are not:I represents full control over the action(only I can do the action),whereas 0 represents no control over an action (others can do it,but I cannot). From a deny-guarantee permission,pr,we can extract a pair of rely-guarantee con- ditions.The rely contains those actions permitted to the environment,while the guaran- tee contains those permitted to the thread(see Fig.3). I-】∈PermDG→P(Actions)xP(Actions) Ipr(a Ipr(a)=(guar.)vpr(a)=0). [a Ipr(a)=(guar,-)v pr(a)=1)) As shorthand notations,we will use pr.R and pr.G to represent the first and the second element in Iprl respectively. 2 We do not consider updates to simultaneous locations as it complicates the presentation
(Expr) E ::= x | n | E + E | E - E | ... (BExp) B ::= true | false | E = E | E , E | ... (Stmts) C ::= x := E | skip | C;C | if B then C else C | while B do C | x := fork C | join E Fig. 4. The Language Informally, the x := fork C command allocates an unused thread identifier t, creates a new thread with thread identifier t and body C, and makes it run in parallel with the rest of the program. Finally, it returns the thread identifier t by storing it in x. The command join E blocks until thread E terminates; it fails if E is not a valid thread identifier. For simplicity, we assume each primitive operation is atomic. The formal operational semantics is presented in §6. Deny-Guarantee Permissions The main component of our logic is the set of denyguarantee permissions, PermDG. A deny-guarantee permission is a function that maps each action altering a single variable2 to a certain deny-guarantee fraction: Vars def = {x, y,z,...} n ∈ Vals def = Z σ ∈ States def = Vars → Vals a ∈ Actions def = {σ[x 7→ n],σ[x 7→ n ′ ] | σ ∈ States ∧ n , n ′ } f ∈ FractionDG def = {(deny, π) | π ∈ (0,1)} ∪ {(guar, π) | π ∈ (0,1)} ∪ {0,1} pr ∈ PermDG def = Actions → FractionDG We sometimes write deny-guarantee fractions in FractionDG in shorthand, with πd for (deny, π), and πg for (guar, π). The fractions represent a permission or a prohibition to perform a certain action. The first two kinds of fractions are symmetric: (deny, π) says that nobody can do the action; (guar, π) says that everybody can do the action. The last two are not: 1 represents full control over the action (only I can do the action), whereas 0 represents no control over an action (others can do it, but I cannot). From a deny-guarantee permission, pr, we can extract a pair of rely-guarantee conditions. The rely contains those actions permitted to the environment, while the guarantee contains those permitted to the thread (see Fig. 3). ~ ∈ PermDG → P(Actions)× P(Actions) ~pr def = ({a | pr(a) = (guar, )∨ pr(a) = 0}, {a | pr(a) = (guar, )∨ pr(a) = 1}) As shorthand notations, we will use pr.R and pr.G to represent the first and the second element in ~pr respectively. 2 We do not consider updates to simultaneous locations as it complicates the presentation
T,pr,Y卡B ([B]o =tt)A(Va.pr(a)=0)A(y=0) o.pr.y pr' (Y=0)A(pr=pr) o,pr.y full (y=0)A(Na.pr(a)=1) c,pr,y卡Thread(E,P-y=[IEo→PI o.pr.y P1*P2 pri,pr2,y1,y2.pr priepr2ay=yiy2 A(c,pr1,y1卡Pi)A(c,pr2,y2乍P2) where means the union of disjoint sets. o,pr.yF P1-P2 Hpr1,p2,YI,Y2.pr2=pr⊕pr1AY2=y世y1 A (o.pr1.y1FP1)implies (o.pr2.Y2 F P2) Fig.5.Semantics of Assertions Note that the deny and guar labels come with a fractional coefficient.These coeffi- cients are used in defining the addition of two deny-guarantee fractions 0⊕x些x⊕0sx (deny)(denyfI then (deny.) else if,π+π'=1 then 1 else undef (guar,(guar.f I then (guar else if.π+π'=1 then 1 else undef 1xfx=0then 1 else undef The addition of two deny-guarantee permissions,pr=pripr2,is defined so that for all aE Actions,pr(a)=pri(a)pr2(a).The permission inverse inv is defined so inv(1)=0, iv(0)=l,iv(guar,π)=(guar,1-π)，and inv(deny,π)=(deny,1-π). It is easy to show that addition is commutative,associative,cancellative,and has 0 as a unit element.This allows us to define a separation logic over PermDG. Assertions and Judgements The assertions are defined below. P.O::=B I pr I full l false I Thread(E,P)I P=P*P-l 3x.P An assertion P is interpreted as a predicate over a program state o,a permission token pr,and a thread queue y.A thread queue,as defined below,is a finite partial function mapping thread identifiers to the postcondition established by the thread when it terminates EThreadIDs N yThreadQueues ThreadlDs一→inAssertions Semantics of assertions is defined in Fig.5. The judgments for commands are in the form of (P)C(O).As in Hoare Logic, a command is specified by a precondition(P)and a postcondition(O).Informally,it means that if the precondition,P,holds in the initial configuration and the environment
σ, pr, γ |= B ⇐⇒ ([[B]]σ = tt)∧(∀a. pr(a) = 0)∧(γ = ∅) σ, pr, γ |= pr′ ⇐⇒ (γ = ∅)∧(pr = pr′ ) σ, pr, γ |= full ⇐⇒ (γ = ∅)∧(∀a. pr(a) = 1) σ, pr, γ |= Thread(E,P) ⇐⇒ γ = [[[E]]σ 7→ P] σ, pr, γ |= P1 ∗ P2 ⇐⇒ ∃pr1, pr2, γ1, γ2. pr = pr1 ⊕ pr2 ∧γ = γ1 ⊎γ2 ∧ (σ, pr1, γ1 |= P1)∧(σ, pr2, γ2 |= P2) where ⊎ means the union of disjoint sets. σ, pr, γ |= P1 −∗ P2 ⇐⇒ ∀pr1, pr2, γ1, γ2. pr2 = pr ⊕ pr1 ∧γ2 = γ⊎γ1 ∧ (σ, pr1, γ1 |= P1) implies (σ, pr2, γ2 |= P2) Fig. 5. Semantics of Assertions Note that the deny and guar labels come with a fractional coefficient. These coeffi- cients are used in defining the addition of two deny-guarantee fractions. 0⊕ x def = x⊕0 def = x (deny, π)⊕(deny, π′ ) def = if π+π ′ < 1 then (deny, π+π ′ ) else if π+π ′ = 1 then 1 else undef (guar, π)⊕(guar, π′ ) def = if π+π ′ < 1 then (guar, π+π ′ ) else if π+π ′ = 1 then 1 else undef 1⊕ x def = x⊕1 def = if x = 0 then 1 else undef The addition of two deny-guarantee permissions, pr = pr1⊕ pr2, is defined so that for all a ∈ Actions, pr(a) = pr1(a)⊕ pr2(a). The permission inverse inv is defined so inv(1) = 0, inv(0) = 1, inv(guar, π) = (guar,1−π), and inv(deny, π) = (deny,1−π). It is easy to show that addition is commutative, associative, cancellative, and has 0 as a unit element. This allows us to define a separation logic over PermDG. Assertions and Judgements The assertions are defined below. P,Q ::= B | pr | full | false | Thread(E,P) | P ⇒ Q | P∗ Q | P−∗ Q | ∃x.P An assertion P is interpreted as a predicate over a program state σ, a permission token pr, and a thread queue γ. A thread queue, as defined below, is a finite partial function mapping thread identifiers to the postcondition established by the thread when it terminates. t ∈ ThreadIDs def = N γ ∈ ThreadQueues def = ThreadIDs ⇀fin Assertions Semantics of assertions is defined in Fig. 5. The judgments for commands are in the form of {P} C {Q}. As in Hoare Logic, a command is specified by a precondition (P) and a postcondition (Q). Informally, it means that if the precondition, P, holds in the initial configuration and the environment
P1 precise (P1)C (P2)x fv(P1+P3) Thread(x,P2)*P3 P4 allowed(Ix :=+].P3) (FORK) (P1*P3)x :fork P.P]C (P4) P1→P1{P}CP}P3→P (P+Thread(E.P)join EP(oIN) (CONS) {P}C{P2} (P)C(P']stable(Po) (FRAME) P→E因allowed(x=E1卫(asN P*PolCIP'*Pol [PIX :=E(P' Fig.6.Proof Rules adheres to its specification,then the command C is safe to execute;moreover every forked thread will fulfil its specification and if C terminates,the final configuration will satisfy O.A formal definition of the semantics is presented in $6. The main proof rules are shown in Fig.6.The proof rules are covered by a general side-condition requiring that any assertion we write in a triple is stable.Intuitively this means that the assertion still holds under any interference from the environment,as expressed in the deny.Requiring stability for every assertion in a triple removes the need for including explicit stability checks in the proof rules,simplifying the presentation. Definition 1 (Stability).An assertion P is stable (written stable(P))if and only if.for allo,o',pr and y,ifo,pr,yP and (,')E pr.R,then a',pr,yP. The fork and assign rules include allowed-statements,which assert that particular rewrites are permitted by deny-guarantee assertions.Rewrites are given as relations over states.In the rules,we write Ix:=Ell for the relation over states denoted by assigning E to x,where E can be for non-deterministic assignment. Definition 2 (Allowed).Let K be a relation over states.Then allowed(K,P)holds if and only if.for all o,'pr and y,ifo,pr,y P and (,')EK.then (,')E pr.G. The assignment rule is an adaptation of Hoare's assignment axiom for sequential programs.In order to deal with concurrency,it checks that the command has enough permission(pr)to update the shared state. The fork and join rules modify the rules given in [7].The fork rule takes a pre- condition and converts it into a Thread-predicate recording the thread's expected post- condition.The rule checks that any pr satisfying the context P3 is sufficient to allow assignment to the thread variable x.It requires that the variable x used to store the thread identifier is not in fv(PI*P3),the free variables for the precondition.As with Gotsman et al.[7],the rule also requires that the precondition Pi is precise. The join rule takes a thread predicate and replaces it with the corresponding post- condition.The frame and consequence rules are modified from standard separation- logic rules.Other rules are identical to the standard Hoare logic rules
P1 precise {P1} C {P2} x < fv(P1 ∗ P3) Thread(x,P2) ∗ P3 ⇒ P4 allowed([[x := ∗]],P3) {P1 ∗ P3} x := fork[P1,P2] C {P4} () {P∗Thread(E,P ′ )} join E {P∗ P ′ } () P1 ⇒ P ′ 1 {P ′ 1 } C {P ′ 2 } P ′ 2 ⇒ P2 {P1} C {P2} () {P} C {P ′ } stable(P0) {P∗ P0} C {P ′ ∗ P0} () P ⇒ [E/x]P ′ allowed([[x := E]],P) {P} x := E {P ′ } () Fig. 6. Proof Rules adheres to its specification, then the command C is safe to execute; moreover every forked thread will fulfil its specification and if C terminates, the final configuration will satisfy Q. A formal definition of the semantics is presented in §6. The main proof rules are shown in Fig. 6. The proof rules are covered by a general side-condition requiring that any assertion we write in a triple is stable. Intuitively this means that the assertion still holds under any interference from the environment, as expressed in the deny. Requiring stability for every assertion in a triple removes the need for including explicit stability checks in the proof rules, simplifying the presentation. Definition 1 (Stability). An assertion P is stable (written stable(P)) if and only if, for all σ, σ ′ , pr and γ, if σ, pr, γ |= P and (σ,σ′ ) ∈ pr.R, then σ ′ , pr, γ |= P. The fork and assign rules include allowed-statements, which assert that particular rewrites are permitted by deny-guarantee assertions. Rewrites are given as relations over states. In the rules, we write ~x := E for the relation over states denoted by assigning E to x, where E can be ∗ for non-deterministic assignment. Definition 2 (Allowed). Let K be a relation over states. Then allowed(K,P) holds if and only if, for all σ, σ ′ , pr and γ, if σ, pr, γ |= P and (σ,σ′ ) ∈ K, then (σ,σ′ ) ∈ pr.G. The assignment rule is an adaptation of Hoare’s assignment axiom for sequential programs. In order to deal with concurrency, it checks that the command has enough permission (pr) to update the shared state. The fork and join rules modify the rules given in [7]. The fork rule takes a precondition and converts it into a Thread-predicate recording the thread’s expected postcondition. The rule checks that any pr satisfying the context P3 is sufficient to allow assignment to the thread variable x. It requires that the variable x used to store the thread identifier is not in fv(P1 ∗ P3), the free variables for the precondition. As with Gotsman et al. [7], the rule also requires that the precondition P1 is precise. The join rule takes a thread predicate and replaces it with the corresponding postcondition. The frame and consequence rules are modified from standard separationlogic rules. Other rules are identical to the standard Hoare logic rules
1{T1*G2*G2*D3*D3*L'*X+1} 2 t1 :fork[T(x+I)Ti](if(x==1)error;x :=1) 3 (G2*G2*D3+D3+L'*Thread(t1,T1) t2 :=forkG.D.G2D:](x :=2;if(x==3)error) 5 (G2+D3+L'+Thread(t1,T1)*Thread(t2.G2 *D3)) 6 join t1; 7 (TI+G2+D3+L'+Thread(t2.G2+D3) 8 x:=2; 9{T1*G2*D3*'*Thread(t2,G2*D3)*x=2} 10 join t2; 11{T1*G2*G2*D3*D3*L'*X=2引 whereT世K:zw小，Gg些x:Zw24gDgx:Zw3 and L' 些[x:zw{1,2,31-*u Fig.7.Proof outline of the fork/join example 4 Two-thread example In $2 we said that the program shown in Fig.I cannot be verified in conventional rely-guarantee reasoning.We now show that deny-guarantee allows us to verify this example.The proof outline is given in Fig.7. We use the following notation to represent permissions.Here xE Vars,A,BC Vals and fE FractionDG. x:A B der ((ofxv]xIEStateAvEAAYEBAY+Y) IXIr det a. f ifaex 10 otherwise Lemma 3 (Permission splitting). [x:AwB世B]r→[x:AB]r*[x:AwB]/ [x:Aw Blfof [x:A B]f*[x:A B] Lemma 4 (Permission subtraction).If P is precise and satisfiable,then (P-*full)* P一ful. Proof.Holds because (P-*)*PA(P*true)and full=P*true hold for any precise and satisfiable P and any O. ▣ The fork/join program has precondition(full *x+1),giving the full permission,1, on every action.The permission [x:Z(1,2,3)]I permits any rewrite of the variable x to the value 1,2 or 3,and prohibits all other rewrites.By Lemma 4, ful=([x:Zw1,2,3]1*ful)*[x:Zw{1,2,3]1 By Lemma 3 can split [x:Z(1,2,3)]1 as follows [x:Zw1,2,31→[x:Zw1]1*[x:Zw2]1*[x:Z3]1 一T1*G2*G2*D3*D3
1 {T1 ∗G2 ∗G2 ∗ D3 ∗ D3 ∗ L ′ ∗ x , 1} 2 t1 := fork[T1∗(x,1),T1] (if(x==1) error; x := 1) 3 {G2 ∗G2 ∗ D3 ∗ D3 ∗ L ′ ∗Thread(t1,T1)} 4 t2 := fork[G2 ∗D3,G2 ∗D3 ] (x := 2; if(x==3) error) 5 {G2 ∗ D3 ∗ L ′ ∗Thread(t1,T1) ∗Thread(t2,G2 ∗ D3)} 6 join t1; 7 {T1 ∗G2 ∗ D3 ∗ L ′ ∗Thread(t2,G2 ∗ D3)} 8 x := 2; 9 {T1 ∗G2 ∗ D3 ∗ L ′ ∗Thread(t2,G2 ∗ D3) ∗x = 2} 10 join t2; 11 {T1 ∗G2 ∗G2 ∗ D3 ∗ D3 ∗ L ′ ∗x = 2} where T1 def = [x: Z 1]1, G2 def = [x: Z 2] 1 2 g , D3 def = [x: Z 3] 1 2 d , and L ′ def = [x: Z {1,2,3}]1 −∗ full Fig. 7. Proof outline of the fork / join example 4 Two-thread example In §2 we said that the program shown in Fig. 1 cannot be verified in conventional rely-guarantee reasoning. We now show that deny-guarantee allows us to verify this example. The proof outline is given in Fig. 7. We use the following notation to represent permissions. Here x ∈ Vars, A,B ⊆ Vals and f ∈ FractionDG. x: A B def = {(σ[x 7→ v],σ[x 7→ v ′ ]) | σ ∈ State∧v ∈ A∧v ′ ∈ B∧v , v ′ } [X]f def = λa. f if a ∈ X 0 otherwise Lemma 3 (Permission splitting). [x: A B⊎ B ′ ]f ⇐⇒ [x: A B]f ∗ [x: A B ′ ]f [x: A B]f ⊕ f ′ ⇐⇒ [x: A B]f ∗ [x: A B]f ′ Lemma 4 (Permission subtraction). If P is precise and satisfiable, then (P −∗ full) ∗ P ⇐⇒ full. Proof. Holds because (P−∗ Q) ∗ P ⇐⇒ Q ∧(P∗ true) and full ⇒ P∗ true hold for any precise and satisfiable P and any Q. The fork / join program has precondition {full ∗ x , 1}, giving the full permission, 1, on every action. The permission [x: Z {1,2,3}]1 permits any rewrite of the variable x to the value 1, 2 or 3, and prohibits all other rewrites. By Lemma 4, full ⇐⇒ ([x: Z {1,2,3}]1 −∗ full) ∗ [x: Z {1,2,3}]1 By Lemma 3 can split [x: Z {1,2,3}]1 as follows [x: Z {1,2,3}]1 ⇐⇒ [x: Z 1]1 ∗ [x: Z 2]1 ∗ [x: Z 3]1 ⇐⇒ T1 ∗G2 ∗G2 ∗ D3 ∗ D3
where T1,G2 and D3 are defined in Fig.7.We define L'as ([x:Z(1,2,3)]1-*full) (the L used in the proof sketch in Fig.2 is L'*G2*D3).Consequently,we can derive the precondition (T1 *G2*G2*D3 *D3*L'*x1) The specification for thread t1 is shown below.Note that x+I is stable because TI prevents the environment from writing I into x.The post-condition does not include x=1,because Ti does not prohibit the environment from writing other values into x. {T1*x≠1}1f(x==1)error;x:=1;{T1} The specification for thread t2 is shown below.The assertion x#3 is stable because the permission D3 is a deny prohibiting the environment from writing 3 in x.Note that a deny is used rather than full permission because another instance of D3 is needed to ensure stability of the assertion on line 9,before the main thread joins t2. (G2*D3)x:=2;(G2*D3*x+3]if(x==3)error (G2*D3) The specifications for t1 and t2 allow us to apply the fork rule (lines 2 and 4). We then join the thread t1 and recover the permission Ti(line 6).Then we apply the assignment rule for the assignment x :2 (line 8). The post-condition x =2 on line 9 is stable because TI *L'gives the exclusive permission,1,on every rewrite except rewrites of x with value 2 or 3,and the deny D3 prohibits rewrites of x with value 3.Consequently the only permitted interference from the environment is to write 2 into x,so x=2 is stable. Finally we apply the join rule,collect the permissions held by the thread t2,and complete the proof. 5 Encoding rely-guarantee reasoning In this section,we show that the traditional rely-guarantee reasoning can be embedded into our deny-guarantee reasoning.First,we present an encoding of parallel composi- tion using the fork and join commands,and derive a proof rule.Then,we prove that every rely-guarantee proof for programs using parallel composition can be translated into a corresponding deny-guarantee proof. 5.1 Adding parallel composition We encode parallel composition into our language by the following translation: CI)C=forkyp.C1:C2:joinx Here the annotations P1.O are required to provide the translation onto the fork,which requires annotations.x is an intermediate variable used to hold the identifier for thread CI.We assume that x is a fresh variable that is not used in Cl or C2.The parallel composition rule for deny-guarantee is as follows: (P1]C1 (O1)(P2)C2(O2)xfv(P1,P2.C1.C2.01.02)P1 precise [P1*P2 *full(x))C1 llx.P10)C2101*02*full(x) (PAR)
where T1, G2 and D3 are defined in Fig. 7. We define L ′ as ([x: Z {1,2,3}]1 −∗ full) (the L used in the proof sketch in Fig. 2 is L ′ ∗G2 ∗ D3). Consequently, we can derive the precondition {T1 ∗G2 ∗G2 ∗ D3 ∗ D3 ∗ L ′ ∗ x , 1} The specification for thread t1 is shown below. Note that x , 1 is stable because T1 prevents the environment from writing 1 into x. The post-condition does not include x = 1, because T1 does not prohibit the environment from writing other values into x. { T1 ∗ x , 1} if(x==1) error; x := 1; { T1} The specification for thread t2 is shown below. The assertion x , 3 is stable because the permission D3 is a deny prohibiting the environment from writing 3 in x. Note that a deny is used rather than full permission because another instance of D3 is needed to ensure stability of the assertion on line 9, before the main thread joins t2. {G2 ∗ D3} x := 2; {G2 ∗ D3 ∗ x , 3} if(x==3) error {G2 ∗ D3} The specifications for t1 and t2 allow us to apply the fork rule (lines 2 and 4). We then join the thread t1 and recover the permission T1 (line 6). Then we apply the assignment rule for the assignment x := 2 (line 8). The post-condition x = 2 on line 9 is stable because T1 ∗ L ′ gives the exclusive permission, 1, on every rewrite except rewrites of x with value 2 or 3, and the deny D3 prohibits rewrites of x with value 3. Consequently the only permitted interference from the environment is to write 2 into x, so x = 2 is stable. Finally we apply the join rule, collect the permissions held by the thread t2, and complete the proof. 5 Encoding rely-guarantee reasoning In this section, we show that the traditional rely-guarantee reasoning can be embedded into our deny-guarantee reasoning. First, we present an encoding of parallel composition using the fork and join commands, and derive a proof rule. Then, we prove that every rely-guarantee proof for programs using parallel composition can be translated into a corresponding deny-guarantee proof. 5.1 Adding parallel composition We encode parallel composition into our language by the following translation: C1 k(x,P1,Q1) C2 def = x := fork[P1,Q1] C1; C2; join x Here the annotations P1,Q1 are required to provide the translation onto the fork , which requires annotations. x is an intermediate variable used to hold the identifier for thread C1. We assume that x is a fresh variable that is not used in C1 or C2. The parallel composition rule for deny-guarantee is as follows: {P1} C1 {Q1} {P2} C2 {Q2} x < fv(P1,P2,C1,C2,Q1,Q2) P1 precise {P1 ∗ P2 ∗ full(x)} C1 k(x,P1,Q1) C2 {Q1 ∗ Q2 ∗ full(x)} ()
Modulo the side-conditions about x and precision,and the full(x)star-conjunct,this is the same rule as in separation logic.The assertion full(x)stands for the full permission on the variable x;that is,we have full permission to assign any value to x. ful(x(c,c')det ifor[x→y=dAv≠o)then 1,else0 We extend this notation to sets of variables:full()full(full). Precision is required as the underlying fork rule requires it.This makes this rule weaker than if we directly represented the parallel composition in the semantics. Lemma 5.The parallel composition rule can be derived from the rules given in Fig.6. Proof.The proof has the following outline. (P1 P2 *full()) x:=forkIP1.01]C1 (Thread(x,1)*P2 *full(x)) C2 (Thread(,1)*2 *full()) join x {Q1*Q2*ful(x)》 The first step uses the first premise,and the frame and fork rules.The second step uses the second premise and the frame rule.The final step uses the frame and join rules. 5.2 Translation Now let us consider the translation of rely-guarantee proofs into the deny-guarantee framework.The encoding of parallel composition into fork and join introduces extra variables,so we partition variables in constructed fork-join programs into two kinds: Vars,the original program variables,and TVars,variables introduced to carry thread identifiers.We will assume that the relies and guarantees from the original proofassume that the TVars are unchanged. In $3,we showed how to extract a pair of rely-guarantee conditions from per- missions pre PermDG.Conversely,we can encode rely-guarantee pairs into sets of PermDG permissions as follows: H ∈P(Actions)xP(Actions)→P(PermDG) IR.Gl ((R.G)FIFEActions(0.1) (guar,F(a)) a∈RAa∈G (R.G)Fa. 0 a∈RAagG a生RAa∈G (deny.F(a)) a年RAagG First,we show that our translation is non-empty:each pair maps to something: Lemma 6 (Non-empty translation).VR,G.[R,G]0
Modulo the side-conditions about x and precision, and the full(x) star-conjunct, this is the same rule as in separation logic. The assertion full(x) stands for the full permission on the variable x; that is, we have full permission to assign any value to x. full(x)(σ,σ′ ) def = if σ[x 7→ v] = σ ′ ∧v , σ(x) then 1, else 0 We extend this notation to sets of variables: full({x1,...,xn}) def = full(x1)⊕...⊕full(xn). Precision is required as the underlying fork rule requires it. This makes this rule weaker than if we directly represented the parallel composition in the semantics. Lemma 5. The parallel composition rule can be derived from the rules given in Fig. 6. Proof. The proof has the following outline. {P1 ∗ P2 ∗ full(x)} x := fork[P1,Q1] C1 {Thread(x,Q1) ∗ P2 ∗ full(x)} C2 {Thread(x,Q1) ∗ Q2 ∗ full(x)} join x {Q1 ∗ Q2 ∗ full(x)} The first step uses the first premise, and the frame and fork rules. The second step uses the second premise and the frame rule. The final step uses the frame and join rules. 5.2 Translation Now let us consider the translation of rely-guarantee proofs into the deny-guarantee framework. The encoding of parallel composition into fork and join introduces extra variables, so we partition variables in constructed fork-join programs into two kinds: Vars, the original program variables, and TVars, variables introduced to carry thread identifiers. We will assume that the relies and guarantees from the original proof assume that the TVars are unchanged. In §3, we showed how to extract a pair of rely-guarantee conditions from permissions pr ∈ PermDG. Conversely, we can encode rely-guarantee pairs into sets of PermDG permissions as follows: ~ ∈ P(Actions)× P(Actions) → P(PermDG) ~R,G def = {hR,GiF | F ∈ Actions → (0,1)} hR,GiF def = λa. (guar,F(a)) a ∈ R∧a ∈ G 0 a ∈ R∧a < G 1 a < R∧a ∈ G (deny,F(a)) a < R∧a < G First, we show that our translation is non-empty: each pair maps to something: Lemma 6 (Non-empty translation). ∀R,G. ~R,G , ∅
