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 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 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 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 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 en￾vironment, 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