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