Commit cd49700f authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers

update docs for new adequacy statement

parent fec84da6
......@@ -27,9 +27,9 @@ Changes in the theory of Iris itself:
the number of forked-off threads, and have a global fixed proposition that
describes the postcondition of each forked-off thread (instead of it being
`True`).
* `[#]` A stronger adequacy statement for weakest preconditions that involves
the final state, involves the post-condition of forked-off threads, and also
applies if the main-thread has not terminated.
* A stronger adequacy statement for weakest preconditions that involves
the final state, the post-condition of forked-off threads, and also applies if
the main-thread has not terminated.
* The user-chosen functor used to instantiate the Iris logic now goes from
COFEs to Cameras (it was OFEs to Cameras).
......
......@@ -250,48 +250,77 @@ This basically just copies the second branch (the non-value case) of the definit
\paragraph{Adequacy of weakest precondition.}
\newcommand\traceprop{\Sigma}
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.
\begin{defn}[Adequacy]
A program $\expr$ in some initial state $\state$ is \emph{adequate} for stuckness $\stuckness$ and a set $V \subseteq \Val \times \State$ of legal return-value-final-state combinations (written $\expr, \state \vDash_\stuckness V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpsteps[\vec\obs] (\tpool', \state')$ we have
\begin{enumerate}
\item Safety: If $\stuckness = \NotStuck$, then for any $\expr' \in \tpool'$ we have that either $\expr'$ is a
value, or \(\red(\expr'_i,\state')\):
\[ \stuckness = \NotStuck \Ra \All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state') \]
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$:
\[ \All \val',\tpool''. \tpool' = [\val'] \dplus \tpool'' \Ra (\val',\state') \in V \]
\end{enumerate}
\end{defn}
To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic:
\[ \pred : \Val \times \State \to \Prop \in \SigFn \]
Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ reflects some set $V$ of legal return values and final states into the logic (also see \Sref{sec:model}):
The most general form of the adequacy statement is about proving properties of arbitrary program executions.
That is, the goal is to prove a statement of the form
\[
\All \expr_0, \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra (\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \in \traceprop
\]
for some \emph{meta-level} relation $\traceprop$ characterizing the ``trace property'' we are interested in.
To state the adequacy theorem, we need a way to talk about $\traceprop$ inside Iris.
To this end, we assume that the signature $\Sig$ contains some predicate $\hat{\traceprop}$:
\[ \hat{\traceprop} : \Expr \times \State \times \List(\Obs) \times \List(\Expr) \times \State \to \Prop \in \SigFn \]
Furthermore, we assume that the \emph{interpretation} $\Sem{\hat{\traceprop}}$ of $\hat{\traceprop}$ reflects $\traceprop$ (also see \Sref{sec:model}):
\[\begin{array}{rMcMl}
\Sem\pred &:& \Sem{\Val\times\State\,} \nfn \Sem\Prop \\
\Sem\pred &\eqdef& \Lam (\val,\state). \Lam \any. \setComp{n}{(v,\state) \in V}
\Sem{\hat{\traceprop}} &:& \Sem{\Expr \times \State \times \List(\Obs) \times \List(\Expr) \times \State\,} \nfn \Sem\Prop \\
\Sem{\hat{\traceprop}} &\eqdef& \Lam (\expr_0, \state_0, \vec\obs, \tpool_1, \state_1). \Lam \any. \setComp{n}{(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \in \traceprop}
\end{array}\]
The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound.
The signature can of course state arbitrary additional properties of $\hat{\traceprop}$, as long as they are proven sound.
The adequacy statement now reads as follows:
\begin{align*}
&\All \mask, \expr, \state.
\\&( \TRUE \proves \All\vec\obs. \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]{x.\; \All \state, m. \stateinterp(\state', (), m) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra
\\&\expr, \state \vDash_\stuckness V
&\All \expr_0, \state_0, \vec\obs, \tpool_1, \state_1.\\
&( \TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F, \pred. {}\\
&\quad\stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; \pred(x)} * {}\\
&\quad(\All \expr_1, \tpool_1'. \tpool_1 = [\expr_1] \dplus \tpool_1' \wand {}\\
&\quad\quad (s = \NotStuck \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1) ) \wand {}\\
&\quad\quad \stateinterp(\state_1, (), |\tpool_1'|) \wand{}\\
&\quad\quad (\toval(\expr_1) \ne \bot \wand \pred(\toval(\expr_1))) \wand{}\\
&\quad\quad (\Sep[\expr \in \tpool_1'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))) \wand{}\\
&\quad\quad \pvs[\top,\emptyset] \hat{\traceprop}(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \\
&\quad ) \Ra{}\\
&([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra (\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \in \traceprop
\end{align*}
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.
Also, notice that the proof of $\expr$ must be performed with a universally quantified list of observations $\vec\obs$, but the \emph{entire} list is known to the proof from the beginning.
In other words, to show that $\traceprop$ holds for all possible executions of the program, we have to prove an entailment in Iris that, starting from the empty context, proves that the initial state interpretation holds, proves a weakest precondition, \emph{and} proves that $\hat{\traceprop}$ holds under the following assumptions:
\begin{itemize}
\item The final thread-pool $\tpool_1$ contains the final state of the main thread $\expr_1$, and any number of additional threads in $\tpool_1'$.
\item If this is a stuck-free weakest precondition, then all threads in the final thread-pool are either values or are reducible in the final state $\state_1$.
\item The state interpretation holds for the final state.
\item If the main thread reduced to a value, the post-condition $\pred$ of the weakest precondition holds for that value.
\item If any other thread reduced to a value, the forked-thread post-condition $\pred_F$ holds for that value.
\end{itemize}
Notice also that the adequacy statement quantifies over the program trace only once, so it can be easily specialized to, say, some particular initial state $\state_0$.
This lets us show properties that only hold for some executions.
Furthermore, 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.
As an example for how to use this adequacy theorem, let us say we wanted to prove that a program $\expr_0$ for which we derived a $\NotStuck$ weakest-precondition cannot get stuck.
We would pick
\[
\traceprop(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \eqdef \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1)
\]
and we would show the following in Iris:
\[
\TRUE \proves \All \state_0, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred_F, \pred. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\NotStuck;\top]{x.\; \pred(x)}
\]
The adequacy theorem would then give us:
\[
\All \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1)
\]
The following variant of adequacy also allows exploiting the second parameter of $\stateinterp$, the number of threads, but only applies when \emph{all} threads have reduced to a value:
Similarly, if we wanted to show that the final value of the main thread is always in some set $V \subseteq \Val$, we could pick
\[
\traceprop(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \eqdef \All\val_1, \tpool_1'. \tpool_1 = [\ofval(\val_1)] \dplus \tpool_1' \Ra \val_1 \in \Val
\]
and then we could derive the following from the main adequacy theorem:
\begin{align*}
&\All \mask, \expr, \state, \vec\obs, \val, \vec\val, \state'.
\\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]%
{x.\; \stateinterp(\state',(),|\vec\val|) * \Sep_{y \in \vec\val} \pred_F(y) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra
\\&([\expr], \state) \tpsteps[\vec\obs] (\val :: \vec\val, \state') \Ra
\\&(\val,\state') \in V
&(\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; x \in V}) \Ra{}\\
&\All \state_0, \vec\obs, \val_1, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] ([\ofval(\val_1)] \dplus \tpool_1, \state_1) \Ra \val_1 \in V
\end{align*}
\paragraph{Hoare triples.}
It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.
Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment