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 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 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 permis￾sion, allowed by the thread, and not allowed for 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 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 cancella￾tive, 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