18
$\begingroup$

A frame rule, like the one given below, captures the idea that, given a program c with precondition p that holds before it runs and postcondition q that holds afterward, some disjoint condition r should hold both before and after c runs. (The * connective requires that its arguments be disjoint.) Often, the pre- and postconditions are states of a heap, and c is an effectful program that modifies the heap in some way.

    {p} c {q}
----------------- (where no free variable in r is modified by c)
{p * r} c {q * r}

Discussions of the frame rule that I've seen always seem to focus on how the disjoint part of the heap, r, is preserved. This enables "local reasoning": when reasoning about the effect that c has, we can disregard the r part of the heap and only concern ourselves with the part that actually changes. But another way to look at it is that the change from p to q is preserved, even though r is now sitting there. In other words, it's important that we end up with the postcondition {q * r}, rather than {q' * r} for some other q'.

So, my question is whether there's any treatment of the frame rule that discusses or makes use of the preservation-of-change-from-p-to-q thing.

$\endgroup$
  • $\begingroup$ One answer to my own question is in this paper: software.imdea.org/~gotsman/papers/interproc-sas06.pdf, in the sentence (emphasis mine) "If P ensures C’s footprint is allocated, then according to Frame, executing C in the presence of additional memory R results in the same behavior, and C does not touch the extra memory." It's that "results in the same behavior" that I was looking for someone to point out, in addition to just "C does not touch the extra memory". (Thanks to @kaosjester for the link.) $\endgroup$ – Lindsey Kuper Oct 11 '12 at 1:44
  • 1
    $\begingroup$ If you read through the soundness proofs of the frame rule and other rules of Separation Logic, you will discover that they are doing exactly what you are after, i.e., they talk about how the change from $p$ to $q$ is preserved. Do pay attention to the locality and frame properties mentioned there. $\endgroup$ – Uday Reddy Oct 12 '12 at 13:21
11
$\begingroup$

But this no-change-to-q property does not actually hold!

Consider {emp} x := alloc(0) {x |-> 0}. Now, if I frame in y |-> 3, I get

{y |-> 3} x := alloc(0) {x |-> 0 * y |-> 3}

but, by the rule of consequence, I could change the postcondition to

{y |-> 3} x := alloc(0) {(x |-> 0 /\ x != y) * y |-> 3}

To make this more concrete, suppose y is the number 37. When I run the allocation command in a completely empty heap, it's possible that I will end up allocating address 37, so that x = 37. But, if I instead start with a heap containing a single cell at address y = 37, this outcome is no longer possible! Adding a frame to the precondition has pruned some of the nondeterminism in the postcondition.

The paper "Local action and abstract separation logic" (Calcagno, O'Hearn, and Yang) is all about understanding the frame rule from a deeper, semantic perspective. The key definition of the paper is locality for "actions", where an action is (the semantic representation of) a program. Locality says that when you add in some frame heap, the only way that the original postcondition can be changed is by pruning some nondeterminism as above. And, in fact, pruning only arises because of allocation.

$\endgroup$
  • $\begingroup$ Thanks for the example and for the reference! Your example makes sense. Is it fair to say, though, that q can only change to "q, and also..."? And, furthermore, if allocation is the only thing that can prune the nondeterminism in the postcondition (which is a cool result in itself), then, if there's some part of the postcondition that is location-independent, then is that part of the postcondition guaranteed to stay the same? Can we say that the postcondition stays the same up to alpha-renaming of locations? (I have an example in mind, but maybe this is better explained via email.) $\endgroup$ – Lindsey Kuper Oct 11 '12 at 4:12
  • 1
    $\begingroup$ Yes, q can only change to "q, and also..." In other words, the postcondition can only become stronger: it will imply the original postcondition. This is part of the definition of locality for actions. It is not true, though, that the change to the postcondition is only tied to renaming. In the example I gave, the extra fact that x and y are distinct is true regardless of the particular address chosen for y. The example captures the freshness of allocation, which is invariant under renaming. $\endgroup$ – Aaron Turon Oct 11 '12 at 15:09
11
$\begingroup$

First, there's a small misconception in the statement of your question, which is what Aaron was also getting at in his answer. Predicates in separation logic are sets of heaps (or equivalently, predicates on heaps), and the separating conjunction $P \ast Q$ is defined as:

$$ P \ast R \triangleq \{h_1 \cdot h_2 \;|\; h_1 \in P \;\wedge\; h_2 \in R \;\wedge\; \mathrm{dom}(h_1) \cap \mathrm{dom}(h_2) = \emptyset\} $$

So in the frame rule

$$ \frac{\{P\}c\{Q\}}{\{P\ast R\}c\{Q \ast R\}} $$

$R$ (and $P$ and $Q$) are not talking about specific heaps --- they are properties of heaps (since subsets and predicates are equivalent). The best way to understand what's going is by looking at the definition of what it means for a Hoare triple to hold:

$$ \{P\}c\{Q\} \triangleq \forall h_1 \in P.\; \forall h' \in \mathrm{Heap}\;\mbox{s.t.}\; h' \# h_1.\;\exists h_2 \in Q.\; \left<h_1\cdot h'; c\right> \mapsto^\ast \left<h_2\cdot h'; \mathsf{skip}\right> $$

This definition basically says that (1) if you run $c$ with any $h_1$ in $P$, then you'll finish in some final state $h_2$ in $Q$, and (2) if you add on any extra memory $h'$, that memory will be unchanged at the end of the run. But note that the specific $h_2$ you get can differ, for different choices of $h'$ --- what's being guaranteed is that the properties $P$ and $Q$ will continue to hold under extension, not that you get exactly the same result heap.

It's not too hard, but still worth working out, to see how this definition of Hoare triple implies that the frame rule holds. As you note, this is a kind of "preservation-of-changes" property, and it has a particularly vivid expression in the statement of the parallel composition rule in concurrent separation logic:

$$ \frac{\{P_1\}c_1\{Q_1\} \qquad \{P_2\}c_2\{Q_2\}}{\{P_1 \ast P_2\}c_1 || c_2 \{Q_1 \ast Q_2\}} $$

If $c_1$ and $c_2$ act on disjoint regions of memory, then each will not interfere with the properties of the other one's execution when they are run in parallel.

There's a discussion of this in the paper by Hoare et al, On Locality and the Exchange Law for Concurrent Processes, where they show how to give a merged algebra of programs and assertions.

$\endgroup$
  • $\begingroup$ The definition for Hoare triples looks wrong: It should say the execution doesn't fault, it should allow for non-termination, it probably shouldn't preclude models that don't have safety monotonicity. (But, yes, I do agree it's perfectly reasonable to talk about "preservation-of-changes" for the reasons you explain.) $\endgroup$ – Radu GRIGore Oct 11 '12 at 10:08
  • 3
    $\begingroup$ (1) I gave the semantics for total correctness triples, and so it asserts that the command completes safely -- I find that total correctness makes explaining the forall/exists character of pre and post-conditions easier to see. (2) This semantics of triples was actually invented (IIRC by Birkedal and Yang) to handle languages that don't have safety monotonicity in the language semantics, by building it into the meaning of triples. As a result, you can have non-monotonic constructs (e.g., queries about how big the heap is) in the language, while still having the frame rule for the Hoare logic. $\endgroup$ – Neel Krishnaswami Oct 11 '12 at 10:46
  • $\begingroup$ (1) OK, but those triples are written differently. (2) I didn't know that. To rephrase what you said: without monotonicity you could lose the frame rule and keep using Hoare triples as usual, which is what I was getting at in the first comment, but you could also strengthen the definition of a triple so that you get back the frame rule. (3) I don't see why it precludes faults. Do you assume $c$ is deterministic? $\endgroup$ – Radu GRIGore Oct 11 '12 at 11:05
  • 1
    $\begingroup$ Thanks, Neel! You're right, I was conflating the properties P and Q with specific heaps. So, to sum up your comment: Q is preserved, but the particular heap that you get at the end could be a different Q-satisfying heap than you were getting before. Yes? $\endgroup$ – Lindsey Kuper Oct 11 '12 at 17:13
  • 1
    $\begingroup$ @RaduGRIGore: yes, I was assuming that the language was deterministic, and this assumption will fail when we add concurrency. Nice catch! $\endgroup$ – Neel Krishnaswami Oct 12 '12 at 14:25
2
$\begingroup$

While not 100% related, this has the flavor of contract idempotence.

If we think of {p} as a pre-condition on c and {q} as a post-condition on c, this idea of a frame rule would ensure that the pre- and post-conditions hold in every context of computation, not the simple case where nothing else exists.

That said, I cannot say that I've seen such a frame rule presented in any of the dozens of contract papers I have read. It's certainly a great idea, though, and requiring such a change may do a lot toward developing a reasonable, tangible understanding of idempotent contracts.

$\endgroup$
  • $\begingroup$ Thanks for the comment. Hm, interesting -- I wonder if anyone else reading this knows of contract papers that state frame properties. $\endgroup$ – Lindsey Kuper Oct 11 '12 at 2:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.