From 3ddafb3b3aebf3efd872f572627404a46f6fbed3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 19 Apr 2016 22:51:56 -0400 Subject: [PATCH] SeparationLogic chapter: program logic --- frap_book.tex | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/frap_book.tex b/frap_book.tex index be5405f..a00b86c 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -3259,6 +3259,88 @@ $$\ptsto{r}{0} \Rightarrow \; \ptsto{r}{?c}$$ Now we can finish the proof by reflexivity of $\Rightarrow$, learning $?c = 0$. +\section{Program Logic} + +We use our automatic cancellation procedure to discharge some of the premises from the rules of the program logic, which we present now. +First, here are the rules that are (almost) exactly the same as from last chapter. + +$$\infer{\hoare{P}{\mt{Return} \; v}{\lambda r. \; P * \lift{r = v}}}{} +\quad \infer{\hoare{P}{x \leftarrow c_1; c_2(x)}{R}}{ + \hoare{P}{c_1}{Q} + & (\forall r. \; \hoare{Q(r)}{c_2(r)}{R}) +}$$ + +$$\infer{\hoare{I(\mt{Again}(i))}{\mt{Loop} \; i \; f}{\lambda r. \; I(\mt{Done}(r))}}{ + \forall a. \; \hoare{I(\mt{Again}(a))}{f(a)}{I} +} +\quad \infer{\hoare{\lift{\bot}}{\mt{Fail}}{\lambda \_. \; \lift{\bot}}}{}$$ + +$$\infer{\hoare{P'}{c}{Q'}}{ + \hoare{P}{c}{Q} + & P' \Rightarrow P + & \forall r. \; Q(r) \Rightarrow Q'(r) +}$$ + +More interesting are the rules for primitive memory operations. +First, we have the rule for $\mt{Read}$. + +$$\infer{\hoare{\exists v. \; \ptsto{a}{v} * R(v)}{\mt{Read} \; a}{\lambda r. \; \ptsto{a}{r} * R(r)}}{}$$ + +In words: before reading from address $a$, it must be the case that $a$ points to some value $v$, and predicate $R(v)$ records what else we know about the memory at that point. +Afterward, we know that $a$ points to the result $r$ of the read operation, and $R$ is still present. +We call $R$ a \emph{frame predicate}\emph{frame predicate}, recording what we know about parts of memory that the command does not touch directly. +We might also say that the \emph{footprint} of this command is the singleton set $\{a\}$. +In general, frame predicates record preserved facts about addresses outside a command's footprint. +The next few rules don't have frame predicates baked in; we finish with a rule that adds them back, in a generic way for arbitrary Hoare triples. + +$$\infer{\hoare{\exists v. \; \ptsto{a}{v}}{\mt{Write} \; a \; v'}{\lambda \_. \; \ptsto{a}{v'}}}{}$$ + +This last rule, for $\mt{Write}$, is even simpler, with no baked-in frame predicate. +We see a straightforward illustration of overwriting $a$'s old value $v$ with the new value $v$'. + +$$\infer{\hoare{\emp}{\mt{Alloc} \; n}{\lambda r. \; \ptsto{r}{0^n}}}{} +\quad \infer{\hoare{\ptsto{a}{\; ?^n}}{\mt{Free} \; a \; n}{\lambda \_. \; \emp}}{}$$ + +The rules for allocation and deallocation deploy a few notations that we don't explain in detail here, with $0^n$ for sequences of $n$ zeroes and $?^n$ for sequences of $n$ arbitrary values. + +The next rule, the \emph{frame rule}\index{frame rule}, gives the second key idea of separation logic, supporting the \emph{small-footprint}\index{small-footprint style} reasoning style. + +$$\infer{\hoare{P * R}{c}{\lambda r. \; Q(r) * R}}{ + \hoare{P}{c}{Q} +}$$ + +In other words, any Hoare triple can be extended by conjoining an arbitrary predicate $R$ in both precondition and postcondition. +Even more intuitively, when a program satisfies a spec, it also satisfies an extended spec that records the state of some other part of memory that is untouched (i.e., is outside the command's footprint). + +For the pragmatics of proving particular programs, we defer to the accompanying Coq code. +\modularity +However, for modular proofs, the frame rule has such an important role that we want to emphasize it here. +It is possible to define (recursively) a predicate $\mt{llist}(\ell, p)$, capturing the idea that the memory contains exactly an imperative linked list, rooted at pointer $p$, representing functional linked list $\ell$. +We can also prove a general specification for a list-reversal function: +$$\forall \ell, p. \; \hoare{\mt{llist}(\ell, p)}{\texttt{reverse}(p)}{\lambda r. \; \mt{llist}(\mt{rev}(\ell), r)}$$ + +Now consider that we have the roots $p_1$ and $p_2$ of two disjoint lists, respectively representing $\ell_1$ and $\ell_2$. +It is easy to instantiate the general theorem and get $\hoare{\mt{llist}(\ell_1, p_1)}{\texttt{reverse}(p_1)}{\lambda r. \; \mt{llist}(\mt{rev}(\ell_1), r)}$ and $\hoare{\mt{llist}(\ell_2, p_2)}{\texttt{reverse}(p_2)}{\lambda r. \; \mt{llist}(\mt{rev}(\ell_2), r)}$. +Applying the frame rule to the former theorem, with $R = \mt{llist}(\ell_2, p_2)$, we get: +$$\hoare{\mt{llist}(\ell_1, p_1) * \mt{llist}(\ell_2, p_2)}{\texttt{reverse}(p_1)}{\lambda r. \; \mt{llist}(\mt{rev}(\ell_1), r) * \mt{llist}(\ell_2, p_2)}$$ +Similarly, applying the frame rule to the latter, with $R = \mt{llist}(\mt{rev}(\ell_1), r)$, we get: +$$\hoare{\mt{llist}(\ell_2, p_2) * \mt{llist}(\mt{rev}(\ell_1), r)}{\texttt{reverse}(p_2)}{\lambda r'. \; \mt{llist}(\mt{rev}(\ell_2), r') * \mt{llist}(\mt{rev}(\ell_1), r)}$$ +Now it is routine to derive the following spec for a larger program: +$$\begin{array}{l} + \{\mt{llist}(\ell_1, p_1) * \mt{llist}(\ell_2, p_2)\} \\ + \hspace{.2in} r \leftarrow \texttt{reverse}(p_1); r' \leftarrow \texttt{reverse}(p_2); \; \mt{Return}(r, r') \\ + \{\lambda (r, r'). \; \mt{llist}(\mt{rev}(\ell_1), r) * \mt{llist}(\mt{rev}(\ell_2), r')\} +\end{array}$$ + +Note that this specification would be incorrect if the two input lists could share any memory cells! +The separating conjunction $*$ in the precondition implicitly formalizes our expectiation of nonaliasing. +The proof internals require only the basic rules for $\mt{Return}$ and sequencing, in addition to the rule of consequence, whose side conditions we discharge using the cancellation approach sketched in the previous section. + +Note also that this highly automatable proof style works just as well when calling functions associated with several different data structures in memory. +The frame rule provides a way to show that any function, in any library, preserves arbitrary memory state outside its footprint. + + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%