diff --git a/docs/iris.sty b/docs/iris.sty index 0b4428cdf7ca443f63d42fa042c7bb0c96a1cc47..414a1b0e9e73786a1198a4fa89508b99fbe5502f 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -139,6 +139,9 @@ \newcommand{\Var}{\textdom{Var}} \newcommand{\ThreadPool}{\textdom{ThreadPool}} +% List +\newcommand{\List}{\ensuremath{\textdom{List}}} + \newcommand{\cofe}{T} \newcommand{\cofeB}{U} \newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs diff --git a/docs/language.tex b/docs/language.tex index 65ae793f43ef9fdf4f31dceb753a4cae460e7ce9..f0d922fc08805a29974dea690c68ffc0fe09f30f 100644 --- a/docs/language.tex +++ b/docs/language.tex @@ -1,5 +1,3 @@ -\let\bar\overline - \section{Language} \label{sec:language} @@ -10,7 +8,7 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav {\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 (\cup_n \Expr^n)$ +\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 All values are stuck: @@ -19,12 +17,12 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav \begin{defn} An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if - $\Exists \expr_2, \state_2, \bar\expr. \expr,\state \step \expr_2,\state_2,\bar\expr$ + $\Exists \expr_2, \state_2, \vec\expr. \expr,\state \step \expr_2,\state_2,\vec\expr$ \end{defn} \begin{defn} An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value: - $\All\state_1, \expr_2, \state_2, \bar\expr. \expr, \state_1 \step \expr_2, \state_2, \bar\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2$ + $\All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2$ \end{defn} \begin{defn}[Context] @@ -33,9 +31,9 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav \item $\lctx$ does not turn non-values into values:\\ $\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, \bar\expr. \expr_1, \state_1 \step \expr_2,\state_2,\bar\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\bar\expr$ + $\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$ \item Reductions stay below $\lctx$ until there is a value in the hole:\\ - $\All \expr_1', \state_1, \expr_2, \state_2, \bar\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\bar\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\bar\expr$ + $\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$ \end{enumerate} \end{defn} @@ -45,15 +43,15 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. \paragraph{Machine syntax} $- \tpool \in \ThreadPool \eqdef \bigcup_n \Expr^n + \tpool \in \ThreadPool \eqdef \List(\Expr)$ \judgment[Machine reduction]{\cfg{\tpool}{\state} \step \cfg{\tpool'}{\state'}} \begin{mathpar} \infer - {\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr} + {\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step - \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \bar\expr}{\state_2}} + \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}} \end{mathpar} diff --git a/docs/program-logic.tex b/docs/program-logic.tex index 5577652af67bdd45807d65dfaacd7a25fb9ce2c1..cd7324b2ec22343030b8153499b72ba12b6dc777 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -160,8 +160,8 @@ We assume that everything making up the definition of the language, \ie values, \textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\ & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\ & \Bigl(\toval(\expr) = \bot \land \All \state. \ownGhost{\gname_{\textmon{State}}}{\authfull \state} \vsW[\mask][\emptyset] {}\\ - &\qquad \red(\expr, \state) * \later\All \expr', \state', \bar\expr. (\expr, \state \step \expr', \state', \bar\expr) \vsW[\emptyset][\mask] {}\\ - &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \state'} * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \bar\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\ + &\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\ + &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \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) \end{align*} @@ -210,14 +210,14 @@ In order to cover the most general case, those rules end up being more complicat \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... - ~~\pvs[\mask][\emptyset] \Exists \state_1. \red(\expr_1,\state_1) * \later\ownPhys{\state_1} * {}\\\qquad~~ \later\All \expr_2, \state_2, \bar\expr. \Bigl( (\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr) * \ownPhys{\state_2} \Bigr) \wand \pvs[\emptyset][\mask] \Bigl(\wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop} + ~~\pvs[\mask][\emptyset] \Exists \state_1. \red(\expr_1,\state_1) * \later\ownPhys{\state_1} * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr. \Bigl( (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) * \ownPhys{\state_2} \Bigr) \wand \pvs[\emptyset][\mask] \Bigl(\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} \end{inbox}} } \\\\ \infer[wp-lift-pure-step] {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \and - \All \state_1, \expr_2, \state_2, \bar\expr. \expr_1,\state_1 \step \expr_2,\state_2,\bar\expr \Ra \state_1 = \state_2 } - {\later\All \state, \expr_2, \bar\expr. (\expr_1,\state \step \expr_2, \state,\bar\expr) \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}} + \All \state_1, \expr_2, \state_2, \vec\expr. \expr_1,\state_1 \step \expr_2,\state_2,\vec\expr \Ra \state_1 = \state_2 } + {\later\All \state, \expr_2, \vec\expr. (\expr_1,\state \step \expr_2, \state,\vec\expr) \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}} \end{mathpar} We can further derive some slightly simpler rules for special cases: @@ -226,20 +226,20 @@ We can derive some specialized forms of the lifting axioms for the operational s \infer[wp-lift-atomic-step] {\atomic(\expr_1) \and \red(\expr_1, \state_1)} - { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \bar\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\bar\expr) * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} + { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \vec\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\vec\expr) * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} \end{inbox}} } \infer[wp-lift-atomic-det-step] {\atomic(\expr_1) \and \red(\expr_1, \state_1) \and - \All \expr'_2, \state'_2, \bar\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\bar\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \bar\expr = \bar\expr'} - {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \All \expr'_2, \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \vec\expr = \vec\expr'} + {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \infer[wp-lift-pure-det-step] {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \\ - \All \state_1, \expr_2', \state'_2, \bar\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\bar\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \bar\expr = \bar\expr'} - {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \All \state_1, \expr_2', \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \vec\expr = \vec\expr'} + {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \end{mathparpagebreakable} @@ -369,14 +369,14 @@ Furthermore, we will often know that namespaces are \emph{disjoint} just by look The namespaces $\namesp.\texttt{iris}$ and $\namesp.\texttt{gps}$ are disjoint no matter the choice of $\namesp$. As a result, there is often no need to track disjointness of namespaces, we just have to pick the namespaces that we allocate our invariants in accordingly. -Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \textlog{list}(\mathbb N)$ be the type of \emph{invariant namespaces}. +Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \List(\mathbb N)$ be the type of \emph{invariant namespaces}. We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$. (In other words, the list is backwards''. This is because cons-ing to the list, like the dot does above, is easier to deal with in Coq than appending at the end.) The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name). They, too, are lists of $\mathbb N$, the same type as namespaces. In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\mathbb N$, the type of plain'' invariant names. -Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\textlog{list}(\mathbb N)$ is countable. +Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\mathbb N)$ is countable. Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: $\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}$ We will overload the notation for invariant assertions for using namespaces instead of names: