Variables as Resource for Shared-Memory Programs: Semantics and Soundness

Parkinson, Bornat, and Calcagno recently introduced a logic for partial correctness in which program variables are treated as resource, generalizing earlier work based on separation logic and permissions. An advantage of their approach is that it yields a logic devoid of complex side conditions: there is no need to pepper the inference rules with “modifies” clauses. They used a simple operational semantics to prove soundness of the sequential fragment of their logic, and they showed that the inference rules of concurrent separation logic can be translated directly into their framework. Their concurrency rules are strictly more powerful than those of concurrent separation logic, since the new logic allows proofs of programs that perform concurrent reads. We provide a denotational semantics and a soundness proof for the concurrent fragment of their logic, extending our earlier work on concurrent separation logic to incorporate permissions in a natural manner.