diff --git a/docs/iris.tex b/docs/iris.tex index 863077ee3c8507d5281ce84c4bfb17837502027b..83d56c6d7aa6b9e1a67b75449110abedc0082149 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 0000000000000000000000000000000000000000..099d1a9e7efdb9c8385c5f7ad573e994d9a4e2bf --- /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 5dff19405d2eaf33e3f1712b4e0c1f722ecddc06..f7b3d1b097f7317ab13e3a6e7fa7e613a94ca3de 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}}}