From 86967a810bc9db7291a23f16d36aee37862585fc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Jan 2017 20:42:35 +0100
Subject: [PATCH] docs: add Ales' description of the paradoxes
---
docs/iris.tex | 2 +
docs/paradoxes.tex | 237 +++++++++++++++++++++++++++++++++++++++++++++
docs/setup.tex | 1 +
3 files changed, 240 insertions(+)
create mode 100644 docs/paradoxes.tex
diff --git a/docs/iris.tex b/docs/iris.tex
index 863077ee3..83d56c6d7 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -52,6 +52,8 @@ For further information, visit the Iris project website at \url{http://plv.mpi-s
\endgroup\clearpage\begingroup
\input{derived}
\endgroup\clearpage\begingroup
+\input{paradoxes}
+\endgroup\clearpage\begingroup
\printbibliography
\endgroup
diff --git a/docs/paradoxes.tex b/docs/paradoxes.tex
new file mode 100644
index 000000000..099d1a9e7
--- /dev/null
+++ b/docs/paradoxes.tex
@@ -0,0 +1,237 @@
+\section{Logical paradoxes}
+\newcommand{\starttoken}{\textsc{s}}
+\newcommand{\finishtoken}{\textsc{f}}
+
+In this section we provide proofs of some logical inconsistencies that arise when slight changes are made to the Iris logic.
+
+\subsection{Saved propositions without a later}
+\label{sec:saved-prop-no-later}
+
+As a preparation for the proof about invariants in \Sref{app:section:invariants-without-a-later}, we show that omitting the later modality from a variant of \emph{saved propositions} leads to a contradiction.
+Saved propositions have been introduced in prior work~\cite{dodds:higher-order-sync,iris2} to prove correctness of synchronization primitives; we will explain all that is necessary here.
+The counterexample assumes a higher-order logic with separating conjunction, magic wand and the modalities $\always$ and $\upd$ satisfying the rules in \Sref{sec:base-logic}.
+
+\begin{thm}
+\label{thm:counterexample-1}
+If there exists a type $\GName$ and an assertion $\_ \Mapsto \_ : \GName \to \Prop \to \Prop$ associating names $\gamma : \GName$ to propositions and satisfying:
+\begin{align}
+ \proves{}& \upd \Exists \gname : \GName. \gname \Mapsto P(\gname)
+ \tagH{sprop-alloc} \\
+ \gname \Mapsto P \proves{}& \always (\gname \Mapsto P)
+ \tagH{sprop-persist} \\
+ \gname \Mapsto \prop * \gname \Mapsto \propB \proves{}
+ &
+ \prop \Lra \propB
+ \tagH{sprop-agree}
+\end{align}
+then $\proves\upd \FALSE$.
+\end{thm}
+
+The type $\GName$ should be thought of as the type of ``locations'' and $\gname \Mapsto P$ should be read as stating that location $\gname$ ``stores'' proposition $P$.
+Notice that these are immutable locations, so the maps-to assertion is persistent.
+The rule \ruleref{sprop-alloc} is then thought of as allocation, and the rule \ruleref{sprop-agree} states that a given location $\gname$ can only store \emph{one} proposition, so multiple witnesses covering the same location must agree.
+
+%Compared to saved propositions in prior work, \ruleref{sprop-alloc} is stronger since the stored proposition can depend on the name being allocated.
+%\derek{Can't we cut the above sentence? This makes it sound like we are doing something weird that we ought not to be since prior work didn't do it. But in fact, I thought that in our construction we don't really need to rely on this feature at all! So I'm confused.}
+The conclusion of \ruleref{sprop-agree} usually is guarded by a $\later$.
+The point of this theorem is to show that said later is \emph{essential}, as removing it introduces inconsistency.
+%
+The key to proving \thmref{thm:counterexample-1} is the following assertion:
+\begin{defn}
+$A(\gname) \eqdef \Exists \prop : \Prop. \always\lnot \prop \land \gname \Mapsto \prop$.
+\end{defn}
+Intuitively, $A(\gname)$ says that the saved proposition named $\gname$ does \emph{not} hold, \ie we can disprove it.
+Using \ruleref{sprop-persist}, it is immediate that $A(\gname)$ is persistent.
+
+Now, by applying \ruleref{sprop-alloc} with $A$, we obtain a proof of $\prop \eqdef \gname \Mapsto A(\gname)$: this says that the proposition named $\gname$ is the assertion saying that it, itself, doesn't hold.
+In other words, $\prop$ says that the assertion named $\gname$ expresses its own negation.
+Unsurprisingly, that leads to a contradiction, as is shown in the following lemma:
+\begin{lem} \label{lem:saved-prop-counterexample-not-agname} We have $\gname \Mapsto A(\gname) \proves \always\lnot A(\gname)$ and $\gname \Mapsto A(\gname) \proves A(\gname)$. \end{lem}
+\begin{proof}%[\lemref{lem:saved-prop-counterexample-not-agname}]
+\leavevmode
+ \begin{itemize}
+ \item First we show $\gname \Mapsto A(\gname) \proves \always\lnot A(\gname)$.
+ Since $\gname \Mapsto A(\gname)$ is persistent it suffices to show $\gname \Mapsto A(\gname) \proves \lnot A(\gname)$.
+ Suppose $\gname \Mapsto A(\gname)$ and $A(\gname)$.
+ Then by definition of \(A\) there is a $\prop$ such that $\always \lnot \prop$ and $\gname \Mapsto \prop$.
+ By \ruleref{sprop-agree} we have $\prop \Lra A(\gname)$ and so from $\lnot \prop$ we get $\lnot A(\gname)$, which leads to a contradiction with $A(\gname)$.
+
+ \item Using the first item we can now prove $\gname \Mapsto A(\gname) \proves A(\gname)$.
+ We need to prove
+ \begin{align*}
+ \Exists \prop : \Prop. \always \lnot \prop \land \gname \Mapsto \prop.
+ \end{align*}
+ We do so by picking $\prop$ to be $A(\gname)$, which leaves us to prove \(\always \lnot A(\gname) \land \gname \Mapsto A(\gname)\).
+ The last conjunct holds by assumption, and the first conjunct follows from the previous item of this lemma.
+ \end{itemize}
+\end{proof}
+
+With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple.
+\begin{proof}[\thmref{thm:counterexample-1}]
+ Using the previous lemmas we have
+ \begin{align*}
+ \proves \All \gname. \lnot (\gname \Mapsto A(\gname)).
+ \end{align*}
+ Together with the rule \ruleref{sprop-alloc} we thus derive $\upd \FALSE$.
+\end{proof}
+
+\subsection{Invariants without a later}
+\label{app:section:invariants-without-a-later}
+
+Now we come to the main paradox: if we remove the $\later$ from \ruleref{inv-open}, the logic becomes inconsistent.
+The theorem is stated as general as possible so taht it also applies to previous, less powerful versions of Iris.
+
+\begin{thm}
+ \label{thm:counterexample-2}
+ Assume a higher-order separation logic with $\always$ and an update modality with a binary mask ${\upd}_{\set{0,1}}$ (think: empty mask and full mask) satisfying strong monad rules with respect to separating conjunction and such that:
+ \begin{mathpar}
+ \inferhref{weaken-mask}{eq:update-weaken-mask}
+ {}{{\upd}_0 \prop \proves {\upd}_1 \prop}
+ \end{mathpar}
+
+\noindent
+ Assume a type $\InvName$ and an assertion $\knowInv{\cdot}{\cdot} : \InvName \to \Prop \to \Prop$ satisfying:
+%
+ \begin{mathpar}
+ \inferhref{inv-alloc}{eq:inv-alloc}
+ {}
+ {\prop \proves {\upd}_1 \Exists \iname. \knowInv \iname \prop}
+ \and
+ \inferhref{inv-persist}{eq:inv-persistent}
+ {}
+ {\knowInv \iname \prop \proves \always \knowInv \iname \prop}
+ \and
+ \inferhref{inv-open-nolater}{eq:inv-open}
+ {\prop * \propB \proves {\upd}_0 (\prop * \propC) }
+ {\knowInv \iname \prop * \propB \proves {\upd}_1 \propC}
+ \end{mathpar}
+
+\noindent
+ Finally, assume the existence of a type $\GName$ and two tokens $\ownGhost{\cdot}{\starttoken} : \GName \to \Prop$ and $\ownGhost{\cdot}{\finishtoken}: \GName \to \Prop$ parameterized by $\GName$ and satisfying the following properties:
+ \begin{mathpar}
+ \inferhref{start-alloc}{eq:start-alloc}
+ {}{\proves {\upd}_0 \Exists \gname. \ownGhost \gname \starttoken}
+ \and
+ \inferhref{start-finish}{eq:start-finish}
+ {}{\ownGhost \gname \starttoken \proves {\upd}_0 \ownGhost \gname \finishtoken}
+ \and
+ \inferhref{start-not-finished}{eq:start-not-finished}
+ {}{\ownGhost \gname \starttoken * \ownGhost \gname \finishtoken \proves \FALSE}
+ \and
+ \inferhref{finished-dup}{eq:finished-dup}
+ {}{\ownGhost \gname \finishtoken \proves \ownGhost \gname \finishtoken * \ownGhost \gname \finishtoken}
+ \end{mathpar}
+
+\noindent
+ Then $\TRUE \proves{\upd}_1 \FALSE$.
+\end{thm}
+
+
+The core of the proof is defining the $\Mapsto$ from the previous counterexample using invariants.
+Then, using the standard proof rules for invariants, we show that it satisfies \ruleref{sprop-alloc} and \ruleref{sprop-persist}.
+Furthermore, assuming the rule for opening invariants without a $\later$, we can prove a slightly weaker version of \ruleref{sprop-agree}, which is sufficient for deriving a contradiction.
+
+
+% Taking ${\upd}_\bot$ and ${\upd}_\top$ to be the fancy update modalities $\pvs[\emptyset]$
+% and $\pvs[\nat]$, respectively, we can see that Iris
+% \emph{almost} satisfies these axioms. First, to implement the tokens,
+% we can use the RA with the carrier
+% $\{\mundef,\epsilon,\starttoken,\finishtoken\}$ and operation
+% $\epsilon \mtimes x = x \mtimes \epsilon = x$,
+% $\finishtoken \mtimes \finishtoken = \finishtoken$ and otherwise
+% $x \mtimes y = \mundef$. Then, observe that the rules for
+% $\knowInv{\cdot}{\cdot}$ are special cases of (derivable) invariant
+% rules in Iris. The fly in the ointment is the \ruleref{eq:inv-open}
+% rule: in Iris, this rule would protect each occurrence of $\prop$
+% in the premise of the rule with a $\later$, whereas here they are
+% unprotected.
+
+We start by defining $\Mapsto$ satisfying (almost) the assumptions of \lemref{lem:counterexample-invariants-saved-prop-agree}.
+%
+\begin{defn}
+We define $\_ \Mapsto \_ : \GName \to \Prop \to \Prop$ as:
+%
+\begin{align*}
+ \gname \Mapsto \prop \eqdef \Exists \iname. \knowInv \iname {\ownGhost \gname \starttoken \lor \ownGhost \gname \finishtoken * \always \prop}.
+\end{align*}
+\end{defn}
+Note that using \ruleref{eq:inv-persistent}, it is immediate that $\gname \Mapsto \prop$ is persistent.
+
+We use the tokens $\ownGhost \gname \starttoken$ and $\ownGhost \gname \finishtoken$ to model invariants that can be initialized ``lazily'': $\ownGhost \gname \starttoken$ indicates that the invariant is still not initialized, whereas the duplicable $\ownGhost \gname \finishtoken$ indicates it has been initialized with a resource satisfying $\prop$.%
+%\footnote{We would usually require the token to be persistent, but it turns out the proof also works with the weaker assumption of duplicability.}
+% RK: cut the footnote, it takes space. Maybe restore later
+
+% TODO, explain this ...
+
+We can show variants of \ruleref{sprop-agree} and \ruleref{sprop-alloc} for the defined $\Mapsto$.
+\begin{lem}
+ \label{lem:counterexample-invariants-saved-prop-alloc}
+We have
+ \(\proves {\upd}_\top \Exists \gname. \gname \Mapsto \prop(\gname)\).
+\end{lem}
+\begin{proof}
+ We have to show the allocation rule \[\proves {\upd}_\top \Exists \gname. \gname \Mapsto \prop.\]
+ From \ruleref{eq:start-alloc} we have a $\gname$ such that ${\upd}_\bot \ownGhost \gname \starttoken$ holds and hence from \ruleref{eq:update-weaken-mask} we have ${\upd}_\top\ownGhost\gname \starttoken$.
+ Since we are proving a goal of the form ${\upd}_\top R$ we may assume $\ownGhost \gname \starttoken$.
+ Thus for any $\prop$ we have ${\upd}_\top\left(\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \prop\right)$.
+ Again since our goal is still of the form ${\upd}_\top$ we may assume $\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \always \prop$.
+ The rule \ruleref{eq:inv-alloc} then gives us precisely what we need.
+ \qed \end{proof}
+
+%
+\begin{lem}
+\label{lem:counterexample-invariants-saved-prop-agree}
+We have
+ \(
+ \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_\top \always \propB
+ \)
+and thus
+ \(
+ \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_\top \always \prop) \Lra ({\upd}_\top \always \propB).
+ \)
+\end{lem}
+
+\begin{proof}[\lemref{lem:counterexample-invariants-saved-prop-agree}]
+\begin{itemize}
+ \item We first show
+ \[\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_\top \always \propB.\]
+ We use \ruleref{eq:inv-open} to open the invariant in $\gname \Mapsto \prop$ and consider two cases:
+ %
+ \begin{enumerate}
+ \item $\ownGhost \gname \starttoken$(the invariant is ``uninitialized'') : In this case, we use \ruleref{eq:start-finish} to ``initialize'' the invariant and obtain $\ownGhost{\gname}{\finishtoken}$.
+ Then we duplicate $\ownGhost \gname \finishtoken$, and use it together with $\always \prop$ to close the invariant.
+ \item $\ownGhost \gname \finishtoken * \always \prop$ (the invariant is ``initialized''): In this case we duplicate $\ownGhost \gname \finishtoken$, and use a copy to close the invariant.
+ \end{enumerate}
+ %
+ After closing the invariant, we have obtained $\ownGhost \gname \finishtoken$.
+ Hence, it is sufficient to prove
+ \[
+ \ownGhost{\gname}{\finishtoken} * \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_\top \always \propB.\]
+ We proceed by using \ruleref{eq:inv-open} to open the other invariant in $\gname \Mapsto \propB$, and we again consider two cases:
+ \begin{enumerate}
+ \item $\ownGhost{\gname}{\starttoken}$ (the invariant is ``uninitialized''): As witnessed by \ruleref{eq:start-not-finished}, this cannot happen, so we derive a contradiction.
+ Notice that this is a key point of the proof: because the two invariants ($\gname \Mapsto \prop$ and $\gname \Mapsto \propB$) \emph{share} the ghost name $\gname$, initializing one of them is enough to show that the other one has been initialized.
+ Essentially, this is an indirect way of saying that really, we have been opening the same invariant two times.
+ \item $\ownGhost{\gname}{\finishtoken} * \always \propB$ (the invariant is ``initialized''):
+ Since $\always \propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\upd}_\top \always \propB$.
+ \end{enumerate}
+\item By applying the above twice, we easily obtain
+\[ \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_\top \always \prop) \Lra ({\upd}_\top \always \propB) \]
+\end{itemize}
+\qed \end{proof}
+% When allocating $\gname \Mapsto \prop(\gname)$ in \lemref{lem:counterexample-invariants-saved-prop-alloc}, we will start off in ``state'' $\ownGhost \gname \starttoken$, and once we have $P$ in \lemref{lem:counterexample-invariants-saved-prop-agree} we use \ruleref{eq:start-finish} to transition to $\ownGhost\gname \finishtoken$, obtaining ourselves a copy of said token.
+% Finally, we use this token with $\gname \Mapsto \propB$ to obtain a proof of $\propB$.
+Intuitively, \lemref{lem:counterexample-invariants-saved-prop-agree} shows that we can ``convert'' a proof from $\prop$ to $\propB$.
+
+We are now in a position to replay the counterexample from \Sref{sec:saved-prop-no-later}.
+The only difference is that because \lemref{lem:counterexample-invariants-saved-prop-agree} is slightly weaker than the rule \ruleref{sprop-agree} of \thmref{thm:counterexample-1}, we need to use ${\upd}_\top \FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
+we let \(
+ A(\gname) \eqdef \Exists \prop : \Prop. \always (\prop \Ra {\upd}_\top \FALSE) \land \gname \Mapsto \prop\)
+and replay the proof that we have presented above.
+
+%TODO: What about executing a view shift under a later?
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End:
diff --git a/docs/setup.tex b/docs/setup.tex
index 5dff19405..f7b3d1b09 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -79,6 +79,7 @@
\newcommand*{\Sref}[1]{\hyperref[#1]{\S\ref*{#1}}}
\newcommand*{\secref}[1]{\hyperref[#1]{Section~\ref*{#1}}}
\newcommand*{\lemref}[1]{\hyperref[#1]{Lemma~\ref*{#1}}}
+\newcommand*{\thmref}[1]{\hyperref[#1]{Theorem~\ref*{#1}}}
\newcommand{\corref}[1]{\hyperref[#1]{Cor.~\ref*{#1}}}
\newcommand*{\defref}[1]{\hyperref[#1]{Definition~\ref*{#1}}}
\newcommand*{\egref}[1]{\hyperref[#1]{Example~\ref*{#1}}}
--
GitLab