Discussing "Separation Logic: A Logic for Shared Mutable Data Structures"

(Link)

Author: John C. Reynolds (Carnegie Mellon University)

Reference: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55-74, doi: 10.1109/LICS.2002.1029817.

Why this paper? Cited by On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs, Compositional Verification of Interacting Systems Using Event Monads, and Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq.

How can we be sure that the programs we write do what they’re supposed to? An answer from the late 1960s is Hoare logic, which gives a formal relationship between programs and specifications. Crucially, Hoare logic can be used in a modular way, in the sense that parts of the program can be reasoned about separately, rather than demanding that an entire program must be reasoned about all at once – a completely impossible task even for some relatively small programs.

Traditional Hoare logic becomes unusable in the face of languages (for example, C) that allow the direct manipulation of memory within the code. Because there is nothing to stop two different program variables pointing to the same physical piece of memory, a manipulation that only seems to effect one variable may also effect another, even if that variable exists in some long distant piece of code. However, the direct manipulation of memory (and potential for ‘sharing’ that this creates) can be extremely useful, as can be seen in various examples in this paper by Reynolds. For example, we see a list reversal where instead of creating a new list that is a reversal of the input, we take the memory-saving approach of reversing by swapping values within the list.

This paper introduces the term separation logic, but mostly reports and summarises previous work by Reynolds and others (primarily Peter O’Hearn, Samin Ishtiaq, and Hongseok Yang, with inspiration from Rod Burstall and David Pym). The key innovation of this group is to change the logical language in which specifications can be stated. A separating conjunction ∗ joins the usual list of logical operators, with a proposition of form P ∗ Q holding if P and Q hold of entirely separate parts of memory. This allows modular reasoning to be restored via a frame rule that says that a true statement about a fragment of one’s code remains true if put in the context of other memory, so long as that extra memory remains separate from the fragment in question. Another connective called separating implication also joins the party, along with a constant stating that no memory is in use, and some syntax to allow one to talk about the content of memory. The paper goes on to present a treasure trove of examples, extensions, and directions for the future, with a heavy emphasis on the application of the logic to a variety of data structures and program constructs.