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]0Modulo 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 per￾missions 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 , ∅