(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 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 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 con￾ditions. The rely contains those actions permitted to the environment, while the guaran￾tee 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