program-logic.tex 25.5 KB
 Ralf Jung committed Oct 06, 2016 1 Ralf Jung committed Oct 04, 2016 2 \section{Program Logic} Ralf Jung committed Oct 06, 2016 3 \label{sec:program-logic} Ralf Jung committed Oct 04, 2016 4 Ralf Jung committed Oct 22, 2016 5 This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic. Ralf Jung committed Oct 06, 2016 6 So in the following, we assume that some language $\Lang$ was fixed. Ralf Jung committed Dec 11, 2017 7 Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composeable-resources}. Ralf Jung committed Oct 22, 2016 8 9 Ralf Jung committed Dec 10, 2017 10 \subsection{World Satisfaction, Invariants, Fancy Updates} Ralf Jung committed Oct 10, 2016 11 \label{sec:invariants} Ralf Jung committed Oct 06, 2016 12 13 14 15 16 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. Robbert Krebbers committed Dec 10, 2017 17 We assume to have the following four cameras available: Ralf Jung committed Oct 06, 2016 18 \begin{align*} Ralf Jung committed Dec 07, 2016 19 20 21 \InvName \eqdef{}& \nat \\ \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\ \textmon{En} \eqdef{}& \pset{\InvName} \\ Ralf Jung committed Dec 12, 2016 22 \textmon{Dis} \eqdef{}& \finpset{\InvName} Ralf Jung committed Oct 06, 2016 23 24 25 \end{align*} The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves. Robbert Krebbers committed Dec 10, 2017 26 We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these cameras have been created, such that these names are globally known. Ralf Jung committed Oct 06, 2016 27 Ralf Jung committed Oct 06, 2016 28 \paragraph{World Satisfaction.} Robbert Krebbers committed Dec 10, 2017 29 We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained: Ralf Jung committed Oct 06, 2016 30 \begin{align*} Ralf Jung committed Dec 07, 2016 31 W \eqdef{}& \Exists I : \InvName \fpfn \Prop. Ralf Jung committed Oct 31, 2016 32 \begin{array}[t]{@{} l} Robbert Krebbers committed Oct 17, 2016 33 \ownGhost{\gname_{\textmon{Inv}}}{\authfull Ralf Jung committed Oct 31, 2016 34 \mapComp {\iname} Robbert Krebbers committed Oct 17, 2016 35 36 37 38 {\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) \end{array} Ralf Jung committed Oct 06, 2016 39 40 41 \end{align*} \paragraph{Invariants.} Robbert Krebbers committed Dec 10, 2017 42 The following proposition states that an invariant with name $\iname$ exists and maintains proposition $\prop$: Robbert Krebbers committed Oct 17, 2016 43 44 $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}} {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}}$ Ralf Jung committed Oct 06, 2016 45 Ralf Jung committed Dec 10, 2017 46 \paragraph{Fancy Updates and View Shifts.} Ralf Jung committed Oct 21, 2016 47 Next, we define \emph{fancy updates}, which are essentially the same as the basic 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 48 $\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 49 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. Robbert Krebbers committed Oct 17, 2016 50 We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$. Ralf Jung committed Oct 10, 2016 51 52 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$. % Ralf Jung committed Oct 21, 2016 53 Fancy updates satisfy the following basic proof rules: Ralf Jung committed Oct 31, 2016 54 \begin{mathparpagebreakable} Ralf Jung committed Oct 21, 2016 55 \infer[fup-mono] Ralf Jung committed Oct 10, 2016 56 57 58 {\prop \proves \propB} {\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB} Ralf Jung committed Oct 21, 2016 59 \infer[fup-intro-mask] Ralf Jung committed Oct 10, 2016 60 {\mask_2 \subseteq \mask_1} Ralf Jung committed Oct 10, 2016 61 {\prop \proves \pvs[\mask_1][\mask_2]\pvs[\mask_2][\mask_1] \prop} Ralf Jung committed Oct 10, 2016 62 Ralf Jung committed Oct 21, 2016 63 \infer[fup-trans] Ralf Jung committed Oct 10, 2016 64 65 66 {} {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop} Ralf Jung committed Oct 21, 2016 67 \infer[fup-upd] Ralf Jung committed Oct 10, 2016 68 69 {}{\upd\prop \proves \pvs[\mask] \prop} Ralf Jung committed Oct 21, 2016 70 \infer[fup-frame] Ralf Jung committed Oct 10, 2016 71 {}{\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 72 Ralf Jung committed Oct 21, 2016 73 \inferH{fup-update} Ralf Jung committed Oct 10, 2016 74 75 76 {\melt \mupd \meltsB} {\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB} Ralf Jung committed Oct 21, 2016 77 \infer[fup-timeless] Ralf Jung committed Oct 10, 2016 78 79 {\timeless\prop} {\later\prop \proves \pvs[\mask] \prop} Ralf Jung committed Oct 10, 2016 80 % Ralf Jung committed Oct 21, 2016 81 % \inferH{fup-allocI} Ralf Jung committed Oct 10, 2016 82 83 84 % {\text{$\mask$ is infinite}} % {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop} %gov Ralf Jung committed Oct 21, 2016 85 % \inferH{fup-openI} Ralf Jung committed Oct 10, 2016 86 87 % {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop} % Ralf Jung committed Oct 21, 2016 88 % \inferH{fup-closeI} Ralf Jung committed Oct 10, 2016 89 % {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE} Ralf Jung committed Oct 31, 2016 90 \end{mathparpagebreakable} Ralf Jung committed Dec 05, 2016 91 (There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.) Ralf Jung committed Oct 06, 2016 92 Ralf Jung committed Oct 21, 2016 93 We can further define the notions of \emph{view shifts} and \emph{linear view shifts}: Ralf Jung committed Oct 06, 2016 94 \begin{align*} Ralf Jung committed Oct 21, 2016 95 \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB \\ Ralf Jung committed Feb 02, 2017 96 97 \prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \wand \pvs[\mask_1][\mask_2] \propB) \\ \prop \vs[\mask] \propB \eqdef{}& \prop \vs[\mask][\mask] \propB Ralf Jung committed Oct 06, 2016 98 \end{align*} Ralf Jung committed Oct 21, 2016 99 These two are useful when writing down specifications and for comparing with previous versions of Iris, but for reasoning, it is typically easier to just work directly with fancy updates. Ralf Jung committed Oct 10, 2016 100 101 102 103 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} Ralf Jung committed Feb 02, 2017 104 {\ownGhost\gname{\melt} \vs[\emptyset] \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}} Ralf Jung committed Oct 10, 2016 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 \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}} Ralf Jung committed Feb 02, 2017 124 {\later \prop \vs[\emptyset] \prop} Ralf Jung committed Oct 10, 2016 125 Ralf Jung committed Oct 10, 2016 126 127 128 129 130 131 132 133 134 135 % \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 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 \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} Ralf Jung committed Dec 10, 2017 153 \subsection{Weakest Precondition} Ralf Jung committed Oct 06, 2016 154 Robbert Krebbers committed Dec 10, 2017 155 Finally, we can define the core piece of the program logic, the proposition that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived. Ralf Jung committed Oct 10, 2016 156 157 \paragraph{Defining weakest precondition.} Ralf Jung committed Oct 06, 2016 158 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$). Robbert Krebbers committed Dec 10, 2017 159 We further assume (as a parameter) a predicate $\stateinterp : \State \to \iProp$ that interprets the physical state as an Iris proposition. Ralf Jung committed Dec 12, 2016 160 This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs. Ralf Jung committed Dec 12, 2017 161 Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck. Ralf Jung committed Oct 06, 2016 162 163 \begin{align*} Ralf Jung committed Dec 13, 2017 164 \textdom{wp}(\stateinterp, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\ Joseph Tassarotti committed Nov 14, 2017 165 & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\ Robbert Krebbers committed Dec 10, 2017 166 & \Bigl(\toval(\expr) = \bot \land \All \state. \stateinterp(\state) \vsW[\mask][\emptyset] {}\\ Ralf Jung committed Dec 12, 2017 167 &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\ Ralf Jung committed Dec 13, 2017 168 &\qquad\qquad \stateinterp(\state') * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\ Ralf Jung committed Oct 06, 2016 169 % (* value case *) Ralf Jung committed Dec 13, 2017 170 \wpre[\stateinterp]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\stuckness)(\mask, \expr, \Lam\val.\prop) Ralf Jung committed Oct 06, 2016 171 \end{align*} Ralf Jung committed Dec 13, 2017 172 173 The $\stateinterp$ will always be set by the context; typically, when instantiating Iris with a language, we also pick the corresponding state interpretation $\stateinterp$. All proof rules leave $\stateinterp$ unchanged. Ralf Jung committed Dec 12, 2017 174 175 If we leave away the mask $\mask$, we assume it to default to $\top$. If we leave away the stuckness $\stuckness$, it defaults to $\NotStuck$. Ralf Jung committed Oct 06, 2016 176 Ralf Jung committed Oct 10, 2016 177 \paragraph{Laws of weakest precondition.} Ralf Jung committed Oct 22, 2016 178 The following rules can all be derived: Ralf Jung committed Oct 04, 2016 179 180 \begin{mathpar} \infer[wp-value] Ralf Jung committed Dec 12, 2017 181 {}{\prop[\val/\var] \proves \wpre{\val}[\stuckness;\mask]{\Ret\var.\prop}} Ralf Jung committed Oct 04, 2016 182 183 \infer[wp-mono] Ralf Jung committed Dec 12, 2017 184 185 {\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB \and (\stuckness_2 = \MaybeStuck \lor \stuckness_1 = \stuckness_2)} {\vctx\mid\wpre\expr[\stuckness_1;\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\stuckness_2;\mask_2]{\Ret\var.\propB}} Ralf Jung committed Oct 04, 2016 186 Ralf Jung committed Oct 21, 2016 187 \infer[fup-wp] Ralf Jung committed Dec 12, 2017 188 {}{\pvs[\mask] \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\prop}} Ralf Jung committed Oct 04, 2016 189 Ralf Jung committed Oct 21, 2016 190 \infer[wp-fup] Ralf Jung committed Dec 12, 2017 191 {}{\wpre\expr[\stuckness;\mask]{\Ret\var.\pvs[\stuckness;\mask] \prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\prop}} Ralf Jung committed Oct 04, 2016 192 193 \infer[wp-atomic] Ralf Jung committed Dec 12, 2017 194 195 196 197 {\stuckness = \NotStuck \Ra \atomic(\expr) \and \stuckness = \MaybeStuck \Ra \stronglyAtomic(\expr)} {\pvs[\mask_1][\mask_2] \wpre\expr[\stuckness;\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop} \proves \wpre\expr[\stuckness;\mask_1]{\Ret\var.\prop}} Ralf Jung committed Oct 04, 2016 198 199 \infer[wp-frame] Ralf Jung committed Dec 12, 2017 200 {}{\propB * \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\propB*\prop}} Ralf Jung committed Oct 04, 2016 201 202 203 \infer[wp-frame-step] {\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1} Ralf Jung committed Dec 12, 2017 204 {\wpre\expr[\stuckness;\mask_2]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\stuckness;\mask_1]{\Ret\var.\propB*\prop}} Ralf Jung committed Oct 04, 2016 205 206 207 \infer[wp-bind] {\text{$\lctx$ is a context}} Ralf Jung committed Dec 12, 2017 208 {\wpre\expr[\stuckness;\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\stuckness;\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\stuckness;\mask]{\Ret\varB.\prop}} Ralf Jung committed Oct 04, 2016 209 210 \end{mathpar} Ralf Jung committed Dec 12, 2016 211 We will also want a rule that connect weakest preconditions to the operational semantics of the language. Ralf Jung committed Oct 04, 2016 212 213 \begin{mathpar} \infer[wp-lift-step] Ralf Jung committed Dec 12, 2016 214 {\toval(\expr_1) = \bot} Ralf Jung committed Oct 04, 2016 215 { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below... Ralf Jung committed Dec 13, 2017 216 ~~\All \state_1. \stateinterp(\state_1) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\mask] \Bigl(\stateinterp(\state_2) * \wpre[\stateinterp]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre[\stateinterp]{\expr_\f}[\stuckness;\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre[\stateinterp]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop} Ralf Jung committed Oct 04, 2016 217 218 219 \end{inbox}} } \end{mathpar} Ralf Jung committed Dec 12, 2016 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 % We can further derive some slightly simpler rules for special cases. % \begin{mathparpagebreakable} % \infer[wp-lift-pure-step] % {\All \state_1. \red(\expr_1, \state_1) \and % \All \state_1, \expr_2, \state_2, \vec\expr. \expr_1,\state_1 \step \expr_2,\state_2,\vec\expr \Ra \state_1 = \state_2 } % {\later\All \state, \expr_2, \vec\expr. (\expr_1,\state \step \expr_2, \state,\vec\expr) \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}} % \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, \vec\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\vec\expr) * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\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, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \vec\expr = \vec\expr'} % {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} % \infer[wp-lift-pure-det-step] % {\All \state_1. \red(\expr_1, \state_1) \\ % \All \state_1, \expr_2', \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \vec\expr = \vec\expr'} % {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\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 244 245 Ralf Jung committed Oct 10, 2016 246 \paragraph{Adequacy of weakest precondition.} Ralf Jung committed Oct 04, 2016 247 Ralf Jung committed Oct 10, 2016 248 249 250 251 The purpose of the adequacy statement is to show that our notion of weakest preconditions is \emph{realistic} in the sense that it actually has anything to do with the actual behavior of the program. There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with. Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck. Ralf Jung committed Jan 11, 2017 252 \begin{defn}[Adequacy] Ralf Jung committed Dec 12, 2017 253 A program $\expr$ in some initial state $\state$ is \emph{adequate} for stuckness $\stuckness$ and a set $V \subseteq \Val$ of legal return values ($\expr, \state \vDash_\stuckness V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpstep^\ast (\tpool', \state')$ we have Ralf Jung committed Jan 11, 2017 254 \begin{enumerate} Ralf Jung committed Dec 12, 2017 255 \item Safety: If $\stuckness = \NotStuck$, then for any $\expr' \in \tpool'$ we have that either $\expr'$ is a Ralf Jung committed Jan 11, 2017 256 value, or $$\red(\expr'_i,\state')$$: Ralf Jung committed Dec 12, 2017 257 $\stuckness = \NotStuck \Ra \All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')$ Ralf Jung committed Jan 11, 2017 258 259 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. \item Legal return value: If $\tpool'_1$ (the main thread) is a value $\val'$, then $\val' \in V$: Ralf Jung committed Feb 02, 2017 260 $\All \val',\tpool''. \tpool' = [\val'] \dplus \tpool'' \Ra \val' \in V$ Ralf Jung committed Jan 11, 2017 261 262 263 \end{enumerate} \end{defn} Ralf Jung committed Jan 12, 2017 264 265 266 To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic: $\pred : \Val \to \Prop \in \SigFn$ Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ reflects some set $V$ of legal return values into the logic (also see \Sref{sec:model}): Ralf Jung committed Oct 10, 2016 267 $\begin{array}{rMcMl} Robbert Krebbers committed Oct 17, 2016 268 \Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\ Ralf Jung committed Oct 10, 2016 269 270 271 272 \Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V} \end{array}$ The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound. The adequacy statement now reads as follows: Ralf Jung committed Oct 04, 2016 273 \begin{align*} Ralf Jung committed Jan 12, 2017 274 &\All \mask, \expr, \val, \state. Robbert Krebbers committed Aug 11, 2018 275 \\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp. \stateinterp(\state) * \wpre[\stateinterp]{\expr}[\stuckness;\mask]{x.\; \pred(x)}) \Ra Ralf Jung committed Dec 12, 2017 276 \\&\expr, \state \vDash_\stuckness V Ralf Jung committed Oct 04, 2016 277 \end{align*} Ralf Jung committed Jan 11, 2017 278 Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update. Ralf Jung committed Oct 04, 2016 279 Ralf Jung committed Oct 10, 2016 280 \paragraph{Hoare triples.} Robbert Krebbers committed Dec 10, 2017 281 It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq. Ralf Jung committed Oct 10, 2016 282 283 Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple: $Ralf Jung committed Oct 21, 2016 284 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \wand \wpre{\expr}[\mask]{\Ret\val.\propB})} Ralf Jung committed Oct 10, 2016 285$ Ralf Jung committed Dec 13, 2017 286 We assume the state interpretation $\stateinterp$ to be fixed by the context. Ralf Jung committed Oct 04, 2016 287 Ralf Jung committed Oct 10, 2016 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 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 \\ Ralf Jung committed Dec 12, 2017 321 \atomic(\expr) Ralf Jung committed Oct 10, 2016 322 323 324 325 326 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 } {\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 353 Ralf Jung committed Dec 10, 2017 354 \subsection{Invariant Namespaces} Ralf Jung committed Oct 10, 2016 355 356 \label{sec:namespaces} Robbert Krebbers committed Dec 10, 2017 357 In \Sref{sec:invariants}, we defined a proposition $\knowInv\iname\prop$ expressing knowledge (\ie the proposition is persistent) that $\prop$ is maintained as invariant with name $\iname$. Ralf Jung committed Oct 10, 2016 358 359 360 361 362 363 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. Jacques-Henri Jourdan committed Oct 13, 2016 364 Namespaces are sets of invariants, following a tree-like structure: Ralf Jung committed Oct 10, 2016 365 366 367 368 369 370 371 372 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. Robbert Krebbers committed Oct 17, 2016 373 Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \List(\nat)$ be the type of \emph{invariant namespaces}. Ralf Jung committed Oct 10, 2016 374 375 376 377 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). Robbert Krebbers committed Oct 17, 2016 378 They, too, are lists of $\nat$, the same type as namespaces. Ralf Jung committed Dec 07, 2016 379 380 In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of plain'' invariant names. Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite. Ralf Jung committed Oct 10, 2016 381 382 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)}$ Robbert Krebbers committed Dec 10, 2017 383 We will overload the notation for invariant propositions for using namespaces instead of names: Ralf Jung committed Oct 10, 2016 384 $\knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop}$ Ralf Jung committed Oct 21, 2016 385 We can now derive the following rules (this involves unfolding the definition of fancy updates): Ralf Jung committed Oct 10, 2016 386 387 \begin{mathpar} \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop} Ralf Jung committed Oct 04, 2016 388 Jacques-Henri Jourdan committed Oct 13, 2016 389 \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \knowInv\namesp\prop} Ralf Jung committed Oct 04, 2016 390 Ralf Jung committed Oct 10, 2016 391 392 393 \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 394 Ralf Jung committed Oct 10, 2016 395 396 397 398 \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 399 Ralf Jung committed Oct 10, 2016 400 401 402 403 \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. Robbert Krebbers committed Dec 10, 2017 404 Accessors are propositions of the form Ralf Jung committed Oct 10, 2016 405 406 $\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC)$ Robbert Krebbers committed Dec 10, 2017 407 408 One way to think about such propositions is as follows: Given some accessor, if during our verification we have the proposition $\prop$ and the mask $\mask_1$ available, we can use the accessor to \emph{access} $\propB$ and obtain the witness $\var$. Ralf Jung committed Oct 10, 2016 409 410 411 412 413 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$. Ralf Jung committed Feb 02, 2017 414 415 416 417 418 419 420 421 422 423 Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the corresponding proof rules for fancy updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any \emph{atomic} expression: \begin{mathpar} \inferH{Acc-vs} {\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \and \All\var. \propB * \prop_F \vs[\mask_2] \Exists\varB. \propB' * \prop_F} {\prop * \prop_F \vs[\mask_1] \propC * \prop_F} \inferH{Acc-Ht} {\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \and \All\var. \hoare{\propB * \prop_F}\expr{\Exists\varB. \propB' * \prop_F}[\mask_2] \and Ralf Jung committed Dec 12, 2017 424 \atomic(\expr)} Ralf Jung committed Feb 02, 2017 425 426 427 {\hoare{\prop * \prop_F}\expr{\propC * \prop_F}[\mask_1]} \end{mathpar} Ralf Jung committed Oct 10, 2016 428 429 430 431 432 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 Jung committed Oct 04, 2016 433 Ralf Jung committed Dec 06, 2016 434 435 For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition: $\Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop)$ Robbert Krebbers committed Dec 10, 2017 436 This accessor is idempotent'' in the sense that it does not actually change the state. After applying it, we get our $\prop$ back so we end up where we started. Ralf Jung committed Dec 06, 2016 437 Ralf Jung committed Oct 04, 2016 438 439 440 441 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: