From 8b008be491e5c51ed475f0a3c8dc14629a578a80 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Mon, 12 Dec 2016 17:47:42 +0100
Subject: [PATCH] docs: update atomicity
---
CHANGELOG.md | 16 ++++++++--------
docs/language.tex | 11 ++++++++---
2 files changed, 16 insertions(+), 11 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b3463405..1d5395f2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,9 +5,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
## Iris 3.0 (unfinished)
-* There now is a deprecation process. The modules `*.deprecated`
- contain deprecated notations and definitions that are provided for
- backwards compatibility and will be removed in a future version of Iris.
+* There now is a deprecation process. The modules `*.deprecated` contain
+ deprecated notations and definitions that are provided for backwards
+ compatibility and will be removed in a future version of Iris.
* View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view
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
* 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
general Iris notion of a language.
-* [#] Slightly weaker notion of atomicity: an expression is atomic if it reduces
- in one step to something that does not reduce further.
-* Changed notation for embedding Coq assertions into Iris. The new notation
- is ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope.
- (The old notations are provided in `base_logic.deprecated`.)
+* Slightly weaker notion of atomicity: an expression is atomic if it reduces in
+ one step to something that does not reduce further.
+* Changed notation for embedding Coq assertions into Iris. The new notation is
+ ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope. (The old notations are
+ provided in `base_logic.deprecated`.)
* Up-closure of namespaces is now a notation (↑) instead of a coercion.
* 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.
diff --git a/docs/language.tex b/docs/language.tex
index ad097eb7..4b34ed2d 100644
--- a/docs/language.tex
+++ b/docs/language.tex
@@ -2,7 +2,7 @@
\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
-\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
\begin{mathpar}
{\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
\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, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
+ 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) \]
\end{defn}
\begin{defn}[Context]
@@ -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}}
\end{mathpar}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End:
--
GitLab