Syntactic Control of Interference and Concurrent Separation Logic

AbstractAt last yearʼs MFPS conference we introduced a revised version of Concurrent Separation Logic in which assertions are tagged with a “rely set” of variables assumed to be unmodified by other processes. We showed that this logic is compositional and sound with respect to an action trace semantics. The revision was motivated by a subtle issue concerning soundness of the original version of the logic, discovered by Ian Wehrman and Josh Berdine. The revised logic fixes this problem and also relaxes the Owicki-Gries constraints on variables, allowing shared variables to be protected by multiple resources rather than a single one, but requiring that a process writing to a shared variable must acquire all resources that protect it, while a process reading a shared variable need only acquire one such resource. This generalization brings concurrent separation logic closer in spirit to permission-based logics, although our formulation makes no explicit mention of permissions. At the same conference, Uday Reddy introduced a concurrent separation logic with static permissions for variables, generalizing John Reynoldsʼs ideas on syntactic control of interference to a concurrent setting. Here we show that there is an extremely close relationship between these two logics. Essentially, every provable assertion in Reddyʼs logic corresponds to a provable assertion in CSL with the same semantic content; and every provable assertion in CSL corresponds to a multitude of assertions in Reddyʼs logic, differing only in the choice of specific permission values. We show that every derivation in Reddyʼs logic can be transformed into a derivation in CSL, by abstracting away from permission details while retaining the relevant information about protection of variables by resources. And we show how to construct, for a given CSL derivation, a family of corresponding derivations in Reddyʼs logic that differ only in inessential permission choices. These results also imply that one can establish soundness of Reddyʼs logic by appealing to soundness of CSL, leading to a simpler soundness proof than the one given in Reddyʼs original paper, which used an augmented form of action trace semantics