From 0876cbadf31a5f72b81fcd55f60023ceda43b781 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 15:26:35 +0100
Subject: [PATCH] docs: one-shot
---
docs/constructions.tex | 30 ++++++++++++++++++++++++++++++
docs/iris.sty | 7 ++++++-
2 files changed, 36 insertions(+), 1 deletion(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 7a08fa78c..b780efec9 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -32,6 +32,36 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\axiomH{ag-agree}{\ag(x) \mtimes \ag(y) \in \mval_n \Ra x \nequiv{n} y}
\end{mathpar}
+\subsection{One-shot}
+
+The purpose of the one-shot CMRA is to lazily initialize the state of a ghost location.
+Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
+\begin{align*}
+ \monoid \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\
+ \mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n}
+\end{align*}
+\begin{align*}
+ \mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
+ \mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot
+\end{align*}
+\begin{align*}
+ \osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\
+ \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
+ \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
+\end{align*}
+The remaining cases of composition go to $\bot$.
+The step-indexed equivalence is inductively defined as follows:
+\begin{mathpar}
+ \axiom{\ospending \nequiv{n} \ospending}
+
+ \infer{\melt \nequiv{n} \meltB}{\osshot(\melt) \nequiv{n} \osshot(\meltB)}
+
+ \axiom{\munit \nequiv{n} \munit}
+
+ \axiom{\bot \nequiv{n} \bot}
+\end{mathpar}
+$\oneshotm(-)$ is a locally non-expansive bifunctor from $\CMRAs$ to $\CMRAs$.
+
% \subsection{Exclusive monoid}
diff --git a/docs/iris.sty b/docs/iris.sty
index 0c73ddd27..7692ff235 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -335,7 +335,12 @@
\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}
-%% STSs
+% One-Shot
+\newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}}
+\newcommand{\ospending}{\textlog{pending}}
+\newcommand{\osshot}{\textlog{shot}}
+
+% STSs
\newcommand{\STSCtx}{\textlog{StsCtx}}
\newcommand{\STSSt}{\textlog{StsSt}}
\newcommand{\STSS}{\mathcal{S}} % states
--
GitLab