From ffc87705817e42a5d3acaf5f7ca4603ba0cf921a Mon Sep 17 00:00:00 2001
From: Hai Dang <dhhai.uns@gmail.com>
Date: Mon, 2 May 2016 15:01:49 +0200
Subject: [PATCH] first RSL typed up, with rel write and acq read
---
.gitignore | 2 +
rsl/basic.tex | 81 ++++++++
rsl/cas.tex | 114 ++++++++++++
rsl/mathpartir.sty | 446 +++++++++++++++++++++++++++++++++++++++++++++
rsl/relacq.tex | 354 +++++++++++++++++++++++++++++++++++
rsl/rsl.tex | 47 +++++
rsl/rsldef.tex | 34 ++++
7 files changed, 1078 insertions(+)
create mode 100644 rsl/basic.tex
create mode 100644 rsl/cas.tex
create mode 100644 rsl/mathpartir.sty
create mode 100644 rsl/relacq.tex
create mode 100644 rsl/rsl.tex
create mode 100644 rsl/rsldef.tex
diff --git a/.gitignore b/.gitignore
index 32820925..4aabc258 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
+.DS_Store
+
*.log
*.aux
*.fdb_latexmk
diff --git a/rsl/basic.tex b/rsl/basic.tex
new file mode 100644
index 00000000..6ba380ae
--- /dev/null
+++ b/rsl/basic.tex
@@ -0,0 +1,81 @@
+\section{Basics}
+
+We assume Layer 1 from Janno's encoding of GPS. This means that we assume the
+strong release-acquire fragment of C11, that is reads are acquire, writes are
+release, read-modify-writes are release-acquire (no relax operations). \TODO what about non-atomics?
+
+\paragraph{Buffer-monotonicity} All RSL assertions must be buffer-monotone, that is
+
+\begin{align*}
+ \intr {P}(\buf) \implies \All \buf' \bsup \buf. \intr {P}(\buf') \\
+\end{align*}
+
+\paragraph{RSL rule interpretation} Same as GPS interpretation.
+
+\begin{mathpar}
+ \iinferH{}{H_1 \and \ldots \and H_n}{P} \and \eqdef \and
+ \cinferH{}{\All \buf.}{\intr{H_1}(\buf) \and \ldots \and \intr{H_2}(\buf)}{\intr P (\buf)}
+\end{mathpar}
+%
+\paragraph{RSL triple interpretation} Same as GPS interpretation.
+%
+\begin{align*}
+ \intr{\hoare{P}e{\Ret \val. Q}} (\buf) \eqdef& \;
+ \All \proc. \hoare{\bseen{\proc}{\buf} \ast \intr P(\buf)}
+ {e,\proc}
+ {\Ret\val. \Exists \buf' \bsup \buf.
+ \bseen{\proc}{\buf'} \ast \intr {Q}(\buf')} \\
+\end{align*}
+%
+\paragraph{Init} The current buffer has observed the initialization of $\loc$.
+$\linit{\loc}$ is buffer-monotone and duplicable.
+%
+\begin{align*}
+ \intr{\linit{\loc}}(\buf) \eqdef& \;
+ \Exists \val, \ts. (\loc, \val, \ts) \in \buf \\
+\end{align*}
+
+\begin{mathpar}
+ \inferH{Init-Split}{}{\linit{\loc} \Lra \linit{\loc} \ast \linit{\loc}} \\
+\end{mathpar}
+%
+\subsection{Basic rules}
+We depend on the following rules in Layer 1 (in Iris) for the encoding:
+%
+\begin{mathpar}
+ \inferH{AtomicRead}{}{\ereadHyp \vdash
+ \hoare{\lhist{\loc}{\hist}}
+ {\eload{\acq}{\loc}, \proc}
+ {\begin{aligned}
+ \Ret\val. &\;
+ \lhist{\loc}{\hist} \ast \Exists \buf_0 \in \hist.
+ \Exists \buf' \bsup (\buf \cup \buf_0). \bseen{\proc}{\buf'} \\
+ &\; \ast \Exists \ts' \ge \ts. \mr{\buf'}{(\loc, \val, \ts')}
+ \ast \head(\buf_0) = (\loc,\val,\ts')
+ \end{aligned}
+ }
+ } \\
+ \and\inferH{AtomicWrite}{}{\estoreHyp \vdash \hoare{\estorePreB
+ }{\estore{\rel}{\loc}{\val}, \proc}{\estorePostB}} \\
+ \and\inferH{CAS}{}{
+ \intr{\linit{\loc}}(\buf) \vdash
+ \ahoare{\ecasPreB}
+ {\ecas{\loc}{\val_o}{\val_n}, \proc}
+ {\Ret\val'.
+ \begin{aligned}
+ &\; \Exists \buf' \bsup \buf. \bseen{\proc}{\buf}
+ \ast \Exists \hist'. \lhist{\loc}{\hist'}
+ \ast \val' = \head^2(\hist).\weval \ast{} \\
+ &\; (\val' = \val_0 \ast h' = \buf' :: \hist \ast \buf' \bsup \head(\hist)) \\
+ \lor &\; (\val' \neq \val_0 \ast h' = \hist \ast \buf' \bsup \head(\hist)) \\
+ \end{aligned} }
+ } \\
+\end{mathpar}
+
+%
+%
+%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rsl"
+%%% End:
diff --git a/rsl/cas.tex b/rsl/cas.tex
new file mode 100644
index 00000000..9b89bb43
--- /dev/null
+++ b/rsl/cas.tex
@@ -0,0 +1,114 @@
+\section{Adding CAS}
+
+We want to support the following additional rules:
+
+\begin{mathpar}
+ \inferH{CAS*}
+ { P \Ra \linit{\loc} \ast \rmwp{\loc}{Q} \\\\
+ P \ast Q(\val) \Ra \relp{\loc}{Q'} \ast Q'(\val') * R\subst{y}{\val}\\\\
+ \hoare{P}{\eload{\acq}{\loc}}{\Ret y. y \neq \val \Ra R}}
+ { \hoare{P}
+ {\ecas{\loc}{\val}{\val'}}
+ {\Ret y. R}} \\
+ \and
+ \inferH{RMW-Split}{}{
+ \rmwp{\loc}{Q} \ast \rmwp{\loc}{Q} \Lra \rmwp{\loc}{Q}} \\
+ \and
+ \inferH{RMW-Acq-Split}{\All \val. Q'(\val) = \top \lor Q(\val) = Q'(\val) = \bot}{
+ \rmwp{\loc}{Q} \Lra \rmwp{\loc}{Q} \ast \acqp{\loc}{Q'}}\\
+ \and
+ \inferH{A-M}{}{
+ \hoare{\top}{\ealloc{}}{\Ret \loc. \relp{\loc}{Q} \ast \rmwp{\loc}{Q}}}\\
+\end{mathpar}
+
+\subsection{Protocol for RMW}
+
+\begin{align*}
+ \mSlP{T}{\loc}{P}.\STSS \; \eqdef& \;
+ \setComp{\sUninitTok{\splset}{i}}{\splset \in \Splset} \\
+ &\; \cup \setComp{\sVSsplitTok{\splset}{\hist}{i}}{
+ \begin{aligned}
+ &\; \splset \in \Splset \land \hist \in \List(\Buf) \\
+ \land &\; \All \buf \in \hist. \mr{b}{(\loc,\_,\_)}
+ \end{aligned}
+ } \\
+ \\
+ \mSlP{T}{\loc}{P}.\ststrans \; \eqdef& \;
+ \set{(\sUninit{\splset},\sUninit{\splset'})} &\; \text{split/join} \\
+ &\; \cup \set{(\sUninit{\splset},(\splset,[\buf]))} &\; \text{first write} \\
+ &\; \cup \setComp{((\splset,\hist),(\splset',\hist))}{...} &\;
+ \text{split/join} \\
+ &\; \cup \setComp{((\splset,\hist),(\splset,\hist))}{...} &\;
+ \text{read/CAS fails} \\
+ &\; \cup \set{((\splset,\hist),(\splset,\buf :: \hist))} &\;
+ \text{write/CAS succeeds} \\
+\end{align*}
+%
+\subsection{Extended interpretation}
+\begin{align*}
+ \resst{\loc}{P}{Q}{\splset} \; \eqdef& \;
+ \bigast_{i \in \splset} i \Mapsto Q(i) \ast
+ \All i \in \splset, \val_\loc, \buf.
+ \intr{Q(i)(\val_\loc)}(\buf) = \top \lor
+ \intr{P(\val_\loc)}(\buf) = \intr{Q(i)(\val_\loc)}(\buf) = \bot\\
+ \intlPs{\psi}{\loc}{P}{\sUninit{\splset}} \; \eqdef& \;
+ \lhist{\loc}{\nil} \ast \Exists Q. \resst{\loc}{P}{Q}{\splset} \\
+ \intlPs{\psi}{\loc}{P}{(\splset, \hist)} \; \eqdef& \;
+ \lhist{\loc}{\hist} \ast \Exists Q. \resst{\loc}{P}{Q}{\splset_1}
+ \ast \intr{P(\head(\hist).\weval)}(\head(\hist)) \\
+ \\
+ \intr{\relp{\loc}{Q}}(\_) \; \eqdef& \;
+ \Exists P, \iname, \gname.
+ \always \later \big(\All \val_\loc, \buf.
+ \intr{Q(\val_\loc)}(\buf) \Ra \intr{P(\val_\loc)}(\buf) \big) \\
+ & \; \quad \ast
+ (\STS(\mSlP{S}{\loc}{P}, \intlP{\varphi}{\loc}{P},\gname,\iname) \lor
+ \STS(\mSlP{T}{\loc}{P}, \intlP{\psi}{\loc}{P},\gname,\iname)) \\
+ \intr{\acqp{\loc}{R}}(\_) \; \eqdef& \;
+ \Exists P, \iname, \gname, \stsstate, i, Q_i.
+ i \Mapsto Q_i
+ \ast \always \later \big(\All \val_\loc, \buf.
+ \intr{Q_i(\val_\loc)}(\buf) \Ra \intr{R(\val_\loc)}(\buf) \big) \\
+ & \; \quad \ast
+ (\Exists \stsstate.
+ \STS(\mSlP{S}{\loc}{P}, \intlP{\varphi}{\loc}{P},\gname,\iname)　
+ \ast \ownGhost{\gamma}{\authfrag \stsstate;[C_i]}) \lor
+ (\Exists \stsstate.
+ \STS(\mSlP{T}{\loc}{P}, \intlP{\psi}{\loc}{P},\gname,\iname)　
+ \ast \ownGhost{\gamma}{\authfrag \stsstate;[C_i]}) \\
+ \intr{\rmwp{\loc}{P}}(\_) \; \eqdef& \;
+ \Exists \iname, \gname. \STS(\mSlP{T}{\loc}{P}, \intlP{\psi}{\loc}{P},\gname,\iname) \\
+\end{align*}
+
+Release, acquire and RMW permissions are all buffer-independent.
+
+Note that $\STS(\mSlP{S}{\loc}{\_}, \_, \_, \_) \ast \STS(\mSlP{T}{\loc}{\_}, \_, \_, \_) \vs \bot$,
+since $\lhist{\loc}{\_}$ is not duplicable.
+
+\subsection{Proofs}
+
+\subsubsection{\ruleref{W-Rel}}
+
+\subsubsection{\ruleref{R-Acq}}
+
+\subsubsection{\ruleref{CAS*}}
+
+\subsubsection{\ruleref{Rel-Split}}
+
+\subsubsection{\ruleref{Acq-Split}}
+
+\subsubsection{\ruleref{RMW-Split}}
+
+\subsubsection{\ruleref{RMW-Acq-Split}}
+
+\subsubsection{\ruleref{A-R}}
+
+\subsubsection{\ruleref{A-M}}
+
+%
+%
+%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rsl"
+%%% End:
diff --git a/rsl/mathpartir.sty b/rsl/mathpartir.sty
new file mode 100644
index 00000000..7d2234ad
--- /dev/null
+++ b/rsl/mathpartir.sty
@@ -0,0 +1,446 @@
+% Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
+%
+% Author : Didier Remy
+% Version : 1.2.0
+% Bug Reports : to author
+% Web Site : http://pauillac.inria.fr/~remy/latex/
+%
+% Mathpartir is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2, or (at your option)
+% any later version.
+%
+% Mathpartir is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details
+% (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+ [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+ \edef \MathparNormalpar
+ {\noexpand \lineskiplimit \the\lineskiplimit
+ \noexpand \lineskip \the\lineskip}%
+ }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0pt}%0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+ {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+ \let \and \mpr@andcr
+ \let \par \mpr@andcr
+ \let \\\mpr@cr
+ \let \eqno \mpr@eqno
+ \let \hva \mpr@hva
+ }
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+ {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+ \noindent $\displaystyle\fi
+ \MathparBindings}
+ {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+\newenvironment{mathparpagebreakable}[1][]
+ {\begingroup
+ \par
+ \mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \mpr@prebindings \mpr@paroptions #1%
+ \vskip \abovedisplayskip \vskip -\lineskip%
+ \ifmmode \else $\displaystyle\fi
+ \MathparBindings
+ }
+ {\unskip
+ \ifmmode $\fi \par\endgroup
+ \vskip \belowdisplayskip
+ \noindent
+ \ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
+ \vbox \bgroup \tabskip 0em \let \\ \cr
+ \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+ \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+ \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+ \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+ \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
+ \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+ \mpr@flatten \mpr@all \mpr@to \mpr@one
+ \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+ \mpr@all \mpr@stripend
+ \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+ \ifx 1\mpr@isempty
+ \repeat
+}
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+ \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+%% Part III -- Type inference rules
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+ \setbox \mpr@hlist
+ \hbox {\strut
+ \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+ \unhbox \mpr@hlist}%
+ \setbox \mpr@vlist
+ \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+ \else \unvbox \mpr@vlist \box \mpr@hlist
+ \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+% \setbox \mpr@hlist
+% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+% \setbox \mpr@vlist
+% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+% \else \unvbox \mpr@vlist \box \mpr@hlist
+% \fi}%
+% }
+
+\def \mpr@item #1{$\displaystyle #1$}
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+ \bgroup
+ \ifx #1T\@premissetrue
+ \else \ifx #1B\@premissefalse
+ \else
+ \PackageError{mathpartir}
+ {Premisse orientation should either be T or B}
+ {Fatal error in Package}%
+ \fi \fi
+ \def \@test {#2}\ifx \@test \mpr@blank\else
+ \setbox \mpr@hlist \hbox {}%
+ \setbox \mpr@vlist \vbox {}%
+ \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+ \let \@hvlist \empty \let \@rev \empty
+ \mpr@tmpdim 0em
+ \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+ \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+ \def \\##1{%
+ \def \@test {##1}\ifx \@test \empty
+ \mpr@htovlist
+ \mpr@tmpdim 0em %%% last bug fix not extensively checked
+ \else
+ \setbox0 \hbox{\mpr@item {##1}}\relax
+ \advance \mpr@tmpdim by \wd0
+ %\mpr@tmpdim 1.02\mpr@tmpdim
+ \ifnum \mpr@tmpdim < \hsize
+ \ifnum \wd\mpr@hlist > 0
+ \if@premisse
+ \setbox \mpr@hlist
+ \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+ \else
+ \setbox \mpr@hlist
+ \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
+ \fi
+ \else
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \else
+ \ifnum \wd \mpr@hlist > 0
+ \mpr@htovlist
+ \mpr@tmpdim \wd0
+ \fi
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \advance \mpr@tmpdim by \mpr@sep
+ \fi
+ }%
+ \@rev
+ \mpr@htovlist
+ \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+ \fi
+ \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+ \let\@@over\over % fallback if amsmath is not loaded
+ \let\@@overwithdelims\overwithdelims
+ \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+ \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+ }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+ \def \mpr@tail{#1}%
+ \def \mpr@body{#2}%
+ \def \mpr@head{#3}%
+ \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+ \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+ \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
+ \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
+ \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
+ \setbox0=\hbox {$\box1 \@@atop \box2$}%
+ \dimen0=\wd0\box0
+ \box0 \hskip -\dimen0\relax
+ \hbox to \dimen0 {$%
+ \mathrel{\mpr@tail}\joinrel
+ \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+ $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+ {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\def \mpr@@reduce #1#2{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+ {\bgroup
+ \ifnum \linewidth<\hsize \hsize \linewidth\fi
+ \mpr@rulelineskip
+ \let \and \qquad
+ \let \hva \mpr@hva
+ \let \@rulename \mpr@empty
+ \let \@rule@options \mpr@empty
+ \let \mpr@over \@@over
+ \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+ {\everymath={\displaystyle}%
+ \def \@test {#2}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+ \else
+ \def \@test {#3}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+ \else
+ \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+ \fi \fi
+ \def \@test {#1}\ifx \@test\empty \box0
+ \else \vbox
+%%% Suggestion de Francois pour les etiquettes longues
+%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+ {\hbox {\RefTirName {#1}}\box0}\fi
+ \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible,
+% and vertical breaks if needed.
+%
+% An empty element obtained by \\\\ produces a vertical break in all cases.
+%
+% The former rule is aligned on the fraction bar.
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+%
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%
+% width set the width of the rule to val
+% narrower set the width of the rule to val\hsize
+% before execute val at the beginning/left
+% lab put a label [Val] on top of the rule
+% lskip add negative skip on the right
+% left put a left label [Val]
+% Left put a left label [Val], ignoring its width
+% right put a right label [Val]
+% Right put a right label [Val], ignoring its width
+% leftskip skip negative space on the left-hand side
+% rightskip skip negative space on the right-hand side
+% vdots lift the rule by val and fill vertical space with dots
+% after execute val at the end/right
+%
+% Note that most options must come in this order to avoid strange
+% typesetting (in particular leftskip must preceed left and Left and
+% rightskip must follow Right or right; vdots must come last
+% or be only followed by rightskip.
+%
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+ {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+ {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+ \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+ \setbox \mpr@right \hbox{}%
+ $\setkeys{mpr}{#1}%
+ \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+ \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+ \box \mpr@right \mpr@vdots$}
+ \setbox1 \hbox {\strut}
+ \@tempdima \dp0 \advance \@tempdima by -\dp1
+ \raise \@tempdima \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode
+ \let \@do \mpr@inferstar@
+ \else
+ \let \@do \mpr@err@skipargs
+ \PackageError {mathpartir}
+ {\string\inferrule* can only be used in math mode}{}%
+ \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \TirNameStyle #1{\small \textsc{#1}}
+\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
+\let \TirName \tir@name
+\let \DefTirName \TirName
+\let \RefTirName \TirName
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
diff --git a/rsl/relacq.tex b/rsl/relacq.tex
new file mode 100644
index 00000000..f1a2725f
--- /dev/null
+++ b/rsl/relacq.tex
@@ -0,0 +1,354 @@
+\section{Release-Acquire Fragment}
+
+\subsection{Per-location protocol}
+%
+We have an Iris invariant to enforce a protocol on each location $\loc$.
+The protocol supports RSL rules (allocation, release write,
+acquire read, split, etc.). CAS is added in the next section.
+%
+\begin{align*}
+ \mSlP{S}{\loc}{P}.\STSS \; \eqdef& \;
+ \setComp{\sUninitTok{\splset}{i}}{\splset \in \Splset} \\
+ &\; \cup \setComp{\sVsplitTok{\splset_1}{\splset_2}{\hist}{i}}{
+ \begin{aligned}
+ &\; \splset_1, \splset_2 \in \Splset
+ \land \splset_2 \subseteq \splset_1 \\
+ \land &\; \hist \in \List(\Buf) \\
+ \land &\; \All \buf \in \hist. \mr{b}{(\loc,\_,\_)}
+ \end{aligned}
+ } \\
+ \\
+ \mSlP{S}{\loc}{P}.\ststrans \; \; \eqdef& \;
+ \set{(\sUninit{\splset},\sUninit{\splset'})} &\; \text{split/join} \\
+ &\; \cup \set{(\sUninit{\splset},(\splset,\splset,[\buf]))} &\; \text{first write} \\
+ &\; \cup \setComp{((\splset_1,\splset_2,\hist),(\splset'_1,\splset'_2,\hist))}{...} &\;
+ \text{split/join} \\
+ &\; \cup \setComp{((\splset_1,\splset_2,\hist),(\splset'_1,\splset'_2,\hist))}{...} &\;
+ \text{read} \\
+ &\; \cup \set{((\splset_1,\splset_2,\hist),(\splset_1,\splset_2,\buf :: \hist))} &\;
+ \text{write} \\
+ \\
+ \ress{\loc}{P}{Q}{\splset} \; \eqdef& \;
+ \bigast_{i \in \splset} i \Mapsto Q(i) \ast
+ \always \later \big(\All \val_\loc, \buf.
+ \intr{P(\val_\loc)}(\buf) \Lra
+ \bigast_{i \in \splset} \intr{Q(i)(\val_\loc)}(\buf)
+ \big) \\
+ \intlPs{\varphi}{\loc}{P}{\sUninit{\splset}} \; \eqdef& \;
+ \lhist{\loc}{\nil} \ast \Exists Q. \ress{\loc}{P}{Q}{\splset} \\
+ \intlPs{\varphi}{\loc}{P}{(\splset_1, \splset_2, \hist)} \; \eqdef& \;
+ \lhist{\loc}{\hist} \ast \Exists Q. \ress{\loc}{P}{Q}{\splset_1}
+ \ast \bigast_{\buf \in \hist} \bigast_{i \in \splset_2}
+ \later \intr{Q(i)(\buf.\weval)}(\buf) \\
+\end{align*}
+
+$\splset$ in $\sUninit{\splset}$ and $\splset_1$ in $(\splset_1,\splset_2,\hist)$
+are sets of names of the \emph{exact partition} of $P$ for all possible values
+of $\loc$. $\splset_2$ contains names of parts of the partition available to read.
+$C_i$ where $i \in \splset_2$ is the permission to read and split the $Q(i)$ part.
+
+\begin{align*}
+ \intr{\relp{\loc}{Q}}(\_)\eqdef& \;
+ \Exists P, \iname, \gname. \STS(\mSlP{S}{\loc}{P}, \intlP{\varphi}{\loc}{P},\gname,\iname)
+ \ast \always \later \big(\All \val_\loc, \buf.
+ \intr{Q(\val_\loc)}(\buf) \Ra \intr{P(\val_\loc)}(\buf) \big) \\
+ \intr{\acqp{\loc}{R}}(\_) \eqdef& \;
+ \Exists P, \iname, \gname, \stsstate, i, Q_i.
+ \STS(\mSlP{S}{\loc}{P}, \intlP{\varphi}{\loc}{P},\gname,\iname)
+ \ast i \Mapsto Q_i \ast \ownGhost{\gamma}{\authfrag \stsstate;[C_i]} \\
+ & \; \qquad \ast \always \later \big(\All \val_\loc, \buf.
+ \intr{Q_i(\val_\loc)}(\buf) \Ra \intr{R(\val_\loc)}(\buf) \big) \
+\end{align*}
+
+Release and acquire permissions are clearly \emph{buffer-indepedent}, therefore
+buffer-monotone.
+
+%
+\subsection{Reads reduce to splits}
+\label{sec:readsplit}
+
+After reading $\val_0$, in order to obtain $\intr{Q(i)(\val_0)}(\buf)$
+for some $\buf$, one needs the token $C_i$ (which means $i \in \splset_2$, so
+one can actually get $\intr{Q(i)(\val_0)}(b)$), splits $Q(i)$ into $Q(i_1)$ and
+$Q(i_2)$ where
+
+\begin{align*}
+ Q(i_1) \eqdef& \;
+ \Lam \val \Lam \buf. \eif v == v_0 \ethen \top \eelse \intr{Q(i)(v)}(b)\\
+ Q(i_2) \eqdef& \;
+ \Lam \val \Lam \buf. \eif v == v_0 \ethen \intr{Q(i)(v)}(b) \eelse \top \\
+\end{align*}
+
+One then can update $\splset_2$ to $\splset'_2 = \splset_2 \setminus \set{i} \uplus \set{i_1}$
+(and $\splset_1$ to $\splset'_1 = I_2 \setminus \set{i} \uplus \set{i_1,i_2}$),
+obtain $\intr{Q(i_2)(\val_0)}(\buf) \equiv \intr{Q(i)(\val_0)}(\buf)$, and
+return only $C_{i_1}$ and $Q(i_1) \equiv Q(i)[\val:=\top]$ for later reads.
+
+\subsection{RSL rules}
+
+With the interpretations above we can have the following rules:
+
+\begin{mathpar}
+ \inferH{W-Rel}{}{
+ \hoare{\later Q(\val) \ast \relp{\loc}{Q}}
+ {\estore{\rel}{\loc}{\val}}
+ {\linit{\loc} \ast \relp{\loc}{Q}}} \\
+ \and
+ \inferH{R-Acq}{}{
+ \hoare{\linit{\loc} \ast \acqp{\loc}{Q}}
+ {\eload{\acq}{\loc}}
+ {\Ret\val. \later Q(v) \ast \acqp(\loc,Q[\val := \top])}} \\
+ \and
+ \inferH{Rel-Split}{}{
+ \relp{\loc}{Q_1} \ast \relp{\loc}{Q_2}
+ \Lra \relp{\loc}{\Lam \val. Q_1(\val) \lor Q_2(\val)}} \\
+ \and
+ \inferH{Acq-Split}{}{
+ \acqp{\loc}{Q_1} \ast \acqp{\loc}{Q_2}
+ \Lra \acqp{\loc}{\Lam \val. Q_1(\val) \ast Q_2(\val)}}\\
+ \and
+ \inferH{A-R}{}{
+ \hoare{\top}{\ealloc{}}{\Ret \loc. \relp{\loc}{Q} \ast \acqp{\loc}{Q}}}\\
+\end{mathpar}
+
+\subsection{Proofs}
+
+\subsubsection{\ruleref{W-Rel}}
+\begin{hproofenv}
+ Context: $\buf, \proc, \bseen{\proc}{\buf}$~\\
+ \pline[\top]{\later \intr{Q(\val)}(\buf) \ast \intr{\relp{\loc}{Q}}(b)}~\\
+ Context: $P, \iname, \gname, \STS(\mSlP{S}{\loc}{P}, \intlP{\varphi}{\loc}{P},\gname,\iname),
+ \always \later \big(\All \val_\loc, \buf.
+ \intr{Q(\val_\loc)}(\buf) \Ra \intr{P(\val_\loc)}(\buf) \big)$~\\
+ \pline[\top]{\later \intr{Q(\val)}(\buf)}~\\
+ \begin{psubenv}{open $\iname$}
+ Context: $\stsstate, Q' $~\\
+ \begin{psubenv}{$\stsstate = \sUninit{\splset}$}
+ Case: $\stsstate = \sUninit{\splset}, \hist = \nil$~\\
+ \pline[-\set\iname]{\later \intr{Q(\val)}(\buf)
+ \ast \ownGhost{\gname}{\authfull \stsstate}
+ \ast \later \lhist{\loc}{\hist}
+ \ast \later \ress{\loc}{P}{Q'}{\splset}}~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\iname]{\lhist{\loc}{\hist}}~\\
+ \cdline{\estore{\rel}{\loc}{\val}, \proc}~\\
+ \pline[-\set\iname]{\estorePostB} \by ~\ruleref{AtomicWrite}~\\
+ \end{psubenv}~\\
+ Context: $\buf' \bsup \buf$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ &\bseen{\proc}{\buf'}
+ \ast \mr{\buf'}{(\loc,\val,\any)} \\
+ &{} \ast \later \intr{Q(\val)}(\buf)
+ \ast \ownGhost{\gname}{\authfull \stsstate}
+ \ast \later \lhist{\loc}{[\buf']}
+ \ast \later \ress{\loc}{P}{Q'}{\splset}
+ \end{aligned}
+ }~\\
+ Pick $\stsstate' \eqdef (\splset,\splset,[\buf'])$~\\
+ \pline[-\set\iname]{
+ \bseen{\proc}{\buf'}
+ \ast \later \intr{Q(\val)}(\buf)
+ \ast \ownGhost{\gname}{\authfull \stsstate'}
+ \ast \later \lhist{\loc}{[\buf']}
+ \ast \later \ress{\loc}{P}{Q'}{\splset}
+ }~\\
+ Have $\later \intr{Q(\val)}(\buf)
+ \Ra \later\later \bigast_{i \in \splset} \intr{Q'(i)(\val)}(\buf')$
+ \by assm., def. ress, and mono. of $Q'(i)(\val)$~\\
+ \pline[-\set\iname]{
+ \bseen{\proc}{\buf'}
+ \ast \later\later \bigast_{\buf_0 \in [\buf']}\bigast_{i \in \splset} \intr{Q'(i)(\val)}(\buf_0)
+ \ast \ownGhost{\gname}{\authfull \stsstate'}
+ \ast \later \lhist{\loc}{[\buf']}
+ \ast \later \ress{\loc}{P}{Q'}{\splset}
+ }~\\
+ \end{psubenv}~\\
+ \hline
+ \begin{psubenv}{$\stsstate = (\splset_1, \splset_2, \hist)$}
+ Case: $\stsstate = (\splset_1, \splset_2, \hist)$~\\
+ \pline[-\set\iname]{\later \intr{Q(\val)}(\buf)
+ \ast \ownGhost{\gname}{\authfull \stsstate}
+ \ast \later \lhist{\loc}{\hist}
+ \ast \later \ress{\loc}{P}{Q'}{\splset_1}
+ \ast \bigast_{\buf_0 \in \hist} \bigast_{i \in \splset_2}
+ \later\later \intr{Q'(i)(\buf_0.\weval)}(\buf_0)}~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\iname]{\lhist{\loc}{\hist}}~\\
+ \cdline{\estore{\rel}{\loc}{\val}, \proc}~\\
+ \pline[-\set\iname]{\estorePostB} \by ~\ruleref{AtomicWrite}~\\
+ \end{psubenv}~\\
+ Context: $\buf' \bsup \buf$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ &\bseen{\proc}{\buf'}
+ \ast \mr{\buf'}{(\loc,\val,\any)}
+ \ast \later \intr{Q(\val)}(\buf)
+ \ast \ownGhost{\gname}{\authfull \stsstate} \\
+ &{}
+ \ast \later \lhist{\loc}{\buf' :: \hist}
+ \ast \later \ress{\loc}{P}{Q'}{\splset_1}
+ \ast \bigast_{\buf_0 \in \hist} \bigast_{i \in \splset_2}
+ \later\later \intr{Q'(i)(\buf_0.\weval)}(\buf_0)
+ \end{aligned}}~\\
+ Pick $\hist' \eqdef \buf' :: \hist; \stsstate' \eqdef (\splset_1,\splset_2,\hist')$~\\
+ Similarly also have
+ $\later \intr{Q(\val)}(\buf)
+ \Ra \later\later \bigast_{i \in \splset_2} \intr{Q'(i)(\val)}(\buf')$~\\
+ \by assm., def. ress, mono. of $Q'(i)(\val)$, and $\splset_2 \subseteq \splset_1$~\\
+ \pline[-\set\iname]{
+ \bseen{\proc}{\buf'}
+ \ast \ownGhost{\gname}{\authfull \stsstate'}
+ \ast \later \lhist{\loc}{\hist'}
+ \ast \later \ress{\loc}{P}{Q'}{\splset_1}
+ \ast \bigast_{\buf_0 \in \hist'} \bigast_{i \in \splset_2}
+ \later\later \intr{Q'(i)(\buf_0.\weval)}(\buf_0)
+ }~\\
+ \end{psubenv}~\\
+ Context: $(\loc,\any,\any)\in \buf'$~\\
+ \end{psubenv}~\\
+ \pline[\top]{\Exists \buf' \bsup \buf. \bseen{\proc}{\buf'} \ast \intr{\linit{\loc}}(\buf')}~\\
+ \pline[\top]{\Exists \buf' \bsup \buf. \bseen{\proc}{\buf'}
+ \ast \intr{\linit{\loc}}(\buf')
+ \ast \intr{\relp{\loc}{Q}}(\buf')}~\\
+
+\end{hproofenv}
+
+\subsubsection{\ruleref{R-Acq}}
+\begin{hproofenv}
+ Context: $\buf, \proc, \loc, \ts, \bseen{\proc}{\buf}, (\loc, \any,\ts) \in \buf$~\\
+ \pline[\top]{\intr{\linit{\loc}}(\buf) \ast \intr{\acqp{\loc}{R}}(\buf)}~\\
+ Context: $P, \iname, \gname, s, i, Q_i, \ts, (\loc, \any, \ts) \in \buf,
+ \STS(\mSlP{S}{\loc}{P}, \intlP{\varphi}{\loc}{P},\gname,\iname),
+ \always \later \big(\All \val_\loc, \buf.
+ \intr{Q_i(\val_\loc)}(\buf) \Ra \intr{R(\val_\loc)}(\buf) \big)$~\\
+ \pline[\top]{i \Mapsto Q_i \ast \ownGhost{\gamma}{\authfrag \stsstate;[C_i]}}~\\
+ \begin{psubenv}{open $\iname$}
+ Context: $Q, \splset_1, \splset_2, \hist, i \in \splset_2$
+ since $\hist \neq \nil$ \by $\bseen{\proc}{\buf}, (\loc, \any,\ts) \in \buf$~\\
+ \pline[-\set\iname]{
+ i \Mapsto Q_i \ast \ownGhost{\gamma}{\authfull (\splset_1, \splset_2, \hist);[C_i]}
+ \ast \later\lhist{\loc}{\hist}
+ \ast \later\ress{\loc}{P}{Q}{\splset_1}
+ \ast \bigast_{\buf_0 \in \hist}
+ \bigast_{j \in \splset_2} \later\later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ }~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\iname]{\later\lhist{\loc}{\hist}}~\\
+ \cdline{\eload{\acq}{\loc}, \proc}~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &\later\lhist{\loc}{\hist} \ast \Exists \buf'' \in \hist.
+ \Exists \buf' \bsup (\buf \cup \buf''). \bseen{\proc}{\buf'} \\
+ &\; \ast \Exists \ts' \ge \ts. \mr{\buf'}{(\loc, \val, \ts')}
+ \ast \head(\buf'') = (\loc,\val,\ts')
+ \end{aligned}
+ } \by ~\ruleref{AtomicRead}
+ \end{psubenv}~\\
+ Context: $\buf', \buf'', \ts', \buf' \bsup (\buf \cup \buf''), \buf'' \in \hist,
+ \ts' \ge \ts, \mr{\buf'}{(\loc, \val, \ts')},
+ \head(\buf'') = (\loc,\val,\ts')$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &
+ i \Mapsto Q_i \ast \ownGhost{\gamma}{\authfull (\splset_1, \splset_2, \hist);[C_i]}
+ \ast \later\lhist{\loc}{\hist} \ast \bseen{\proc}{\buf'} \\
+ & {}\ast \ress{\loc}{P}{Q}{\splset_1}
+ \ast \bigast_{\buf_0 \in \hist} \bigast_{j \in \splset_2} \later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ \end{aligned}
+ }~\\
+ Context: $\always \later \big(\All \val_\loc, \buf. \intr{P(\val_\loc)}(\buf) \Lra
+ \bigast_{j \in \splset_1} \intr{Q(j)(\val_\loc)}(\buf) \big)$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &
+ \ownGhost{\gamma}{\authfull (\splset_1, \splset_2, \hist);[C_i]}
+ \ast \later\lhist{\loc}{\hist} \ast \bseen{\proc}{\buf'}
+ \ast i \Mapsto Q_i \ast i \Mapsto Q(i) \\
+ &{} \ast
+ \bigast_{j \in \splset_1 \setminus \set{i}} j \Mapsto Q(j)
+ \ast \bigast_{\buf_0 \in \hist} \big(\bigast_{j \in \splset_2\setminus \set{i}}
+ \later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ \ast \later \intr{Q(i)(\buf_0.\weval)}(\buf_0)\big)
+ \end{aligned}
+ }~\\
+ Allocate $i_1 \Mapsto Q(i_1), i_2 \Mapsto Q(i_2)$ where $i_1,i_2 \notin \splset$,
+ $Q(i_1), Q(i_2)$ are defined as in \ref{sec:readsplit} for $\val_0 \eqdef \val$~\\
+ It's clear that $\All v, b. Q(i)(v)(b) \Lra Q(i_1)(v)(b) \ast Q(i_2)(v)(b)$~\\
+ Pick $\splset'_1 \eqdef \splset_1 \setminus \set{i} \uplus \set{i_1,i_2},
+ \splset'_2 \eqdef \splset_2 \setminus \set{i} \uplus \set{i_1}$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &
+ \ownGhost{\gamma}{\authfull (\splset'_1, \splset'_2, \hist);[C_{i_1}]}
+ \ast \later\lhist{\loc}{\hist} \ast \bseen{\proc}{\buf'}
+ \ast \later Q_i = Q(i) \ast \bigast_{j \in \splset'_1} j \Mapsto Q(j) \\
+ &{} \ast
+ \bigast_{\buf_0 \in \hist} \big(\bigast_{j \in \splset_2\setminus \set{i}}
+ \later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ \ast \later \intr{Q(i_1)(\buf_0.\weval)}(\buf_0)
+ \ast \later \intr{Q(i_2)(\buf_0.\weval)}(\buf_0)\big)
+ \end{aligned}
+ }~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &
+ \ownGhost{\gamma}{\authfull (\splset'_1, \splset'_2, \hist);[C_{i_1}]}
+ \ast \later\lhist{\loc}{\hist} \ast \bseen{\proc}{\buf'}
+ \ast \later Q_i = Q(i) \ast \bigast_{j \in \splset'_1} j \Mapsto Q(j) \\
+ &{} \ast
+ \bigast_{\buf_0 \in \hist} \bigast_{j \in \splset'_2}
+ \later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ \ast \bigast_{\buf_0 \in \hist}\later \intr{Q(i_2)(\buf_0.\weval)}(\buf_0)
+ \end{aligned}
+ }~\\
+ Have $\later Q(i_2)(\val)(\buf'') = Q(i)(\val)(\buf'') = Q_i(\val)(\buf'')$
+ since $\buf''.\weval = \val$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &
+ \ownGhost{\gamma}{\authfull (\splset'_1, \splset'_2, \hist);[C_{i_1}]}
+ \ast \later\lhist{\loc}{\hist} \ast \bseen{\proc}{\buf'}
+ \bigast_{j \in \splset'_1} j \Mapsto Q(j) \\
+ &{} \ast
+ \bigast_{\buf_0 \in \hist} \bigast_{j \in \splset'_2}
+ \later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ \ast \later \intr{Q_i(\val)}(\buf'')
+ \end{aligned}
+ } since $\buf'' \in \hist$~\\
+ \pline[-\set\iname]{
+ \begin{aligned}
+ \Ret \val. &
+ \ownGhost{\gamma}{\authfull (\splset'_1, \splset'_2, \hist);[C_{i_1}]}
+ \ast \later\lhist{\loc}{\hist} \ast \bseen{\proc}{\buf'}
+ \bigast_{j \in \splset'_1} j \Mapsto Q(j) \\
+ &{} \ast
+ \bigast_{\buf_0 \in \hist} \bigast_{j \in \splset'_2}
+ \later \intr{Q(j)(\buf_0.\weval)}(\buf_0)
+ \ast \later \intr{R(\val)}(\buf') \ast i_1 \Mapsto Q(i_1)
+ \end{aligned}
+ } \by mono. of $Q_i$, assm.~\\
+ \end{psubenv}~\\
+ \pline[\top]{\Ret \val. \Exists \buf' \bsup \buf. \bseen{\proc}{\buf'}
+ \ast \Exists \stsstate', i'. i' \Mapsto Q_{i}[\val := \top]
+ \ast \ownGhost{\gamma}{\authfrag \stsstate';[C_{i'}]}
+ \ast \later\intr{R(\val)}(\buf')}~\\
+ \pline[\top]{\Ret \val. \Exists \buf' \bsup \buf. \bseen{\proc}{\buf'}
+ \ast \later\intr{R(\val)}(\buf')
+ \ast \intr{\acqp{\loc}{R[\val:=\top]}}(\buf')}\\
+\end{hproofenv}
+
+\subsubsection{\ruleref{Rel-Split}}
+
+\subsubsection{\ruleref{Acq-Split}}
+
+\subsubsection{\ruleref{A-R}}
+%
+%
+%
+%
+%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rsl"
+%%% End:
diff --git a/rsl/rsl.tex b/rsl/rsl.tex
new file mode 100644
index 00000000..ab0c65f2
--- /dev/null
+++ b/rsl/rsl.tex
@@ -0,0 +1,47 @@
+\documentclass[10pt]{article}
+\newif\ifslow\slowfalse %\slowtrue
+%\usepackage{lmodern}
+%\usepackage{fontenc}
+%\usepackage[utf8]{inputenc}
+\ifslow
+ \usepackage[english]{babel}
+ \usepackage[babel=true]{microtype}
+\fi
+\usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}
+%\usepackage[backend=bibtex]{biblatex} % If we want biblatex
+
+\input{../setup}
+\input{../layer1def}
+\input{../layer2def}
+\input{rsldef}
+\usepackage[section]{placeins}
+
+%\bibliography{bib} % If we want biblatex
+
+
+\begin{document}
+
+\title{\bfseries RSL in Iris}
+
+\def\andcr{\end{tabular}\\\begin{tabular}[t]{c}}% see \@maketitle in article.cls and \and in latex.ltx
+\maketitle
+\let\andcr\relax%
+
+\thispagestyle{empty}
+
+%\clearpage
+\tableofcontents
+
+\input{basic}
+\input{relacq}
+\input{cas}
+
+\iffalse%
+\printbibliography % If we want biblatex
+\else
+\bibliographystyle{abbrv}
+\advance\baselineskip-4pt
+\bibliography{bib}
+\fi
+
+\end{document}
diff --git a/rsl/rsldef.tex b/rsl/rsldef.tex
new file mode 100644
index 00000000..0bf91400
--- /dev/null
+++ b/rsl/rsldef.tex
@@ -0,0 +1,34 @@
+%% RSL
+
+\newcommand{\linit}[1]{\mathrm{Init}(#1)}
+\newcommand{\mSlP}[3]{\mathbb{#1}_{#2,#3}}
+\newcommand{\intlP}[3]{{#1}_{#2,#3}}
+\newcommand{\intlPs}[4]{\intlP{#1}{#2}{#3}(#4)}
+
+\newcommand{\sqsetComp}[2]{
+\left[%
+#1%
+\;\middle|\;%
+#2%
+\right]
+}
+
+\newcommand{\sUninit}[1]{\textsf{uninit}(#1)}
+\newcommand{\sUninitTok}[2]{\sUninit{#1};\sqsetComp{C_{#2}}{#2 \notin #1}}
+\newcommand{\splset}{I}
+\newcommand{\Splset}{\fpset{\Nat}}
+\newcommand{\sVsplitTok}[4]{(#1,#2,#3)|\sqsetComp{C_{#4}}{#4 \notin #2}}
+\newcommand{\sVSsplitTok}[3]{(#1,#2)|\sqsetComp{C_{#3}}{#3 \notin #1}}
+
+\newcommand{\ress}[4]{\mathrm{ress}(#1,#2,#3,#4)}
+\newcommand{\resst}[4]{\mathrm{ress2}(#1,#2,#3,#4)}
+
+\newcommand{\relp}[2]{\mathrm{Rel}(#1,#2)}
+\newcommand{\acqp}[2]{\mathrm{Acq}(#1,#2)}
+\newcommand{\rmwp}[2]{\mathrm{RMWAcq}(#1,#2)}
+\newcommand{\stsstate}{s}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "rsl"
+%%% End:
--
GitLab