From 6676a195c79742d3125b447b8470af477229fb4f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 May 2022 19:38:50 +0200
Subject: [PATCH] document HeapLang syntax and operational semantics
---
iris_heap_lang/lang.v | 17 +-
iris_staging/heap_lang/interpreter.v | 20 +-
tex/bib.bib | 17 ++
tex/heaplang.sty | 85 ++++++++
tex/heaplang.tex | 281 +++++++++++++++++++++++++++
tex/iris.sty | 1 +
tex/iris.tex | 5 +-
tex/language.tex | 1 +
tex/setup.tex | 1 +
9 files changed, 411 insertions(+), 17 deletions(-)
create mode 100644 tex/heaplang.sty
create mode 100644 tex/heaplang.tex
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 54e771682..4141e9e45 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -107,8 +107,6 @@ Inductive expr :=
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
- (* Concurrency *)
- | Fork (e : expr)
(* Heap *)
| AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
| Free (e : expr)
@@ -117,6 +115,8 @@ Inductive expr :=
| CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
| Xchg (e0 : expr) (e1 : expr) (* exchange *)
| FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
+ (* Concurrency *)
+ | Fork (e : expr)
(* Prophecy *)
| NewProph
| Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
@@ -243,7 +243,6 @@ Proof.
| InjR e, InjR e' => cast_if (decide (e = e'))
| Case e0 e1 e2, Case e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
- | Fork e, Fork e' => cast_if (decide (e = e'))
| AllocN e1 e2, AllocN e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Free e, Free e' =>
@@ -257,6 +256,7 @@ Proof.
cast_if_and (decide (e0 = e0')) (decide (e1 = e1'))
| FAA e1 e2, FAA e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+ | Fork e, Fork e' => cast_if (decide (e = e'))
| NewProph, NewProph => left _
| Resolve e0 e1 e2, Resolve e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
@@ -410,6 +410,11 @@ Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
(** Evaluation contexts *)
+(** Note that [ResolveLCtx] is not by itself an evaluation context item: we do
+not reduce directly under Resolve's first argument. We only reduce things nested
+further down. Once no nested contexts exist any more, the expression must take
+exactly one more step to a value, and Resolve then (atomically) also uses that
+value for prophecy resolution. *)
Inductive ectx_item :=
| AppLCtx (v2 : val)
| AppRCtx (e1 : expr)
@@ -498,7 +503,6 @@ Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
| InjL e => InjL (subst x v e)
| InjR e => InjR (subst x v e)
| Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
- | Fork e => Fork (subst x v e)
| AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Free e => Free (subst x v e)
| Load e => Load (subst x v e)
@@ -506,6 +510,7 @@ Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
+ | Fork e => Fork (subst x v e)
| NewProph => NewProph
| Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
end.
@@ -661,8 +666,6 @@ Inductive head_step : expr → state → list observation → expr → state →
head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
| CaseRS v e1 e2 σ :
head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
- | ForkS e σ:
- head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
| AllocNS n v σ l :
(0 < n)%Z →
(∀ i, (0 ≤ i)%Z → (i < n)%Z → σ.(heap) !! (l +ₗ i) = None) →
@@ -707,6 +710,8 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
(Val $ LitV $ LitInt i1) (state_upd_heap <[l:=Some $ LitV (LitInt (i1 + i2))]>σ)
[]
+ | ForkS e σ:
+ head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
| NewProphS σ p :
p ∉ σ.(used_proph_id) →
head_step NewProph σ
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index eca5ef424..322b43439 100644
--- a/iris_staging/heap_lang/interpreter.v
+++ b/iris_staging/heap_lang/interpreter.v
@@ -749,15 +749,15 @@ Section interpret_ok.
(repeat case_match; subst; try errored;
success;
eauto using state_wf_upd).
- - constructor; intros.
- simpl.
- apply state_wf_holds; auto.
- match goal with
| H: interp_alloc _ _ = (_, _) |- _ => invc H
end.
apply state_wf_init_alloc; eauto.
lia.
- apply state_wf_same_dom; eauto.
+ - constructor; intros.
+ simpl.
+ apply state_wf_holds; auto.
Qed.
Local Hint Resolve interpret_wf : core.
@@ -792,13 +792,6 @@ Section interpret_ok.
lazymatch goal with
| |- context[Case (Val ?v)] => destruct v; try errored; step_atomic; eauto
end.
- - (* Fork *)
- eapply rtc_once. exists [].
- lazymatch goal with
- | |- context[Fork ?e] => eapply (step_atomic _ _ _ _ [e] []); simpl; eauto
- end.
- apply head_prim_step; simpl.
- eauto using head_step.
- (* AllocN *)
lazymatch goal with
| H: interp_alloc _ _ = _ |- _ => invc H
@@ -806,6 +799,13 @@ Section interpret_ok.
eapply atomic_step. constructor; auto; intros.
simpl. apply state_wf_holds; eauto.
simpl; lia.
+ - (* Fork *)
+ eapply rtc_once. exists [].
+ lazymatch goal with
+ | |- context[Fork ?e] => eapply (step_atomic _ _ _ _ [e] []); simpl; eauto
+ end.
+ apply head_prim_step; simpl.
+ eauto using head_step.
Qed.
(** * Theory for expressions that are stuck after some execution steps. *)
diff --git a/tex/bib.bib b/tex/bib.bib
index a8f88cf36..240bf697b 100644
--- a/tex/bib.bib
+++ b/tex/bib.bib
@@ -3849,3 +3849,20 @@ year = {2013}
volume = {20},
year = {1955}
}
+
+@article{iris:prophecy,
+ author = {Ralf Jung and
+ Rodolphe Lepigre and
+ Gaurav Parthasarathy and
+ Marianna Rapoport and
+ Amin Timany and
+ Derek Dreyer and
+ Bart Jacobs},
+ title = {The future is ours: prophecy variables in separation logic},
+ journal = {{PACMPL}},
+ volume = {4},
+ number = {{POPL}},
+ doi = {10.1145/3371113},
+ pages = {45:1--45:32},
+ year = {2020}
+}
diff --git a/tex/heaplang.sty b/tex/heaplang.sty
new file mode 100644
index 000000000..4cf01cd5a
--- /dev/null
+++ b/tex/heaplang.sty
@@ -0,0 +1,85 @@
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{heaplang}
+
+\RequirePackage{marvosym}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% CONCRETE LANGUAGE SYNTAX AND SEMANTICS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textlang}[1]{\texttt{#1}}
+
+\newcommand{\ProphId}{\textdom{ProphId}}
+
+\newcommand{\langkw}[1]{\textlang{\bfseries #1}}
+\newcommand{\langv}[1]{\ensuremath{\mathit{#1}}} % Yes, this makes language-level variables look like logic-level variables. but we still distinguish locally bound variables from global definitions.
+\newcommand{\lvar}{\langv{\var}}
+\newcommand{\lvarB}{\langv{\varB}}
+\newcommand{\lvarC}{\langv{\varC}}
+\newcommand{\lvarF}{\langv{f}}
+
+\newcommand{\loc}{\ell}
+\newcommand{\prophid}{p}
+
+\newcommand{\stateHeap}{\textproj{heap}}
+\newcommand{\stateProphs}{\textproj{prophs}}
+
+\newcommand\exprForm{{\langkw{e}}}
+\newcommand\valForm{{\langkw{v}}}
+
+\def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{=} #2 \spac \langkw{in} \spac}
+\def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
+\def\Else{\spac\langkw{else} \spac}
+\def\Ref(#1){\langkw{ref}(#1)}
+\def\Rec#1(#2)={\langkw{rec}\spac{#1}({#2}) \mathrel{=} }
+\def\RecE#1(#2)={\langkw{rec}_\exprForm\spac{#1}({#2}) \mathrel{=} }
+\def\RecV#1(#2)={\langkw{rec}_\valForm\spac{#1}({#2}) \mathrel{=} }
+\def\Skip{\langkw{skip}}
+\def\Assert{\langkw{assert}}
+\def\Inl{\langkw{inl}}
+\def\Inr{\langkw{inr}}
+\def\Fst{\langkw{fst}}
+\def\Snd{\langkw{snd}}
+\def\True{\langkw{true}}
+\def\False{\langkw{false}}
+\def\NewProph{\langkw{newproph}}
+\def\ResolveWith#1at#2to#3{\langkw{resolve}\spac\langkw{with}\spac#1\spac\langkw{at}\spac#2\spac\langkw{to}\spac#3}
+\def\Resolve#1to#2{\langkw{resolve}\spac#1\spac\langkw{to}\spac#2}
+\def\MatchCore#1with#2|#3end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\mid#3\spac\langkw{end}}
+\def\Match#1with#2=>#3|#4=>#5end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}}
+\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
+ \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
+ &\Ra#3\\|&\Ra#5\\%
+ \multicolumn{3}{l}{\langkw{end}#6}%
+ \end{array}}}
+\def\MatchMLL#1with#2=>#3|#4=>#5|#6=>#7end#8{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
+ \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
+ &\Ra#3\\|&\Ra#5\\|&\Ra#7\\%
+ \multicolumn{3}{l}{\langkw{end}#8}%
+ \end{array}}}
+\def\MatchS#1with#2=>#3end{
+ \langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
+
+\newcommand\Alloc{\langkw{Alloc}}
+\newcommand\Free{\langkw{Free}}
+\newcommand\CAS{\langkw{CAS}}
+\newcommand\CmpXchg{\langkw{CmpXchg}}
+\newcommand\Xchg{\langkw{Xchg}}
+\newcommand\FAA{\langkw{FAA}}
+\newcommand\deref{\mathop{!}}
+\let\gets\leftarrow
+
+\newcommand*\Fork[1]{\langkw{fork}\spac\set{#1}}
+
+\newcommand{\fold}{\langkw{fold}\spac}
+\newcommand{\unfold}{\langkw{unfold}\spac}
+
+\newcommand{\HLOp}{\circledcirc}
+\newcommand{\Ptradd}{\mathop{+_{\langkw{l}}}}
+
+\newcommand{\TT}{()}
+\newcommand*\poison{\text{\Biohazard}}
+
+\newcommand\valeq{\cong}
+\newcommand\valne{\ncong}
+\newcommand\litCompareSafe{\textlog{lit\_compare\_safe}}
+\newcommand\valCompareSafe{\textlog{val\_compare\_safe}}
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
new file mode 100644
index 000000000..8b895d129
--- /dev/null
+++ b/tex/heaplang.tex
@@ -0,0 +1,281 @@
+\section{HeapLang}
+\label{sec:heaplang}
+
+So far, we have treated the programming language we work on entirely generically.
+In this section we present the default language that ships with Iris, HeapLang.
+HeapLang is an ML-like languages with a higher-order heap, unstructured concurrency, some common atomic operations, and prophecy variables.
+It is an instance of the language interface (\Sref{sec:language}), so we only define a per-thread small-step operational semantics---the thread-pool semantics are given in in \Sref{sec:language:concurrent}.
+
+\subsection{HeapLang syntax and operational semantics}
+
+The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions} and \Val{} of \emph{values}, is defined as follows:
+\begin{align*}
+\val,\valB \in \Val \bnfdef{}&
+ z \mid
+ \True \mid \False \mid
+ \TT \mid
+ \poison \mid
+ \loc \mid
+ \prophid \mid {}& (z \in \integer, \loc \in \Loc, \prophid \in \ProphId) \\&
+ \RecV\lvarF(\lvar)= \expr \mid
+ (\val,\valB)_\valForm \mid
+ \Inl(\val)_\valForm \mid
+ \Inr(\val)_\valForm \\
+\expr \in \Expr \bnfdef{}&
+ \val \mid
+ \lvar \mid
+ \RecE\lvarF(\lvar)= \expr \mid
+ \expr_1(\expr_2) \mid
+ {}\\ &
+ \HLOp_1 \expr \mid
+ \expr_1 \HLOp_2 \expr_2 \mid
+ \If \expr then \expr_1 \Else \expr_2 \mid
+ {}\\ &
+ (\expr_1,\expr_2)_\exprForm \mid
+ \Fst(\expr) \mid
+ \Snd(\expr) \mid
+ {}\\ &
+ \Inl(\expr)_\exprForm \mid
+ \Inr(\expr)_\exprForm \mid
+ \MatchCore \expr with \expr_1 | \expr_2 end \mid
+ {}\\ &
+ \Alloc(\expr_1,\expr_2) \mid
+ \Free(\expr) \mid
+ \deref \expr \mid
+ \expr_1 \gets \expr_2 \mid
+ \CmpXchg(\expr_1, \expr_2, \expr_3) \mid
+ \Xchg(\expr_1, \expr_2) \mid
+ \FAA(\expr_1, \expr_2) \mid
+ \kern-30ex{}\\ &
+ \Fork \expr \mid
+ \NewProph \mid
+ \ResolveWith \expr_1 at \expr_2 to \expr_3 \\
+\HLOp_1 \bnfdef{}& - \mid \ldots ~~\text{(list incomplete)} \\
+\HLOp_2 \bnfdef{}& + \mid - \mid \Ptradd \mid \mathop{=} \mid \ldots ~~\text{(list incomplete)}
+\end{align*}
+(Note that \langkw{match} contains a literal $|$ that is not part of the BNF but part of HeapLang syntax.)
+
+Recursive abstractions, pairs, and the injections exist both as a value form and an expression form.
+The expression forms will reduce to the value form once all their arguments are values.
+Conceptually, one can think of that as corresponding to ``boxing'' that most functional language implementations do.
+We will leave away the disambiguating subscript when it is clear from the context or does not matter.
+All of this lets us define $\ofval$ as simply applying the value injection (the very first syntactic form of $\Expr$), which makes a lot of things in Coq much simpler.
+$\toval$ is defined recursively in the obvious way.
+
+For our set of states and observations, we pick
+\begin{align*}
+ \loc \ni \Loc \eqdef{}& \integer \\
+ \prophid \ni \ProphId \eqdef{}& \integer \\
+ \sigma \ni \State \eqdef{}& \record{\begin{aligned}
+ \stateHeap:{}& \Loc \fpfn \Val,\\
+ \stateProphs:{}& \pset{\ProphId}
+ \end{aligned}} \\
+ \obs \ni \Obs \eqdef{}& \ProphId \times (\Val \times \Val)
+\end{align*}
+
+The HeapLang operational semantics is defined via the use of \emph{evaluation contexts}:
+\begin{align*}
+\lctx \in \Lctx \bnfdef{}&
+ \bullet \mid \Lctx_{>} \\
+\lctx_{>} \in \Lctx_{>} \bnfdef{}&
+ \expr(\lctx) \mid
+ \lctx (\val) \mid
+ {}\\ &
+ \HLOp_1 \lctx \mid
+ \expr \HLOp_2 \lctx \mid
+ \lctx \HLOp_2 \val \mid
+ \If \lctx then \expr_1 \Else \expr_2 \mid
+ {}\\ &
+ (\expr, \lctx) \mid
+ (\lctx, \val) \mid
+ \Fst(\lctx) \mid
+ \Snd(\lctx) \mid
+ {}\\ &
+ \Inl(\lctx) \mid
+ \Inr(\lctx) \mid
+ \MatchCore \lctx with \expr_1 | \expr_2 end \mid
+ {}\\ &
+ \Alloc(\expr, \lctx) \mid
+ \Alloc(\lctx, \val) \mid
+ \Free(\lctx) \mid
+ \deref \lctx \mid
+ \expr \gets \lctx \mid
+ \lctx \gets \val \mid
+ {}\\ &
+ \CmpXchg(\expr_1, \expr_2, \lctx) \mid
+ \CmpXchg(\expr_1, \lctx, \val_3) \mid
+ \CmpXchg(\lctx, \val_2, \val_3) \mid
+ {}\\ &
+ \Xchg(\expr, \lctx) \mid
+ \Xchg(\lctx, \val) \mid
+ \FAA(\expr, \lctx) \mid
+ \FAA(\lctx, \val) \mid
+ {}\\ &
+ \ResolveWith \expr_1 at \expr_2 to \lctx \mid
+ \ResolveWith \expr_1 at \lctx to \val_3 \mid
+ {}\\ &
+ \ResolveWith \lctx_{>} at \val_2 to \val_3
+\end{align*}
+Note that we use right-to-left evaluation order.
+This means in a curried function call $f(x)(y)$, we know syntactically the arguments will all evaluate before $f$ gets to do anything, which makes specifying curried calls a lot easier.
+
+The \langkw{resolve} evaluation context for the leftmost expression (the nested expression that executes atomically together with the prophecy resolution) is special: it must not be empty; only further nested evaluation contexts are allowed.
+\langkw{resolve} takes care of reducing the expression once the nested contexts are taken care of, and at that point it requires the expression to reduce to a value in exactly one step.
+Hence we define $\Lctx_{>}$ for non-empty evaluation contexts.
+For more details on prophecy variables, see \cite{iris:prophecy}.
+
+This lets us define the primitive reduction relation in terms of a ``head step'' reduction; see \figref{fig:heaplang-reduction-pure} and \figref{fig:heaplang-reduction-impure}.
+Comparison (both for $\CmpXchg$ and the binary comparison operator) is a bit tricky and uses a helper judgment (\figref{fig:heaplang-valeq}).
+Basically, two values can only be compared if at least one of them is ``compare-safe''.
+Compare-safe values are basic literals (integers, Booleans, locations, unit) as well as $\Inl$ and $\Inr$ of those literals.
+The intention of this is to forbid directly comparing large values such as pairs, which could not be done in a single atomic step on a real machine.
+
+\begin{figure}[p]
+\judgment[Per-thread reduction]{\expr_1, \state_1 \step [\vec\obs] \expr_2, \state_2, \vec\expr}
+\begin{mathpar}
+\infer
+ {\expr_1, \state_1 \hstep [\vec\obs] \expr_2, \state_2, \vec\expr}
+ {\fillctx\lctx[\expr_1], \state_1 \step[\vec\obs] \fillctx\lctx[\expr_2], \state_2, \vec\expr}
+\end{mathpar}
+
+\judgment[``Head'' reduction (pure)]{\expr_1, \state_1 \hstep [\vec\obs] \expr_2, \state_2, \vec\expr}
+\newcommand\alignheader{\kern-30ex}
+\begin{align*}
+&\alignheader\textbf{``Boxing'' reductions} \\
+(\RecE\lvarF(\lvar)= \expr, \state) \hstep[\nil]{}&
+ (\RecV\lvarF(\lvar)= \expr, \state, \nil) \\
+((\val_1, \val_2)_\exprForm, \state) \hstep[\nil]{}&
+ ((\val_1, \val_2)_\valForm, \state, \nil) \\
+(\Inl(\val)_\exprForm, \state) \hstep[\nil]{}&
+ (\Inl(\val)_\valForm, \state, \nil) \\
+(\Inr(\val)_\exprForm, \state) \hstep[\nil]{}&
+ (\Inr(\val)_\valForm, \state, \nil) \\
+&\alignheader\textbf{Pure reductions} \\
+((\RecV\lvarF(\lvar)= \expr)(\val), \state) \hstep[\nil]{}&
+ (\subst {\subst \expr \lvarF {(\Rec\lvarF(\lvar)= \expr)}} \lvar \val, \state, \nil) \\
+(-_{\HLOp} z, \state) \hstep[\nil]{}&
+ (-z, \state, \nil) \\
+(z_1 +_{\HLOp} z_2, \state) \hstep[\nil]{}&
+ (z_1 + z_2, \state, \nil) \\
+(z_1 -_{\HLOp} z_2, \state) \hstep[\nil]{}&
+ (z_1 - z_2, \state, \nil) \\
+(\loc \Ptradd z, \state) \hstep[\nil]{}&
+ (\loc + z, \state, \nil) \\
+(\val_1 =_{\HLOp} \val_2, \state) \hstep[\nil]{}&
+ (\True, \state, \nil)
+ &&\text{if $\val_1 \valeq \val_2$} \\
+(\val_1 =_{\HLOp} \val_2, \state) \hstep[\nil]{}&
+ (\False, \state, \nil)
+ &&\text{if $\val_1 \valne \val_2$} \\
+(\If \True then \expr_1 \Else \expr_2, \state) \hstep[\nil]{}&
+ (\expr_1, \state, \nil) \\
+(\If \False then \expr_1 \Else \expr_2, \state) \hstep[\nil]{}&
+ (\expr_2, \state, \nil) \\
+(\Fst((\val_1, \val_2)_\valForm), \state) \hstep[\nil]{}&
+ (\val_1, \state, \nil) \\
+(\Snd((\val_1, \val_2)_\valForm), \state) \hstep[\nil]{}&
+ (\val_2, \state, \nil) \\
+(\MatchCore \Inl(\val)_\valForm with \expr_1 | \expr_2 end, \state) \hstep[\nil]{}&
+ (\expr_1(\val), \state, \nil) \\
+(\MatchCore \Inr(\val)_\valForm with \expr_1 | \expr_2 end, \state) \hstep[\nil]{}&
+ (\expr_2(\val), \state, \nil)
+\end{align*}
+\caption{HeapLang pure and boxed reduction rules. \\ \small
+The $\HLOp$ subscript indicates that this is the HeapLang operator, not the mathematical operator.}
+\label{fig:heaplang-reduction-pure}
+\end{figure}
+
+\begin{figure}
+\judgment[``Head'' reduction (impure)]{\expr_1, \state_1 \hstep [\vec\obs] \expr_2, \state_2, \vec\expr}
+\newcommand\alignheader{\kern-30ex}
+\begin{align*}
+&\alignheader\textbf{Heap reductions} \\
+(\Alloc(z, \val), \state) \hstep[\nil]{}&
+ (\loc, \mapinsert {[\loc,\loc+z)} \val {\state:\stateHeap}, \nil)
+ &&\text{if $z>0$ and \(\All i<z. \state.\stateHeap(\loc+i) = \bot\)} \\
+(\Free(\loc), \state) \hstep[\nil]{}&
+ ((), \mapinsert \loc \bot {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\deref\loc, \state) \hstep[\nil]{}&
+ (\val, \state, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\loc\gets\valB, \state) \hstep[\nil]{}&
+ (\TT, \mapinsert \loc \valB {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\CmpXchg(\loc,\valB_1,\valB_2), \state) \hstep[\nil]{}&
+ ((\val, \True), \mapinsert\loc{\valB_2}{\state:\stateHeap}, \nil)
+ &&\text{if $\state.\stateHeap(l) = \val$ and $\val \valeq \valB_1$} \\
+(\CmpXchg(\loc,\valB_1,\valB_2), \state) \hstep[\nil]{}&
+ ((\val, \False), \state, \nil)
+ &&\text{if $\state.\stateHeap(l) = \val$ and $\val \valne \valB_1$} \\
+(\Xchg(\loc, \valB) \hstep[\nil]{}&
+ (\val, \mapinsert \loc \valB {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\FAA(\loc, z_2) \hstep[\nil]{}&
+ (z_1, \mapinsert \loc {z_1+z_2} {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = z_1$} \\
+&\alignheader\textbf{Special reductions} \\
+(\Fork\expr, \state) \hstep[\nil]{}&
+ (\TT, \state, \expr) \\
+(\NewProph, \state) \hstep[\nil]{}&
+ (\prophid, \state:\stateProphs \uplus \set{\prophid}, \nil)
+ &&\text{if $\prophid \notin \state.\stateProphs$}
+\end{align*}
+\begin{mathpar}
+\infer
+ {(\expr, \state) \hstep[\vec\obs] (\val, \state', \vec\expr')}
+ {(\ResolveWith \expr at \prophid to \valB, \state) \hstep[\vec\obs \dplus [(\prophid, (\val, \valB))]] (\val, \state', \vec\expr')}
+\end{mathpar}
+\caption{HeapLang impure reduction rules. \\ \small
+Here, $\state:\stateHeap$ denotes $\sigma$ with the $\stateHeap$ field updated as indicated.
+$[\loc,\loc+z)$ in the $\Alloc$ rule indicates that we update all locations in this (left-closed, right-open) interval.}
+\label{fig:heaplang-reduction-impure}
+\end{figure}
+
+\begin{figure}
+\judgment[Value (in)equality]{\val \valeq \valB, \val \valne \valB}
+\begin{align*}
+ \val \valeq \valB \eqdef{}& \val = \valB \land (\valCompareSafe(\val) \lor \valCompareSafe(\valB)) \\
+ \val \valne \valB \eqdef{}& \val \ne \valB \land (\valCompareSafe(\val) \lor \valCompareSafe(\valB))
+\end{align*}
+\begin{mathpar}
+ \axiom{\litCompareSafe(z)}
+
+ \axiom{\litCompareSafe(\True)}
+
+ \axiom{\litCompareSafe(\False)}
+
+ \axiom{\litCompareSafe(\loc)}
+
+ \axiom{\litCompareSafe(\TT)}
+
+\\
+
+ \infer
+ {\litCompareSafe(\val)}
+ {\valCompareSafe(\val)}
+
+ \infer
+ {\litCompareSafe(\val)}
+ {\valCompareSafe(\Inl(\val))}
+
+ \infer
+ {\litCompareSafe(\val)}
+ {\valCompareSafe(\Inr(\val))}
+\end{mathpar}
+\caption{HeapLang value comparison judgment.}
+\label{fig:heaplang-valeq}
+\end{figure}
+
+\subsection{Syntactic sugar}
+
+We recover many of the common language operations as syntactic sugar.
+\begin{align*}
+ \Lam \lvar. \expr \eqdef{}& \Rec\any(\lvar)= \expr \\
+ \Let \lvar = \expr in \expr' \eqdef{}& (\Lam \lvar. \expr')(\expr) \\
+ \expr; \expr' \eqdef{}& \Let \any = \expr in \expr' \\
+ \Skip \eqdef{}& \TT; \TT \\
+ \Ref(\expr) \eqdef{}& \Alloc(1,\expr) \\
+ \CAS(\expr_1, \expr_2, \expr_3) \eqdef{}& \Snd(\CmpXchg(\expr_1, \expr_2, \expr_3)) \\
+ \Resolve \expr_1 to \expr_2 \eqdef{}& \ResolveWith \Skip at \expr_1 to \expr_2
+\end{align*}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End:
diff --git a/tex/iris.sty b/tex/iris.sty
index 7d29b2905..1fb20fc65 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -31,6 +31,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nat}{\mathbb{N}}
+\newcommand{\integer}{\mathbb{Z}}
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} % big-star
\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
diff --git a/tex/iris.tex b/tex/iris.tex
index 0895f76fb..0631f53da 100644
--- a/tex/iris.tex
+++ b/tex/iris.tex
@@ -27,7 +27,7 @@
This document describes formally the Iris program logic.
Every result in this document has been fully verified in Coq.
The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/iris/iris}.
-For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
+For further information, visit the Iris project website at \url{https://iris-project.org}.
\end{abstract}
\clearpage\begingroup
@@ -69,6 +69,9 @@ For a list of changes in Iris since then, please consult our changelog at \url{h
\input{paradoxes}
\endgroup
\clearpage\begingroup
+\input{heaplang}
+\endgroup
+\clearpage\begingroup
\printbibliography
\endgroup
diff --git a/tex/language.tex b/tex/language.tex
index 88c6e9275..4096960c4 100644
--- a/tex/language.tex
+++ b/tex/language.tex
@@ -46,6 +46,7 @@ Otherwise, we need strong atomicity.
\end{defn}
\subsection{Concurrent Language}
+\label{sec:language:concurrent}
For any language $\Lang$, we define the corresponding thread-pool semantics.
diff --git a/tex/setup.tex b/tex/setup.tex
index f7b3d1b09..3a3bc63ce 100644
--- a/tex/setup.tex
+++ b/tex/setup.tex
@@ -18,6 +18,7 @@
\usepackage{\basedir pftools}
\usepackage{\basedir iris}
+\usepackage{\basedir heaplang}
\usepackage{xcolor} % for print version
--
GitLab