Commit fc0a0cc9 authored by Ralf Jung's avatar Ralf Jung

describe observations in appendix

parent e3cdf16b
......@@ -11,7 +11,7 @@ Changes in and extensions of the theory:
the quantification over the next states and the later modality. This makes it
possible to prove more powerful lifting lemmas: The new versions feature an
"update that takes a step".
* [#] Weaken the semantics of CAS in heap_lang to be efficiently implementable:
* Weaken the semantics of CAS in heap_lang to be efficiently implementable:
CAS may only be used to compare "unboxed" values that can be represented in a
single machine word.
* Add weakest preconditions for total program correctness.
......@@ -19,7 +19,7 @@ Changes in and extensions of the theory:
longer considered experimental.
* The adequacy statement for weakest preconditions now also involves the
final state.
* [#] Add the notion of an "observation" to the language interface, so that
* Add the notion of an "observation" to the language interface, so that
every reduction step can optionally be marked with an event, and an execution
trace has a matching list of events. Change WP so that it is told the entire
future trace of observations from the beginning. Use this in heap_lang to
......@@ -29,9 +29,9 @@ Changes in and extensions of the theory:
functions.
* Add atomic updates and logically atomic triples, including tactic support.
See `heap_lang/lib/increment.v` for an example.
* [#] heap_lang now uses right-to-left evaluation order. This makes it
* heap_lang now uses right-to-left evaluation order. This makes it
significantly easier to write specifications of curried functions.
* [#] heap_lang values are now injected in heap_lang expressions via a specific
* heap_lang values are now injected in heap_lang expressions via a specific
constructor of the expr inductive type. This simplifies much the tactical
infrastructure around the language. In particular, this allow us to get rid
the reflection mechanism that was needed for proving closedness, atomicity and
......
......@@ -7,8 +7,8 @@
\RequirePackage{array}
\RequirePackage{dashbox}
\RequirePackage{tensor}
\RequirePackage{xifthen}
\RequirePackage{xparse}
\RequirePackage{xstring}
\RequirePackage{mathtools}
\usetikzlibrary{shapes}
......@@ -23,7 +23,7 @@
\newcommand{\nat}{\mathbb{N}}
\newcommand*{\Sep}{\scalerel*{\ast}{\sum}}
\newcommand*{\Sep}[1][]{\scalerel*{\ast}{\sum}\ifthenelse{\isempty{#1}}{}{_{#1}\;}}
\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
\newcommand\pord{\sqsubseteq}
......@@ -141,12 +141,6 @@
\newcommand{\iPreProp}{\textdom{iPreProp}}
\newcommand{\Wld}{\textdom{Wld}}
\newcommand{\Res}{\textdom{Res}}
\newcommand{\State}{\textdom{State}}
\newcommand{\Val}{\textdom{Val}}
\newcommand{\Loc}{\textdom{Loc}}
\newcommand{\Expr}{\textdom{Expr}}
\newcommand{\Var}{\textdom{Var}}
\newcommand{\ThreadPool}{\textdom{ThreadPool}}
% List
\newcommand{\List}{\ensuremath{\textdom{List}}}
......@@ -381,11 +375,21 @@
\newcommand{\val}{v}
\newcommand{\valB}{w}
\newcommand{\state}{\sigma}
\newcommand{\step}{\ra_{\mathsf{t}}}
\newcommand{\hstep}{\ra_{\mathsf{h}}}
\newcommand{\tpstep}{\ra_{\mathsf{tp}}}
\newcommand{\step}[1][]{\xrightarrow{{#1}}_{\mathsf{t}}}
\newcommand{\hstep}[1][]{\xrightarrow{{#1}}_{\mathsf{h}}}
\newcommand{\tpstep}[1][]{\xrightarrow{{#1}}_{\mathsf{tp}}}
\newcommand{\tpsteps}[1][]{\xrightarrow{{#1}}\mathrel{\vphantom{\to}^{*}_{\mathsf{tp}}}}
\newcommand{\lctx}{K}
\newcommand{\Lctx}{\textdom{Ctx}}
\newcommand{\obs}{\kappa}
\newcommand{\State}{\textdom{State}}
\newcommand{\Val}{\textdom{Val}}
\newcommand{\Loc}{\textdom{Loc}}
\newcommand{\Expr}{\textdom{Expr}}
\newcommand{\Var}{\textdom{Var}}
\newcommand{\Obs}{\textdom{Obs}}
\newcommand{\ThreadPool}{\textdom{ThreadPool}}
\newcommand{\toval}{\mathrm{expr\any to\any val}}
\newcommand{\ofval}{\mathrm{val\any to\any expr}}
......
\section{Language}
\label{sec:language}
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a nonempty set $\State$ of \emph{states} (metavariable $\state$) such that
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), a set $\Obs$ of \emph{observations} and a set $\State$ of \emph{states} (metavariable $\state$) such that
\begin{itemize}[itemsep=0pt]
\item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \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}
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \Expr \times \State \times \Expr \times \State \times \List(\Expr)\]
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. \\
\item There exists a \emph{primitive reduction relation} \[(-,- \;\step[-]\; -,-,-) \subseteq (\Expr \times \State) \times \List(\Obs) \times (\Expr \times \State \times \List(\Expr))\]
A reduction $\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr$ indicates that, when $\expr_1$ in state $\state_1$ reduces to $\expr_2$ with new state $\state_2$, the new threads in the list $\vec\expr$ is forked off and the observations $\vec\obs$ are made.
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 and no observations are made. \\
\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
\[ \Exists \expr_2, \state_2, \vec\expr. \expr,\state \step \expr_2,\state_2,\vec\expr \]
\[ \Exists \vec\obs, \expr_2, \state_2, \vec\expr. \expr,\state \step[\vec\obs] \expr_2,\state_2,\vec\expr \]
\end{defn}
\begin{defn}
An expression $\expr$ is \emph{weakly atomic} if it reduces in one step to something irreducible:
\[ \atomic(\expr) \eqdef \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \lnot \red(\expr_2, \state_2) \]
\[ \atomic(\expr) \eqdef \All\state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr \Ra \lnot \red(\expr_2, \state_2) \]
It is \emph{strongly atomic} if it reduces in one step to a value:
\[ \stronglyAtomic(\expr) \eqdef \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \toval(\expr_2) \neq \bot \]
\[ \stronglyAtomic(\expr) \eqdef \All\state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr \Ra \toval(\expr_2) \neq \bot \]
\end{defn}
We need two notions of atomicity to accommodate both kinds of weakest preconditions that we will define later:
If the weakest precondition ensures that the program cannot get stuck, weak atomicity is sufficient.
......@@ -34,11 +34,14 @@ Otherwise, we need strong atomicity.
A function $\lctx : \Expr \to \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 $
$$\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $$
\item One can perform reductions below $\lctx$:\\
$\All \expr_1, \state_1, \expr_2, \state_2, \vec\expr. \expr_1, \state_1 \step \expr_2,\state_2,\vec\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\vec\expr $
$$\All \expr_1, \state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \expr_1, \state_1 \step[\vec\obs] \expr_2,\state_2,\vec\expr \Ra \lctx(\expr_1), \state_1 \step[\vec\obs] \lctx(\expr_2),\state_2,\vec\expr $$
\item Reductions stay below $\lctx$ until there is a value in the hole:\\
$\All \expr_1', \state_1, \expr_2, \state_2, \vec\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\vec\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\vec\expr $
\begin{align*}
&\All \expr_1', \state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step[\vec\obs] \expr_2,\state_2,\vec\expr \Ra {}\\
&\qquad \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step[\vec\obs] \expr_2',\state_2,\vec\expr
\end{align*}
\end{enumerate}
\end{defn}
......@@ -51,15 +54,17 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\tpool \in \ThreadPool \eqdef \List(\Expr)
\]
\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
\judgment[Machine reduction]{\cfg{\tpool}{\state} \tpstep[\vec\obs]
\cfg{\tpool'}{\state'}}
\begin{mathpar}
\infer
{\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
{\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \tpstep[\vec\obs]
\cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}}
\end{mathpar}
We use $\tpsteps[-]$ for the reflexive transitive closure of $\tpstep[-]$, as usual concatenating the lists of observations of the individual steps.
%%% Local Variables:
%%% mode: latex
......
......@@ -156,17 +156,17 @@ Finally, we can define the core piece of the program logic, the proposition that
\paragraph{Defining weakest precondition.}
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$).
We further assume (as a parameter) a predicate $\stateinterp : \State \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, and a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-of threads.
The state interpretation can depend on the current physical state as well as the total number of \emph{forked} threads (that is one less that the total number of threads).
We further assume (as a parameter) a predicate $\stateinterp : \State \times \List(\Obs) \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, and a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-of threads.
The state interpretation can depend on the current physical state, the list of \emph{future} observations as well as the total number of \emph{forked} threads (that is one less that the total number of threads).
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.
Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck.
\begin{align*}
\textdom{wp}(\stateinterp, \pred_F, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\
& (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
& \Bigl(\toval(\expr) = \bot \land \All \state, n. \stateinterp(\state, n) \vsW[\mask][\emptyset] {}\\
&\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
&\qquad\qquad \stateinterp(\state', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
& \Bigl(\toval(\expr) = \bot \land \All \state, \vec\obs, \vec\obs', n. \stateinterp(\state, \vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] {}\\
&\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
&\qquad\qquad \stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep[\expr'' \in \vec\expr] \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
\wpre[\stateinterp;\pred_F]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\pred_F,\stuckness)(\mask, \expr, \Lam\val.\prop)
\end{align*}
The $\stateinterp$ and $\pred_F$ will always be set by the context; typically, when instantiating Iris with a language, we also pick the corresponding state interpretation $\stateinterp$ and fork-postcondition $\pred_F$.
......@@ -209,13 +209,15 @@ The following rules can all be derived:
\end{mathpar}
We will also want a rule that connect weakest preconditions to the operational semantics of the language.
This basically just copies the second branch (the non-value case) of the definition of weakest preconditions.
\begin{mathpar}
\infer[wp-lift-step]
{\toval(\expr_1) = \bot}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
~~\All \state_1,n. \stateinterp(\state_1,n) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
\qquad~~ \All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask]
\Bigl(\stateinterp(\state_2,n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\Bigr) {}\\
~~\All \state_1,\vec\obs,\vec\obs',n. \stateinterp(\state_1,\vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
\qquad~ \All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
\qquad\qquad\Bigl(\stateinterp(\state_2,\vec\obs',n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep[\expr_\f \in \vec\expr] \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\Bigr) {}\\
\proves \wpre[\stateinterp\pred_F]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
\end{inbox}} }
\end{mathpar}
......@@ -253,7 +255,7 @@ There are two properties we are looking for: First of all, the postcondition sho
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) \tpstep^\ast (\tpool', \state')$ we have
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')\):
......@@ -274,19 +276,20 @@ Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ ref
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:
\begin{align*}
&\All \mask, \expr, \val, \state.
\\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]{x.\; \All \state, m. \stateinterp(\state', m) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra
&\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
\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.
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:
\begin{align*}
&\All \mask, \expr, \val, \state.
\\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,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)}) \Ra
\\&([\expr], \state) \tpstep^\ast (\val :: \vec\val, \state') \Ra
\\&\val \in V
&\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
\end{align*}
\paragraph{Hoare triples.}
......
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