docs: WP stuckness

docs/iris.sty

@@ -264,6 +264,10 @@
 
 \newcommand{\stateinterp}{S}
 
+\newcommand\stuckness{s}
+\newcommand\NotStuck{\textlog{NotStuck}}
+\newcommand\MaybeStuck{\textlog{Stuck}}
+
 \newcommand{\later}{\mathop{{\triangleright}}}
 \newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
 \newcommand{\always}{\mathop{\Box}}
@@ -359,7 +363,6 @@
 \newcommand{\inhabited}[1]{\textlog{inhabited}(#1)}
 \newcommand{\timeless}[1]{\textlog{timeless}(#1)}
 \newcommand{\persistent}[1]{\textlog{persistent}(#1)}
-\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
 \newcommand{\infinite}{\textlog{infinite}}
 
 \newcommand\InvName{\textdom{InvName}}
@@ -387,6 +390,7 @@
 \newcommand{\toval}{\mathrm{expr\any to\any val}}
 \newcommand{\ofval}{\mathrm{val\any to\any expr}}
 \newcommand{\atomic}{\mathrm{atomic}}
+\newcommand{\stronglyAtomic}{\mathrm{strongly\any atomic}}
 \newcommand{\red}{\mathrm{red}}
 \newcommand{\Lang}{\Lambda}
 

docs/iris.tex

@@ -43,7 +43,7 @@ That paper is hence much more suited as an introduction to the model of Iris tha
 The following differences between Iris as described in \citetitle{iris-ground-up} and the latest version documented here are worth mentioning:
 \begin{itemize}
 \item As an experimental feature, we added the \emph{plainly modality} $\plainly$.
-\item \ralf{TODO: WP stuckness bits.}
+\item As an experimental feature, weakest preconditions take a \emph{stuckness} $\stuckness$ as parameter, indicating whether the program may get stuck or not.
 \end{itemize}
 \endgroup
 

docs/language.tex

@@ -21,9 +21,14 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav
 \end{defn}
 
 \begin{defn}
-  An expression $\expr$ is \emph{atomic} if it reduces in one step to something irreducible:
-  \[ \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) \]
+  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) \]
+  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 \]
 \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.
+Otherwise, we need strong atomicity.
 
 \begin{defn}[Context]
   A function $\lctx : \Expr \to \Expr$ is a \emph{context} if the following conditions are satisfied:

docs/program-logic.tex

@@ -158,49 +158,52 @@ Finally, we can define the core piece of the program logic, the proposition that
 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 \to \iProp$ that interprets the physical state as an Iris proposition.
 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} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\
+  \textdom{wp}_\stuckness \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\
         & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
         & \Bigl(\toval(\expr) = \bot \land \All \state. \stateinterp(\state) \vsW[\mask][\emptyset] {}\\
-        &\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
+        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
         &\qquad\qquad \stateinterp(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
 %  (* value case *)
-  \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\mask, \expr, \Lam\val.\prop)
+  \wpre\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}_\stuckness(\mask, \expr, \Lam\val.\prop)
 \end{align*}
-If we leave away the mask, we assume it to default to $\top$.
+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$.
 
 \paragraph{Laws of weakest precondition.}
 The following rules can all be derived:
 \begin{mathpar}
 \infer[wp-value]
-{}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}}
+{}{\prop[\val/\var] \proves \wpre{\val}[\stuckness;\mask]{\Ret\var.\prop}}
 
 \infer[wp-mono]
-{\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}}
+{\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}}
 
 \infer[fup-wp]
-{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
+{}{\pvs[\mask] \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\prop}}
 
 \infer[wp-fup]
-{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
+{}{\wpre\expr[\stuckness;\mask]{\Ret\var.\pvs[\stuckness;\mask] \prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\prop}}
 
 \infer[wp-atomic]
-{\physatomic{\expr}}
-{\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}}
+{\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}}
 
 \infer[wp-frame]
-{}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
+{}{\propB * \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\propB*\prop}}
 
 \infer[wp-frame-step]
 {\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
-{\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}}
+{\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}}
 
 \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}}
+{\wpre\expr[\stuckness;\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\stuckness;\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\stuckness;\mask]{\Ret\varB.\prop}}
 \end{mathpar}
 
 We will also want a rule that connect weakest preconditions to the operational semantics of the language.
@@ -208,7 +211,7 @@ We will also want a rule that connect weakest preconditions to the operational s
   \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. \stateinterp(\state_1) \vsW[\mask][\emptyset] \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{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr)  {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}
+        ~~\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{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\stuckness;\top]{\Ret\any.\TRUE}\Bigr)  {}\\\proves \wpre{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
       \end{inbox}} }
 \end{mathpar}
 
@@ -245,11 +248,11 @@ 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 a set $V \subseteq \Val$ of legal return values ($\expr, \state \vDash 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$ of legal return values ($\expr, \state \vDash_\stuckness V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpstep^\ast (\tpool', \state')$ we have
 \begin{enumerate}
-\item Safety: For any $\expr' \in \tpool'$ we have that either $\expr'$ is a
+\item Safety: If $\stuckness = \NotStuck$, then for any $\expr' \in \tpool'$ we have that either $\expr'$ is a
   value, or \(\red(\expr'_i,\state')\):
-  \[ \All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \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' \in V \]
@@ -267,8 +270,8 @@ The signature can of course state arbitrary additional properties of $\pred$, as
 The adequacy statement now reads as follows:
 \begin{align*}
  &\All \mask, \expr, \val, \state.
- \\&( \TRUE \proves {\upd}_\mask \Exists \stateinterp. \stateinterp(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
- \\&\expr, \state \vDash V
+ \\&( \TRUE \proves {\upd}_\mask \Exists \stateinterp. \stateinterp(\state) * \wpre{\expr}[\stuckness;\mask]{x.\; \pred(x)}) \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.
 
@@ -312,7 +315,7 @@ We only give some of the proof rules for Hoare triples here, since we usually do
   {\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}
+   \atomic(\expr)
   }
   {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']}
 \and
@@ -415,7 +418,7 @@ Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the corresponding proof rul
   \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
-   \physatomic\expr}
+   \atomic(\expr)}
   {\hoare{\prop * \prop_F}\expr{\propC * \prop_F}[\mask_1]}
 \end{mathpar}