program-logic.tex 25.5 KB
 Ralf Jung committed Oct 06, 2016 1 2 \let\bar\overline Ralf Jung committed Oct 04, 2016 3 \section{Language} Ralf Jung committed Oct 06, 2016 4 \label{sec:language} Ralf Jung committed Oct 04, 2016 5 6 7 8 9 10 A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that \begin{itemize} \item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that \begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val} \end{mathpar} Ralf Jung committed Oct 06, 2016 11 12 13 \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\cup_n \textdom{Expr}^n)$ A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off. We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\ Ralf Jung committed Oct 04, 2016 14 15 16 17 18 19 \item All values are stuck: $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ \end{itemize} \begin{defn} An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if Ralf Jung committed Oct 06, 2016 20 $\Exists \expr_2, \state_2, \bar\expr. \expr,\state \step \expr_2,\state_2,\bar\expr$ Ralf Jung committed Oct 04, 2016 21 22 23 24 \end{defn} \begin{defn} An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value: Ralf Jung committed Oct 06, 2016 25 $\All\state_1, \expr_2, \state_2, \bar\expr. \expr, \state_1 \step \expr_2, \state_2, \bar\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2$ Ralf Jung committed Oct 04, 2016 26 27 28 29 30 31 32 33 \end{defn} \begin{defn}[Context] A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied: \begin{enumerate}[itemsep=0pt] \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ \item One can perform reductions below $\lctx$:\\ Ralf Jung committed Oct 06, 2016 34 $\All \expr_1, \state_1, \expr_2, \state_2, \bar\expr. \expr_1, \state_1 \step \expr_2,\state_2,\bar\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\bar\expr$ Ralf Jung committed Oct 04, 2016 35 \item Reductions stay below $\lctx$ until there is a value in the hole:\\ Ralf Jung committed Oct 06, 2016 36 $\All \expr_1', \state_1, \expr_2, \state_2, \bar\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\bar\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\bar\expr$ Ralf Jung committed Oct 04, 2016 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 \end{enumerate} \end{defn} \subsection{Concurrent language} For any language $\Lang$, we define the corresponding thread-pool semantics. \paragraph{Machine syntax} $\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n$ \judgment[Machine reduction]{\cfg{\tpool}{\state} \step \cfg{\tpool'}{\state'}} \begin{mathpar} \infer Ralf Jung committed Oct 06, 2016 53 {\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr} Ralf Jung committed Oct 04, 2016 54 {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step Ralf Jung committed Oct 06, 2016 55 \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \bar\expr}{\state_2}} Ralf Jung committed Oct 04, 2016 56 57 58 59 \end{mathpar} \clearpage \section{Program Logic} Ralf Jung committed Oct 06, 2016 60 \label{sec:program-logic} Ralf Jung committed Oct 04, 2016 61 Ralf Jung committed Oct 10, 2016 62 This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the logic described in \Sref{sec:dc-logic}. Ralf Jung committed Oct 06, 2016 63 So in the following, we assume that some language $\Lang$ was fixed. Ralf Jung committed Oct 06, 2016 64 65 \subsection{World Satisfaction, Invariants, View Shifts} Ralf Jung committed Oct 10, 2016 66 \label{sec:invariants} Ralf Jung committed Oct 06, 2016 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 To introduce invariants into our logic, we will define weakest precondition to explicitly thread through the proof that all the invariants are maintained throughout program execution. However, in order to be able to access invariants, we will also have to provide a way to \emph{temporarily disable} (or open'') them. To this end, we use tokens that manage which invariants are currently enabled. We assume to have the following four CMRAs available: \begin{align*} \textmon{State} \eqdef{}& \authm(\exm(\textdom{State})) \\ \textmon{Inv} \eqdef{}& \authm(\mathbb N \fpfn \agm(\latert \iPreProp)) \\ \textmon{En} \eqdef{}& \pset{\mathbb N} \\ \textmon{Dis} \eqdef{}& \finpset{\mathbb N} \end{align*} The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves. Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine. Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created. (We will discuss later how this assumption is discharged.) Ralf Jung committed Oct 06, 2016 85 \paragraph{World Satisfaction.} Ralf Jung committed Oct 06, 2016 86 87 We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained: \begin{align*} Ralf Jung committed Oct 10, 2016 88 W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \setComp{\iname \mapsto \aginj(\latertinj(\wIso(I(\iname))))}{\iname \in \dom(I)}} * \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right) Ralf Jung committed Oct 06, 2016 89 90 91 92 \end{align*} \paragraph{Invariants.} The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$: Ralf Jung committed Oct 10, 2016 93 $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag\set{\iname \mapsto \aginj(\latertinj(\wIso(\prop)))}}$ Ralf Jung committed Oct 06, 2016 94 Ralf Jung committed Oct 10, 2016 95 \paragraph{View Updates and View Shifts.} Ralf Jung committed Oct 06, 2016 96 Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants: Ralf Jung committed Oct 10, 2016 97 $\pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop)$ Ralf Jung committed Oct 06, 2016 98 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update. Ralf Jung committed Oct 10, 2016 99 100 101 102 103 104 105 106 107 108 109 We use $\top$ as symbol for the largest possible mask, $\mathbb N$. We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$. % View updates satisfy the following basic proof rules: \begin{mathpar} \infer[vup-mono] {\prop \proves \propB} {\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB} \infer[vup-intro-mask] {\mask_2 \subseteq \mask_1} Ralf Jung committed Oct 10, 2016 110 {\prop \proves \pvs[\mask_1][\mask_2]\pvs[\mask_2][\mask_1] \prop} Ralf Jung committed Oct 10, 2016 111 112 113 114 115 \infer[vup-trans] {} {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop} Ralf Jung committed Oct 10, 2016 116 117 118 \infer[vup-upd] {}{\upd\prop \proves \pvs[\mask] \prop} Ralf Jung committed Oct 10, 2016 119 \infer[vup-frame] Ralf Jung committed Oct 10, 2016 120 {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \propB * \prop} Ralf Jung committed Oct 10, 2016 121 122 123 124 125 126 127 128 \inferH{vup-update} {\melt \mupd \meltsB} {\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB} \infer[vup-timeless] {\timeless\prop} {\later\prop \proves \pvs[\mask] \prop} Ralf Jung committed Oct 10, 2016 129 130 131 132 133 134 135 136 137 138 % % \inferH{vup-allocI} % {\text{$\mask$ is infinite}} % {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop} %gov % \inferH{vup-openI} % {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop} % % \inferH{vup-closeI} % {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE} Ralf Jung committed Oct 10, 2016 139 \end{mathpar} Ralf Jung committed Oct 10, 2016 140 (There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:invariants}.) Ralf Jung committed Oct 06, 2016 141 142 143 144 145 146 We further define the notions of \emph{view shifts} and \emph{linear view shifts}: \begin{align*} \prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \Ra \pvs[\mask_1][\mask_2] \propB) \\ \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB \end{align*} Ralf Jung committed Oct 10, 2016 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 These two are useful when writing down specifications, but for reasoning, it is typically easier to just work directly with view updates. Still, just to give an idea of what view shifts are'', here are some proof rules for them: \begin{mathparpagebreakable} \inferH{vs-update} {\melt \mupd \meltsB} {\ownGhost\gname{\melt} \vs \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}} \and \inferH{vs-trans} {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC} {\prop \vs[\mask_1][\mask_3] \propC} \and \inferH{vs-imp} {\always{(\prop \Ra \propB)}} {\prop \vs[\emptyset] \propB} \and \inferH{vs-mask-frame} {\prop \vs[\mask_1][\mask_2] \propB} {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB} \and \inferH{vs-frame} {\prop \vs[\mask_1][\mask_2] \propB} {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC} \and \inferH{vs-timeless} {\timeless{\prop}} {\later \prop \vs \prop} Ralf Jung committed Oct 10, 2016 174 175 176 177 178 179 180 181 182 183 % \inferH{vs-allocI} % {\infinite(\mask)} % {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}} % \and % \axiomH{vs-openI} % {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} % \and % \axiomH{vs-closeI} % {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } % Ralf Jung committed Oct 10, 2016 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 \inferHB{vs-disj} {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC} {\prop \lor \propB \vs[\mask_1][\mask_2] \propC} \and \inferHB{vs-exist} {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} \and \inferHB{vs-always} {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC} {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} \and \inferH{vs-false} {} {\FALSE \vs[\mask_1][\mask_2] \prop } \end{mathparpagebreakable} \subsection{Weakest Precondition} Ralf Jung committed Oct 06, 2016 202 203 Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived. Ralf Jung committed Oct 10, 2016 204 205 \paragraph{Defining weakest precondition.} Ralf Jung committed Oct 06, 2016 206 207 208 We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$). \begin{align*} Ralf Jung committed Oct 06, 2016 209 210 211 \textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\ & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\ & \Bigl(\toval(\expr) = \bot \land \All \state. \ownGhost{\gname_{\textmon{State}}}{\authfull \state} \vsW[\mask][\emptyset] {}\\ Ralf Jung committed Oct 06, 2016 212 &\qquad \red(\expr, \state) * \later\All \expr', \state', \bar\expr. (\expr, \state \step \expr', \state', \bar\expr) \vsW[\emptyset][\mask] {}\\ Ralf Jung committed Oct 06, 2016 213 &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \state'} * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \bar\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\ Ralf Jung committed Oct 06, 2016 214 % (* value case *) Ralf Jung committed Oct 06, 2016 215 \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\mask, \expr, \Lam\val.\prop) Ralf Jung committed Oct 06, 2016 216 \end{align*} Ralf Jung committed Oct 06, 2016 217 If we leave away the mask, we assume it to default to $\top$. Ralf Jung committed Oct 06, 2016 218 Ralf Jung committed Oct 06, 2016 219 220 221 222 This ties the authoritative part of \textmon{State} to the actual physical state of the reduction witnessed by the weakest precondition. The fragment will then be available to the user of the logic, as their way of talking about the physical state: $\ownPhys\state \eqdef \ownGhost{\gname_{\textmon{State}}}{\authfrag \state}$ Ralf Jung committed Oct 10, 2016 223 224 \paragraph{Laws of weakest precondition.} The following rules can all be derived inside the DC logic: Ralf Jung committed Oct 04, 2016 225 226 227 228 229 \begin{mathpar} \infer[wp-value] {}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}} \infer[wp-mono] Ralf Jung committed Oct 10, 2016 230 231 {\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB} {\vctx\mid\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}} Ralf Jung committed Oct 04, 2016 232 233 234 235 236 237 238 239 \infer[pvs-wp] {}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}} \infer[wp-pvs] {}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}} \infer[wp-atomic] Ralf Jung committed Oct 10, 2016 240 {\physatomic{\expr}} Ralf Jung committed Oct 04, 2016 241 242 243 244 245 246 247 248 {\pvs[\mask_1][\mask_2] \wpre\expr[\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop} \proves \wpre\expr[\mask_1]{\Ret\var.\prop}} \infer[wp-frame] {}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}} \infer[wp-frame-step] {\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1} Ralf Jung committed Oct 10, 2016 249 {\wpre\expr[\mask_2]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask_1]{\Ret\var.\propB*\prop}} Ralf Jung committed Oct 04, 2016 250 251 252 253 254 255 \infer[wp-bind] {\text{$\lctx$ is a context}} {\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}} \end{mathpar} Ralf Jung committed Oct 10, 2016 256 257 We will also want rules that connect weakest preconditions to the operational semantics of the language. In order to cover the most general case, those rules end up being more complicated: Ralf Jung committed Oct 04, 2016 258 259 \begin{mathpar} \infer[wp-lift-step] Ralf Jung committed Oct 10, 2016 260 {\toval(\expr_1) = \bot} Ralf Jung committed Oct 04, 2016 261 { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below... Ralf Jung committed Oct 10, 2016 262 ~~\pvs[\mask][\emptyset] \Exists \state_1. \red(\expr_1,\state_1) * \later\ownPhys{\state_1} * {}\\\qquad~~ \later\All \expr_2, \state_2, \bar\expr. \Bigl( (\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr) * \ownPhys{\state_2} \Bigr) \wand \pvs[\emptyset][\mask] \Bigl(\wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop} Ralf Jung committed Oct 04, 2016 263 264 265 266 267 \end{inbox}} } \\\\ \infer[wp-lift-pure-step] {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \and Ralf Jung committed Oct 10, 2016 268 269 \All \state_1, \expr_2, \state_2, \bar\expr. \expr_1,\state_1 \step \expr_2,\state_2,\bar\expr \Ra \state_1 = \state_2 } {\later\All \state, \expr_2, \bar\expr. (\expr_1,\state \step \expr_2, \state,\bar\expr) \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}} Ralf Jung committed Oct 04, 2016 270 271 \end{mathpar} Ralf Jung committed Oct 10, 2016 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 We can further derive some slightly simpler rules for special cases: We can derive some specialized forms of the lifting axioms for the operational semantics. \begin{mathparpagebreakable} \infer[wp-lift-atomic-step] {\atomic(\expr_1) \and \red(\expr_1, \state_1)} { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \bar\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\bar\expr) * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} \end{inbox}} } \infer[wp-lift-atomic-det-step] {\atomic(\expr_1) \and \red(\expr_1, \state_1) \and \All \expr'_2, \state'_2, \bar\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\bar\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \bar\expr = \bar\expr'} {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \infer[wp-lift-pure-det-step] {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \\ \All \state_1, \expr_2', \state'_2, \bar\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\bar\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \bar\expr = \bar\expr'} {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \end{mathparpagebreakable} Ralf Jung committed Oct 10, 2016 293 294 Ralf Jung committed Oct 10, 2016 295 \paragraph{Adequacy of weakest precondition.} Ralf Jung committed Oct 04, 2016 296 297 298 299 300 The adequacy statement concerning functional correctness reads as follows: \begin{align*} &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra Ralf Jung committed Oct 06, 2016 301 \\&( \ownPhys\state * \ownM\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra Ralf Jung committed Oct 04, 2016 302 303 304 305 306 \\&\cfg{\state}{[\expr]} \step^\ast \cfg{\state'}{[\val] \dplus \tpool'} \Ra \\&\pred(\val) \end{align*} where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants. Ralf Jung committed Oct 10, 2016 307 \ralf{TODO: We can't just embed meta-level predicates like this. After all, this is a deep embedding.} Ralf Jung committed Oct 04, 2016 308 309 310 311 312 Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further. \begin{align*} &\All \mask, \expr, \state, \melt, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra Ralf Jung committed Oct 06, 2016 313 \\&( \ownPhys\state * \ownM\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra Ralf Jung committed Oct 04, 2016 314 315 316 317 318 319 \\&\cfg{\state}{[\expr]} \step^\ast \cfg{\state'}{\tpool'} \Ra \\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state') \end{align*} Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step. Ralf Jung committed Oct 10, 2016 320 321 322 323 324 325 \paragraph{Hoare triples.} It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq. Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple: $\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}$ Ralf Jung committed Oct 04, 2016 326 Ralf Jung committed Oct 10, 2016 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 We only give some of the proof rules for Hoare triples here, since we usually do all our reasoning directly with weakest preconditions and use Hoare triples only to write specifications. \begin{mathparpagebreakable} \inferH{Ht-ret} {} {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]} \and \inferH{Ht-bind} {\text{$\lctx$ is a context} \and \hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\ \All \val. \hoare{\propB}{\lctx(\val)}{\Ret\valB.\propC}[\mask]} {\hoare{\prop}{\lctx(\expr)}{\Ret\valB.\propC}[\mask]} \and \inferH{Ht-csq} {\prop \vs \prop' \\ \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ \All \val. \propB' \vs \propB} {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} \and % \inferH{Ht-mask-weaken} % {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} % {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask \uplus \mask']} % \\\\ \inferH{Ht-frame} {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]} \and % \inferH{Ht-frame-step} % {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3} % {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]} % \and \inferH{Ht-atomic} {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\ \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\ \physatomic{\expr} } {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']} \and \inferH{Ht-false} {} {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} \and \inferHB{Ht-disj} {\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]} {\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]} \and \inferHB{Ht-exist} {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]} \and \inferHB{Ht-box} {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]} {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]} % \and % \inferH{Ht-inv} % {\hoare{\later\propC*\prop}{\expr}{\Ret\val.\later\propC*\propB}[\mask] \and % \physatomic{\expr} % } % {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]} % \and % \inferH{Ht-inv-timeless} % {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and % \physatomic{\expr} \and \timeless\propC % } % {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]} \end{mathparpagebreakable} Ralf Jung committed Oct 04, 2016 392 Ralf Jung committed Oct 10, 2016 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 \subsection{Invariant Namespaces} \label{sec:namespaces} In \Sref{sec:invariants}, we defined an assertion $\knowInv\iname\prop$ expressing knowledge (\ie the assertion is persistent) that $\prop$ is maintained as invariant with name $\iname$. The concrete name $\iname$ is picked when the invariant is allocated, so it cannot possibly be statically known -- it will always be a variable that's threaded through everything. However, we hardly care about the actual, concrete name. All we need to know is that this name is \emph{different} from the names of other invariants that we want to open at the same time. Keeping track of the $n^2$ mutual inequalities that arise with $n$ invariants quickly gets in the way of the actual proof. To solve this issue, instead of remembering the exact name picked for an invariant, we will keep track of the \emph{namespace} the invariant was allocated in. Namesapces are sets of invariants, following a tree-like structure: Think of the name of an invariant as a sequence of identifiers, much like a fully qualified Java class name. A \emph{namespace} $\namesp$ then is like a Java package: it is a sequence of identifiers that we think of as \emph{containing} all invariant names that begin with this sequence. For example, \texttt{org.mpi-sws.iris} is a namespace containing the invariant name \texttt{org.mpi-sws.iris.heap}. The crux is that all namespaces contain infinitely many invariants, and hence we can \emph{freely pick} the namespace an invariant is allocated in -- no further, unpredictable choice has to be made. Furthermore, we will often know that namespaces are \emph{disjoint} just by looking at them. The namespaces $\namesp.\texttt{iris}$ and $\namesp.\texttt{gps}$ are disjoint no matter the choice of $\namesp$. As a result, there is often no need to track disjointness of namespaces, we just have to pick the namespaces that we allocate our invariants in accordingly. Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \textlog{list}(\mathbb N)$ be the type of \emph{invariant namespaces}. We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$. (In other words, the list is backwards''. This is because cons-ing to the list, like the dot does above, is easier to deal with in Coq than appending at the end.) The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name). They, too, are lists of $\mathbb N$, the same type as namespaces. In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\mathbb N$, the type of plain'' invariant names. Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\textlog{list}(\mathbb N)$ is countable. Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: $\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}$ We will overload the notation for invariant assertions for using namespaces instead of names: $\knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop}$ We can now derive the following rules (this involves unfolding the definition of view updates): \begin{mathpar} \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop} Ralf Jung committed Oct 04, 2016 427 Ralf Jung committed Oct 10, 2016 428 \axiomH{inv-alloc}{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop} Ralf Jung committed Oct 04, 2016 429 Ralf Jung committed Oct 10, 2016 430 431 432 \inferH{inv-open} {\namesp \subseteq \mask} {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} Ralf Jung committed Oct 04, 2016 433 Ralf Jung committed Oct 10, 2016 434 435 436 437 \inferH{inv-open-timeless} {\namesp \subseteq \mask \and \timeless\prop} {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \prop * (\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} \end{mathpar} Ralf Jung committed Oct 04, 2016 438 Ralf Jung committed Oct 10, 2016 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 \subsection{Accessors} The two rules \ruleref{inv-open} and \ruleref{inv-open-timeless} above may look a little surprising, in the sense that it is not clear on first sight how they would be applied. The rules are the first \emph{accessors} that show up in this document. Accessors are assertions of the form $\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC)$ One way to think about such assertions is as follows: Given some accessor, if during our verification we have the assertion $\prop$ and the mask $\mask_1$ available, we can use the accessor to \emph{access} $\propB$ and obtain the witness $\var$. We call this \emph{opening} the accessor, and it changes the mask to $\mask_2$. Additionally, opening the accessor provides us with $\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC$, a \emph{linear view shift} (\ie a view shift that can only be used once). This linear view shift tells us that in order to \emph{close} the accessor again and go back to mask $\mask_1$, we have to pick some $\varB$ and establish the corresponding $\propB'$. After closing, we will obtain $\propC$. Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the correspond proof rules for view updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any \emph{atomic} expression. Furthermore, in the special case that $\mask_1 = \mask_2$, the accessor can be opened around \emph{any} expression. For this reason, we also call such accessors \emph{non-atomic}. The reasons accessors are useful is that they let us talk about opening X'' (\eg opening invariants'') without having to care what X is opened around. Furthermore, as we construct more sophisticated and more interesting things that can be opened (\eg invariants that can be cancelled'', or STSs), accessors become a useful interface that allows us to mix and match different abstractions in arbitrary ways. \ralf{This would be much more convincing if we had forward references here to sections describing canellable invariants and STSs.} Ralf Jung committed Oct 04, 2016 460 461 462 463 464 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: