Commit 8b008be4 authored by Ralf Jung's avatar Ralf Jung

docs: update atomicity

parent 390748ab
...@@ -5,9 +5,9 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -5,9 +5,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
## Iris 3.0 (unfinished) ## Iris 3.0 (unfinished)
* There now is a deprecation process. The modules `*.deprecated` * There now is a deprecation process. The modules `*.deprecated` contain
contain deprecated notations and definitions that are provided for deprecated notations and definitions that are provided for backwards
backwards compatibility and will be removed in a future version of Iris. compatibility and will be removed in a future version of Iris.
* View shifts are radically simplified to just internalize frame-preserving * View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view updates. Weakestpre is defined inside the logic, and invariants and view
shifts with masks are also coded up inside Iris. Adequacy of weakestpre is shifts with masks are also coded up inside Iris. Adequacy of weakestpre is
...@@ -23,11 +23,11 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -23,11 +23,11 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Renaming and moving things around: uPred and the rest of the base logic are * Renaming and moving things around: uPred and the rest of the base logic are
in `base_logic`, while `program_logic` is for everything involving the in `base_logic`, while `program_logic` is for everything involving the
general Iris notion of a language. general Iris notion of a language.
* [#] Slightly weaker notion of atomicity: an expression is atomic if it reduces * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
in one step to something that does not reduce further. one step to something that does not reduce further.
* Changed notation for embedding Coq assertions into Iris. The new notation * Changed notation for embedding Coq assertions into Iris. The new notation is
is ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope. ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope. (The old notations are
(The old notations are provided in `base_logic.deprecated`.) provided in `base_logic.deprecated`.)
* Up-closure of namespaces is now a notation (↑) instead of a coercion. * Up-closure of namespaces is now a notation (↑) instead of a coercion.
* With invariants and the physical state being handled in the logic, there * With invariants and the physical state being handled in the logic, there
is no longer any reason to demand the CMRA unit to be discrete. is no longer any reason to demand the CMRA unit to be discrete.
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
\label{sec: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$), and a nonempty set \State of \emph{states} (metavariable $\state$) such that
\begin{itemize} \begin{itemize}[itemsep=0pt]
\item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that \item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that
\begin{mathpar} \begin{mathpar}
{\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and
...@@ -21,8 +21,8 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav ...@@ -21,8 +21,8 @@ A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metav
\end{defn} \end{defn}
\begin{defn} \begin{defn}
An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value: 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 \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 \lnot \red(\expr_2, \state_2) \]
\end{defn} \end{defn}
\begin{defn}[Context] \begin{defn}[Context]
...@@ -55,3 +55,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. ...@@ -55,3 +55,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}} \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}}
\end{mathpar} \end{mathpar}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
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