diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..32820925abcdf41a21cd63ab54dbfcb58aab5584
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,14 @@
+*.log
+*.aux
+*.fdb_latexmk
+*.fls
+*.out
+*.pdf
+*.dvi
+*.synctex.gz
+*.prv
+*.toc
+.#*
+_*
+auto
+*.fmt
diff --git a/appendix.tex b/appendix.tex
index 625bbbeea79a8d368dd0acc220523f4e8f844458..23fc5a4c2e7f15e4f41196acd83e43ec96936534 100644
--- a/appendix.tex
+++ b/appendix.tex
@@ -38,8 +38,11 @@
\clearpage
\part{Modelling GPS for SRA in Iris}
-\input{framework}
-
+\input{intro}
+\input{defs}
+\input{lang}
+\input{layer1}
+\input{layer2}
%% \part{Working with Iris}
%% \input{encodings}
%% \input{atomic-shifts}
diff --git a/defs.tex b/defs.tex
new file mode 100644
index 0000000000000000000000000000000000000000..b8891dea49b6d40c4bd18a8fac94b52d73bf2b4f
--- /dev/null
+++ b/defs.tex
@@ -0,0 +1,57 @@
+\clearpage
+\section{Definitions}
+\subsection{General Types and Operators}
+\begin{align*}
+ \OrdList(T, R) \eqdef{}& \setComp{l \in \List(T)}{l\mbox{ ordered w.r.t. }R} \\
+\end{align*}
+
+\subsection{SRA-Specific Definitions}
+\def\What#1{\mbox{(#1)}}
+\[\begin{array}{c@{}r@{}lr}
+ \multicolumn{4}{l}{\hphantom{\hspace{0.9\textwidth}}} \\
+ \What{Meta Var.} \\ % & \What{Concept}
+ % & \What{Definition} & \What{What to call it} \\
+ \ts & \Time \eqdef{}& \Nat &\What{Timestamps} \\
+ \loc & \Loc \eqdef{}& \Nat &\What{Locations} \\
+ \val & \Value \eqdef{}& \Nat &\What{Values} \\
+ \we & \WriteEvent \eqdef{}
+ & \irecordSig[\weloc][\Loc][\weval][\Value][\wetime][\Time]
+ &\What{Write Event} \\
+ & \we_1 \werel \we_2 \eqdef{}& \we_1.\weloc = \we_2.\weloc \implies
+ \we_1.\wetime < \we_2.\wetime &\What{Partial Event Order} \\
+ \buf & \Buf \eqdef{}& \OrdList(\WriteEvent, \werel) & \What{Buffer} \\
+\end{array}\]
+%
+We will write $(\loc, \val, \ts)$ instead of
+$\irecord[\weloc][\loc][\weval][\val][\wetime][\ts]$ when convenient.
+
+\judgment{Future Buffer Relation}{\buf_2 \bsup \buf_1}
+\begin{align*}
+ \buf_2 \bsup \buf_1 \eqdef{}
+ & \All (\loc, \any, \ts_1) \in \buf_1.
+ \Exists \ts_2 \ge \ts_1. (\loc, \any, \ts_2) \in \buf_2
+\end{align*}
+The notion of future buffers is critical to the development.
+It encapsulates the influence of the non-deterministic communication between
+processes that goes on in the background.
+We will make sure to expose only assertions that are stable under this relation
+to the user.
+%
+%
+\subsection{Monoids}
+We equip some types defined above with a monoid structure.
+\begin{align*}
+ \BufMon \eqdef{}& \Monoid(\Buf, \nil, \cup) \\
+ \buf_1 \cup \buf_2 \eqdef{}
+ &
+ \begin{cases}
+ \buf_1 & \mbox{ if } \buf_1 \bsup \buf_2 \\
+ \buf_2 & \mbox{ if } \buf_2 \bsup \buf_1 \\
+ \bot & \mbox{ ow. }
+ \end{cases} \\
+\end{align*}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "appendix"
+%%% End:
diff --git a/framework.tex b/framework.tex
index 19e8e12518100c608e063342c2c6835b9ce0e32c..4652c982f0042067398086e090df5618f0555388 100644
--- a/framework.tex
+++ b/framework.tex
@@ -1,1069 +1,3 @@
-% CONVENTION:
-% Use \Ra/Lra for the logic and \implies/\iff for the metalogic.
-
-% This short (for now) note lays out a \emph{generic} separation logic which
-% manages sharing through invariants and ownership through (partial commutative)
-% monoids. The logic is generic in that the actual language it applies to is
-% taken as a parameter, giving in particular the atomic (per-thread) reduction
-% relation. Over this, we layer concurrency (by giving a semantics to \kw{fork}
-% and lifting to thread pools). The generic logic provides numerous logical
-% connectives and the semantics of Hoare triples and view shifts, together with a
-% large portion of the proof theory---including, in particular, the structural
-% rules for Hoare logic. Ultimately, these are proved sound relative to some
-% simple assumptions about the language. It should be possible, moreover, to give
-% a generic adequacy proof for Hoare triples as applied to the lifted thread-pool
-% semantics.
-
-% \section{Preliminaries}
-% We need several different generic and specific operations and orders on lists.
-% \subsection{Lists, Buffers}
-% \begin{align*}
-% \hd{\buf} = v \eqdef\;& \Exists e_0, \ldots, e_{n-1}. \buf = [e_0, \ldots, e_{n-1}, v] &\mbox{(Head)}\\
-% \length{\buf} = n \eqdef\;& \Exists e_0, \ldots, e_n. \buf = [e_0, \ldots, e_n] &\mbox{(Length)}\\
-% \btake{\buf}{i} = q' \eqdef\;& i <= \length{\buf} \land \Exists e_0, \ldots, e_{\length{\buf}}. q' = [e_0, \ldots, e_{i-1}] &\mbox{($i$-Prefix, exclusive)}\\
-% \\
-% q' \ge \buf \eqdef\;& \Exists q''. q' = \buf \mdoubleplus q'' & \mbox{(Monoid order)} \\
-% q' \qext \buf \eqdef\;& \Exists n, e_0, \ldots, e_n \in W, k \le n, i_0, \ldots, i_k \in [n].
-% & \mbox{(Subsequence order)}
-% \\
-% & q' = [e_0, \ldots, e_n] \land \buf = [e_{i_0}, \ldots, e_{i_k}] \land i_0 < \ldots < i_k \\
-% \dom{\buf} \eqdef\;& \{ \loc \alt (\loc, \_, \_) \in \buf \} \\
-% \buf[\loc] = \buf' \eqdef\;& \All \buf'' \subseteq \buf. \dom{\buf''} = \{l\} \implies \buf'' \qtxe \buf' &\mathrm{(Filter)} \\
-% \mri{\buf}{\loc} \eqdef\;& \max_{n < \length{\buf} \land \buf_n.L = \loc} n \\
-% \mr{\buf}{\loc} \eqdef\;& \buf_{\mri{\buf}{\loc}} % \max_{(\_, \_, t) \in \buf[\loc]} t & \mbox{with } \max_{\emptyset} t \eqdef -1\\
-% \\
-% \mrp{\buf}{\loc} \eqdef\;& \btake{\buf}{\mri{\buf}{\loc}} \\
-% \buf' \bsup \buf \eqdef\;& \All \loc. \mr{q'}{\loc} \geq \mr{\buf}{\loc} &\mbox{(Subsumption order)} \\
-% %\qprefixes{\buf} \eqdef\;& [\btake{\buf}{1}, \ldots, \btake{\buf}{\length{q}-1}] \\
-% %\zip{\buf}{\buf'} \eqdef\;& \ldots \\
-% e <^{=\Loc}_{\Time} e' \eqdef\;& e.L = e'.L \implies e.T < e'.T &\mathllap{\mbox{(Per-location Timestamp order)}}
-% \end{align*}
-
-% \section{Extensions to Iris}
-% We build upon an undocumented version of Iris that has no fixed notion of fork.
-% Instead, we can now define arbitrary reductions that fork off new threads and, crucially, change the physical state.
-
-% In addition, we make use of a novel interface for invariants which allows us to structure islands hierarchically:
-% \janno{TODO: This is probably wrong; TODO: masks}
-% \begin{mathpar}
-% \axiom{}{\nknowInv{\iota}{P} \eqdef \exists j. \knowInv{\iota.j}{P}}
-% \\
-% \axiom{}{P \vs \nknowInv{\iota}{P}}
-% \end{mathpar}
-%% It provides us with a new kind of state, \textbf{thread state} (denoted by $\ownThread{\threadstate}$, where $\threadstate \subset \mathrm{ThreadId}$).
-%% From this, we derive $\tid{i}$, an exclusive token representing one thread. Only $\fork{}$ creates new thread id tokens.
-%% \begin{align*}
-%% \ownThread{\threadstate} \cdot \ownThread{\threadstate'} &\vs \bot \\
-%% \tid{i} \cdot \tid{i} &\vs \bot
-%% \end{align*}
-%% For all of this to make sense, we also add the ability to execute view shifts around fork.
-%% This enables us to put thread ids into an invariant:
-%% \begin{mathpar}
-%% \infer
-%% {P \vs \ownThread{\threadstate} \ast P'
-%% \\
-%% \hoare{P'}{e}{\top}
-%% \\
-%% \ownThread{\threadstate \uplus i} \vs Q
-%% }
-%% %-------------------------------------------
-%% {\hoare{\later P \ast \later R}{\fork{e}}{i. Q \ast R}}
-%% \end{mathpar}
-%% where $Q$ can mention $i$. \janno{add masks}
-
-\section{Instantiating Iris}
-
-\paragraph{Expressions and Evaluation Contexts}
-Our expressions are those of GPS.
-\textbf{Note} that we have two fork constructs. One of them, $\gfork\!\!$, mirros the
-fork expression of GPS and is responsible for creating new processors.
-The second one, $\fork\!\!$, will be used later to concurrently run non-deterministic
-inter-processor communication.
-\janno{Clean this up}
-%
-\begin{align*}
- \loc \in \Loc ::={}& \ldots \\
- \expr \in \Expr ::={}&
- \val \in \Nat
- \walt \ealloc{\blocks}
- \walt \eload{\rtype}{\loc}
- \walt \estore{\wtype}{\loc}{\val}
- \walt \escas{\loc}{\val}{\val} \\
- & \walt \gfork \expr \walt \fork \expr \\
- &
- \walt \elet{\var}{\expr}{\expr'}
- \walt \erepeat{\expr}
- \walt \Some \expr
- \walt \None
- \\
- K \in \ECTX ::={}& \cdot \walt \elet{x}{K}{e} \walt \erepeat{K}
-\end{align*}
-However, the expressions we present to Iris are defined as follows: \[\IExpr = \Expr \times \ThreadId.\]
-
-\paragraph{Physical State}
-\begin{align*}
- \state \in \Sigma &\eqdef \recordSig[\sbuf][\Sigma_B][\sind][\Sigma_I][\stime][\Sigma_T]
- & \mbox{(Physical State)}\\
- \Sigma_B &\eqdef W^{\ast} & \mbox{(Buffer State)} \\
- W &\eqdef \recordSig[\weloc][\Loc][\weval][\Value][\wetime][\Time] &\; \mbox{(Write event)} \\
- \Sigma_I &\eqdef \Nat \times \Nat \fpfn \Nat & \mbox{(Index State)}\\
- \Sigma_T &\eqdef \Loc \fpfn \Nat &\; \mbox{(Timestamp server)} \\
-\end{align*}
-
-
-\paragraph{Atomic stepping relation}
-Essentially as in the SRA paper, with one exception:
-%% \begin{enumerate} %
-%% The original SRA paper has a fixed number of processors. We'd like to generalize that to better fit Iris' style of concurrency.
-%% Therefore,
-%% \item prefork (\textbf{new}):
-%% \begin{align*}
-%% \state; \prefork(\expr) \rightarrow_\thread \fork(\expr) ; \state' & \qquad \text{ if } (\state', \thread') = \textlog{newproc}(\state, \thread)
-%% \end{align*}
-%% where $\textlog{newproc}$ performs the necessary actions to add a new processor as a clone of $\thread$. \\
-%% \item
-We added a new expression called $\eprocess$ that attempts to import a new write event from a random processor into another random processor's buffer.
-It may ignore the write event it found if that event is outdated.
-$\eprocess$ always reduces to $()$.
-Intuitively, this combines SRA's \textbf{process} and \textbf{skip} in a single expression.
-
-The machine step relation is split into two: one with associated events and one without. The former is used for every expression that changes the machine state except $\eprocess$, whereas the latter is used exclusively for $\eprocess$.
-\\
-Example reductions:
-\begin{mathpar}
- \def\lstate{(\state_B, \state_I, \state_T)}
- \inferH{LOAD}%
- {\mr{\state_B(\proc)}{(\loc, \val, \_)}}%
- {\lstate; (\eload{\rtat}{\loc}, \proc) \rightarrow \lstate; (\val, \proc)}%
- %
- \and\inferH{STORE}%
- {\state_B' = \Cupd\state_B[\proc -::> (\loc, \val, \state_T(\loc)+1)]
- \\
- \state_T' = \Iupd\state_T[\loc -+> 1]
- }%
- {\lstate; (\estore{\wtat}{\loc}{\val}, \proc) \rightarrow
- (\state_B', \state_I, \state_T'); (\unitval, \proc)}%
- %
- \and\inferH{SCAS-OK}
- {\mr{\state_B(\proc)}{(\loc, \val_o, \state_T(\loc))}
- \\ \state_B' = \state_B[\proc \pointsto (\loc, \val_n, \state_T'(\loc)) :: \state_B(\proc)]
- \\ \state_T' = \state_T[\loc \pointsto \state_T(\loc)+1]}
- {\lstate; (\escas{\loc}{\val_o}{\val_n}, \proc) \rightarrow (\state_B', \state_I, \state_T'); (\Some{1}, \proc)}
- %
- \and\inferH{SCAS-FAIL}
- {\mr{\state_B(\proc)}{(\loc, \val_r, \state_T(\loc))}
- \\ \val_r \neq \val_o
- }
- {\lstate; (\escas{\loc}{\val_o}{\val_n}, \proc) \rightarrow \lstate; (\Some{0}, \proc)}
- %
- \and\inferH{SCAS-OLD}
- {\mr{\state_B(\proc)}{(\loc, \_, t)}
- \\ t < \state_T(\loc)
- }
- {\lstate; (\escas{\loc}{\val_o}{\val_n}, \proc) \rightarrow \lstate; (\None, \proc)}%
- %
- \and\inferH
- {PROCESS-OK}
- {\proc \neq \procB
- \\ k = \state_I(\proc, \procB)
- \\ \length{\state_B(\procB)} > k
- \\ (\loc, \val, \ts) = \state_B(\procB)_k
- \\ \bnew{\state_B(\proc)}{(\loc, \val, \ts)}
- }
- {\lstate; (process, \proc) \rightarrow
- (\fpfnupd{\state_B}{\proc}{(\loc,\val,\ts) :: \state_B(\proc)},
- \fpfnupd{\state_I}{(\proc, \procB)}{k+1}, \state_T)
- ; ((), \proc)}
- %
- \and\inferH
- {PROCESS-SKIP}
- {\proc \neq \procB
- \\ k = \state_I(\proc,\procB)
- \\ \length{\state_B(\procB)} > k
- \\ (\loc, \val, \ts) = \state_B(\procB)_k
- \\ \neg \bnew{\state_B(\proc)}{(\loc, \val, \ts)}
- }
- {\lstate; (process, \proc) \rightarrow
- (\state_B, \fpfnupd{\state_I}{(\proc,\procB)}{k+1}, \state_T)
- ; ((), \proc)}
- %
- \and\inferH
- {PROCESS-ALONE}
- {\dom{\state_B} = \emptyset \lor \Exists \procB. \dom{\state_B} = \set{\procB}}
- {\lstate; (process, \proc) \rightarrow
- (\state_B, \state_I, \state_T)
- ; ((), \proc)}
- %
- \and\inferH
- {PROCESS-BUSYBEAVER}
- {\All \procB \in \dom{\state_B}. \state_I(\proc, \procB) = \length{\state_B(\procB)}}
- {\lstate; (process, \proc) \rightarrow
- (\state_B, \state_I, \state_T)
- ; ((), \proc)}
-\end{mathpar}
-\\
-To illustrate the impact of the $\ThreadId$ component in $\IExpr$, we give the reduction rule of fork. This rule is the only one in which the $\ThreadId$ plays an important role.
-In addition, it showcases the new way to do fork in Iris.
-Note how the right-hand side of the reduction lists two expressions.
-The second expressions represents the ``forked'' thread.
-
-We have to take care of ``cloning'' the original processor and everything that
-is related to it in the physical state.
-%
-\janno{This rule is a little long}
-%% \end{enumerate}
-\begin{mathpar}
- \inferH{GFORK}
- {\proc \in \dom{\state.\sbuf} \\
- \procB \not\in \dom{\state.\sbuf} \\
- }
- {(\state_B, \state_I, \state_T); (\gfork{e}, \proc)
- \rightarrow
- (\Fupd\state_B[\procB -> \state_B(\proc)],
- \Fupd{%
- \Fupd\state_I[\proc, \procB -> \length{\state_B(\proc)}]%
- }[\All \proc'. \procB, \proc' -> \state_I(\proc, \proc')],
- \state_T
- ); (\procB, \proc); (e, \procB)}
-\end{mathpar}
-%
-Additionally, we have the second fork expression, which will not create a new
-processor.
-Instead, it creates an Iris thread which will run in the context of the original processor.
-\begin{mathpar}
- \inferH{GFORK}
- {\proc \in \dom{\state.\sbuf}}
- {\state; (\fork{e}, \proc)
- \rightarrow
- \state; (\unitval, \proc); (e, \proc)}
-\end{mathpar}
-
-\paragraph{\textlog{atomic} on expressions}
-
-\begin{align*}
- &\textlog{atomic}((\eload{\rtype}{\loc}, \pi)) \\
- &\textlog{atomic}((\estore{\wtype}{\expr}{\expr'}, \pi)) \\
- &\textlog{atomic}((\escas{\loc}{V_O}{\val_n}, \pi)) \\
- &\textlog{atomic}((\gfork{e}, \pi))
-\end{align*}
-
-\paragraph{Monoids}
-We split the construction of ghost space into two layers.
-%
-\begin{enumerate}
-\item
- We introduce lower bounds for buffers so that the buffers can be updated concurrently.
- At the same time, we introduce logical per-location histories.
- In these, we keep track of the timestamps, values, and the committing processor's buffer (including the new write event).
- We call the entries of these histories historic events.
-\item
- The last layer adds STS encodings of GPS protocols.
- The STS states are lists of protocol states paired with historic events.
- The STS invariant will tie the STS state to the previous layer's histories.
-\end{enumerate}
-
-We introduce the required monoids step-by-step while explaining and proving every layer of abstraction.
-
-\section{Interpreting GPS assertions}
-We will gradually introduce the interpretation of the various GPS assertions as we introduce the required abstractions.
-The basic connectives can be translated without mentioning the monoids we build
-up later.
-\janno{TODO: change to judgment}
-
-\begin{align*}
- \intr{\GPSProp} \eqdef&\; \MonQPred \\
- \intr{\GPSPred{X}} \eqdef&\; X \rightarrow \MonQPred
-\end{align*}
-
-\begin{align*}
- \intr{\cdot} \in &\; \Pi \; \GPSType \in \GPSTypes. \; \intr\GPSType \\
- \intr{\ownGhost{\gamma}{m}} (\buf) \eqdef& \; \ownGhost{\gamma}{m} \\
- %\intr{\loc \pointsto \val} (\buf) \eqdef& \; \Exists \buf' \bsub \buf. \ol{\loc}{\buf'} \\
- \intr{P(x)} (\buf) \eqdef&\; \intr{P}(x)(\buf) \\
- \intr{P \ast Q} (\buf) \eqdef& \; \intr P(q) \ast \intr Q(\buf)\\
- \intr{P \implies Q} (\buf) \eqdef& \; \All q' \bsup q. \intr P (\buf') \implies \intr Q (\buf') \\
- \intr{\All x \in X. P} (\buf) \eqdef&\; \All x \in X. \intr {P}(\buf) \\
- \intr{\Exists x \in X. P} (\buf) \eqdef&\; \Exists x \in X. \intr {P}(\buf) \\
- %\intr{\hoare{P}e{v. Q(v)}} \; q \eqdef& \; \All \buf' \bsup \buf, i. \\
- %&\;\hoare{\kq{i}{\buf'} \ast \intr P(\buf')}{e,i}{v. \Exists \buf'' \bsub \buf'. \kq{i}{\buf''} \ast \intr {Q(v)}(\buf'')} \\
- %\intr{\ldots} \; q \eqdef& \; \ldots
-\end{align*}
-
-
-\subsection{New Assertions}
-\label{sec:new-assertions}
-To simplify proofs, we introduce a new modality $\qpure$.
-This asserts that the interpretation of a GPS assertion $P$ holds regardless of the buffer.
-Additionally, we introduce an injection of monotone buffer predicates into the GPS assertion language.
-While $\qpure$ will be visible in our outer-most layer, the injection is only used within the inner layers.
-
-\begin{align*}
- \intr{\qpure P} (\_) \eqdef{}& \intr P(\nil) \\
- \intr{\lam \buf. \bpred} (\buf_0) \eqdef{}& \bpred\subst\buf{\buf_0} \
-\end{align*}
-
-
-\subsection{Interpreting GPS inference rules}
-It will be convenient to interpret entire GPS inference rules, which we do as follows:
-\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}
-
-\pagebreak
-\section{Layer 1}
-Our first layer will introduce lower bounds on processor buffers.
-We introduce a new monoid $\GMB \eqdef \auth{\Nat \fpfn \monhist(\Loc \times \Value \times \Time, <^{=\Loc}_{\Time})}$.
-$\monhist$ has only duplicable elements that represent lower bounds on the buffers.
-
-In addition, we introduce a definite history for every location. These histories consist of a list of buffers.
-Every buffer in $\loc$'s part of the map represents a write event to location $\loc$ in that the buffer is a snapshot
-of the committing processor's buffer at the time of the write access, including the newly preoduced write event.
-%\janno{This is confusing. TODO: talk about MO}
-\begin{align*}
- \GH \eqdef \auth{\Loc \fpfn \ex{\listty(\monlist(\Loc \times \Value \times \Time, <^{=\Loc}_{\Time})}}
-\end{align*}
-%
-We write $\head^2(\hist)$ to refer to the first entry of the first buffer in a
-locations's history $\hist$.
-
-We impose a consistency condition:
-every write event in a processor's buffer has to be justified by a write event in the respective location's history.
-
-\[\begin{array}{rlr}
- \PSInv \eqdef{}& \Exists \state_I, \state_T, \fMB, \fH. \ownPhys{(\fMB, \state_I, \state_T)} \ast \oMB{\fMB} \ast \oH{\fH} \\
- & {}\ast \always \PS((\fMB, \state_I, \state_T), \fMB, \fH) \\
- \PS(\state, \fMB, \fH) \eqdef{}& \SInv(\state.B, \state.I, \state.T) \land \HInv(\state.T, \fH)
- \land \DBHInv(\fMB, \fH) \\
- \SInv(\SProcs, \SIndex, \STime) \eqdef{}
- & \dom{\SIndex} = \dom{\SProcs}^2 \\
- & {}\land \All \proc \in \dom{\SProcs}, (\loc, \_, \ts) \in \SProcs(\proc). \ts \le \STime(\loc) \\
- &{}\land \All (\proc,\procB) \in \dom{\SIndex}. \\
- & \begin{array}{r@{}l}%
- & \SIndex(\proc, \procB) \le \length{\SProcs(\procB)} \\
- {}\land{}& \SProcs(\proc) \bsup \btake(\SProcs(\procB),\SIndex(\proc,\procB))
- \end{array}%
- \\
- \HInv(\STime, \fH) \eqdef{}& \dom{\fH} = \dom{\STime} \\
- & {}\land \All \loc \in \dom{\fH}. \head^2(\fH(\loc)).\wetime = \STime(\loc)\\
- \\
- \buf \lesssim \fH \eqdef{}& \All \buf_0, \loc, \val, \ts. \buf = \_ \doubleplus (\loc, \val, \ts) :: \buf_0
- \implies \Exists \buf'_0 \bsub \buf_0. (\loc,\val,\ts)::\buf'_0 \in \fH(\loc)
- \\
- \DBHInv(\fMB, \fH) \eqdef{}& \All {{\proc \in \dom{\fMB}}}. \fMB(\proc) \lesssim \fH
-\end{array}\]
-%
-\paragraph{Intuition} The $\lesssim$ relation enforces that, if processor $\pi$ commits a write event, every processor that learns of this write event
-must also have at least processor $\pi$'s knowledge (in terms of write events) up to that event.
-This knowledge is represented by the buffer in the location's history.
-
-Interestingly, we do not rely on enforcing exactly this condition.
-Instead, we simply do not record the origin of a write event.
-Only the processor's buffer is recorded.
-It is not necessary to know that the buffers in the locations history came from
-a processor.
-%
-\subsection{Laws}
-%
-We give the reasoning principles we want to use in this layer.
-The island name $\ips$ referes to the island that stores $\PSInv$.
-%
-\[\begin{array}{lrcl}
- &\bseen{\proc}{\buf} &\implies{}& \always\bseen{\proc}{\buf} \\
- \buf \bsub \buf_0 \vdash& \bseen{\proc}{\buf} &\implies{}& \bseen{\proc}{\buf_0} \\
- &\bseen{\proc}{\buf_1} \ast \bseen{\proc}{\buf_2} &\vs[\ips][\ips]& \begin{cases} \bseen{\proc}{\buf} & \mbox{ if } b = \max_\bsup(\buf_1, \buf_2) \\ \bot & \mbox{ ow. } \end{cases} \\
- &\lhist{\loc}{\hist} \ast \lhist{\loc}{\hist'} &\implies{}& \bot \\
- &\lhist{\loc}{\buf::\hist} &\vs[\ips][\ips]& \lhist{\loc}{\buf::\hist} \ast \head(\buf).L = \loc \\
- \mr{\buf}{(\loc, \val, \ts)} \vdash& \bseen{\proc}{\buf} \ast \lhist{\loc}{\hist} &\vs[\ips][\ips]& \always (\buf \bsup \btill{\hist(\loc)}{\ts}) \ast \lhist{\loc}{\hist}
-\end{array}\]
-%
-%
-\subsection{Definitions}
-%
-\begin{align*}
- \bseen{\proc}{\buf} \eqdef{}& \always\kmq{\proc}{\buf} \\
- \lhist{\loc}{\hist} \eqdef{}& \oh{\loc}{\hist} \\
- \btill{\hist}{\ts} \eqdef{}& \argmax_{\substack{i < \length{\hist} \\ \mr{\hist_i}{(\loc, \_, \ts}}} \hist_i
-\end{align*}
-%
-%
-\subsection{GPS Assertions}
-The lower bounds on buffers introduced in this layer are sufficient to provide
-the interpretation of GPS triples.
-Note that we frequently leave out the return value $\val$ when the expression
-reduces to $\unitval$.
-%
-\begin{align*}
- \intr{\hoare{P}e{\Ret \val. Q}} \; \buf \eqdef& \; \All \pi. \hoare{\bseen{\pi}{\buf} \ast \intr P(\buf)}{e,\pi}{\Ret\val. \Exists \buf' \bsub \buf. \bseen{\pi}{\buf'} \ast \intr {Q}(\buf')} \\
-\end{align*}
-%
-%
-\subsection{Triples}
-We provide the first set of triples.
-The pre- and post-conditions of the triples are not monotone buffer predicates.
-Thus, the triples are \textbf{not} representable in GPS.
-
-\begin{mathpar}
- \inferH{AtomicRead2}{}{\ereadHyp \vdash \hoare{\ereadPreB
- }{\eload{\rtat}{\loc}, \proc}{\ereadPostB } } \\
- \and\inferH{AtomicWrite2}{}{\estoreHyp \vdash \hoare{\estorePreB
- }{\estore{\wtat}{\loc}{\val}, \proc}{\estorePostB }} \\
- \and\inferH{CAS2}{}{\ecasHyp \vdash \hoare{\ecasPreB }{\escas{\loc}{\val_o}{\val_n}}{\ecasPostB }} \\
- \and\inferH{Process2}{}{\processHyp \vdash \hoare{\top}{\eprocess, \proc}{\processPostB}}
- \and\inferH{GFork2}{\gforkUHyp \vdash \hoare{\gforkUPreB}{e, \procB}{\gforkUPostB}}
- {\gforkHyp \vdash \hoare{\gforkPreB}{\gfork(e), \proc}{\gforkPostB}} \\
- \and\inferH{Fork2}{\forkUHyp \vdash \hoare{\forkUPreB}{e, \proc}{\forkUPostB}}
- {\forkHyp \vdash \hoare{\forkPreB}{\fork(e), \proc}{\forkPostB}} \\
-\end{mathpar}
-
-
-\subsection{Proofs}
-%
-\subsubsection{Lemmas}
-\begin{lem}[$\HInv$:Store]\label{lem:store-sinv}
- $\All \SProcs, \SIndex, \STime, \proc_0 \in \dom{\SProcs}, \loc_0 \in
- \dom{\STime}, \val_0.$
- \def\STimeB{\Iupd\STime[\loc_0 -+> 1]}%
- \def\SProcsB{\Cupd\SProcs[\proc_0 -::> (\loc_0, \val_0, \STime(\loc)+1)]}%
- \begin{align*}
- \SInv(\SProcs, \SIndex, \STime) \Ra \SInv(
- & \SProcsB, \\
- & \SIndex, \\
- & \STimeB).
- \end{align*}
- \begin{proof}~\\
- We have $\dom{\SIndex} = \dom{\SProcs}^2$,
- $\All \proc \in \dom{\SProcs}, (\loc, \_, \ts) \in \SProcs(\proc). \ts \le \STime(\loc)$,~\\
- and $\All (\proc, \procB) \in \dom{\SIndex}.
- \SIndex(\proc, \procB) \le \length{\SProcs(\procB)} \land \SProcs(\proc) \bsup \btake(\SProcs(\procB), \SIndex(\proc, \procB))$.
- \begin{enumerate}
- \item $\dom{\SIndex} = \dom{\SProcs}^2$. By assumption.
- \item Suppose $\proc \in \dom{\SProcs}$, $(\loc, \val, \ts) \in \SProcsB(\proc)$.~\\
- To show: $\ts \le \STimeB(\loc)$.
- \begin{enumerate}
- \item $\proc = \proc_0$, $(\loc',\val',\ts) = (\loc_0, \val_0, \STime(\loc)+1)$: ~\\
- We have $\ts = \STimeB(\loc_0) = \STime(\loc_0)+1$.
- \item Otherwise:
- by assumption.
- \end{enumerate}
-
- \item Suppose $(\proc, \procB) \in \dom{\SIndex}$.
- \begin{enumerate}
- \item To show: $\SIndex(\proc, \procB) \le \length{\SProcsB(\procB)}$.~\\
- By assumption and the fact that we only increase the length of a buffer.
- \item To show: $\SProcs(\proc) \bsup \btake(\SProcsB(\procB), \SIndex(\proc, \procB))$.~\\
- By assumption and the fact that we only grow a buffer (but not the
- indices).
- \end{enumerate}
- \qedhere
- \end{enumerate}
- \end{proof}
-\end{lem}
-%
-%
-\begin{lem}[$\SInv$:Store]\label{lem:store-hinv}
- $\All \STime, \fH, \loc_0 \in \dom{\STime}, \val_0, \buf_0.$
- \def\STimeB{\Iupd\STime[\loc_0 -+> 1]}%
- \def\fHB{\Cupd\fH[\loc_0 -::> ((\loc_0, \val_0, \STime(\loc_0)+1) :: \buf_0)]}%
- \begin{align*}
- \HInv(\STime, \fH) \Ra \HInv(
- & \STimeB, \\
- & \fHB)
- \end{align*}
- \begin{proof}~\\
- We have $\dom{\fH} = \dom{\STime}$,
- and $\All \loc \in \dom{\fH}. \head^2(\fH(\loc)).\wetime = \STime(\loc)$.
- \begin{enumerate}
- \item To show: $\dom{\fH} = \dom{\STimeB}$. By assumption.
- \item Suppose $\loc \in \dom{\fHB}$. ~\\
- To show: $\head^2(\fHB(\loc)).\wetime = \STimeB(\loc)$.
- \begin{enumerate}
- \item $\loc = \loc_0$. By reflexivity.
- \item Otherwise: by assumption.
- \end{enumerate}
- \qedhere
- \end{enumerate}
- \end{proof}
-\end{lem}
-%
-%
-\begin{lem}\label{lem:lesssim-mono}
- $\All \buf, \fH_1, \fH_2. $~\\
- $(\All \loc. \Exists \hist. \fH_2(\loc) = \fH_1(\loc) \mdoubleplus \hist)
- \Ra \buf \lesssim \fH_1 \Ra \buf \lesssim \fH_2$
- \begin{proof}~\\
- Suppose $\buf_0, \loc, \val, \ts. \buf = \_ \doubleplus (\loc, \val, \ts) ::
- \buf_0$.~\\
- To show: $\Exists \buf'_0 \bsub \buf_0. (\loc,\val,\ts)::\buf'_0 \in
- \fH_2(\loc)$.~\\
- We have $\buf_1 \bsub \buf_0$ \st $(\loc, \val, \ts) :: \buf_1 \in
- \fH_1(\loc)$.~\\
- We pick $\buf'_0 \eqdef \buf_1$.~\\
- By assumption, $(\loc, \val, \ts) :: \buf'_0 \in \fH_2(\loc)$.
- \end{proof}
-\end{lem}
-%
-%
-\begin{lem}[$\DBInv$:Store]\label{lem:store-dbinv}
- $\All \fMB, \fH, \proc_0 \in \dom{\fMB}, \loc_0 \in \dom{\fH}, \val_0, \ts_0, \buf_0.$
- \def\fHB{\Cupd\fH[\loc_0 -::> ((\loc_0, \val_0, \ts_0) :: \buf_0)]}%
- \def\fMBB{\Cupd\fMB[\proc_0 -::> (\loc_0, \val_0, \ts_0)]}%
- \begin{align*}
- \DBInv(\fMB, \fH) \Ra \DBInv(
- & \fMBB, \\
- & \Fupd\fH[\loc_0 -> (\loc_0, \val_0, \ts_0) :: \fMB(\proc_0)])
- \end{align*}
- \begin{proof}~\\
- We have $\All {{\proc \in \dom{\fMB}}}. \fMB(\proc) \lesssim \fH$. ~\\
- Suppose $\proc \in \dom{\fMBB}$. ~\\
- To show: $\fMBB(\proc) \lesssim \fHB$.
- \begin{enumerate}
- \item $\proc = \proc_0$:~\\
- To show: $(\loc_0, \val_0, \ts_0) :: \buf_0 \lesssim \fHB$.~\\
- Suppose $\buf_1, \loc \in \dom{\fHB}, \val, \ts$.~\\
- Suppose $(\loc_0, \val_0, \ts_0) :: \buf_0 = \_
- \doubleplus (\loc, \val, \ts) :: \buf_1$.~\\
- To show: $\Exists \buf_1' \bsup \buf_1. (\loc, \val, \ts) :: \buf_1 \in \fHB(\loc)$.
- \begin{enumerate}
- \item $\buf_1 = \buf_0$:~\\
- We have $(\loc, \val, \ts) = (\loc_0, \val_0, \ts_0)$.~\\
- To show $\Exists \buf_1' \bsup \buf_0. (\loc_0, \val_0, \ts_0) :: \buf_1'
- \in ((\loc_0, \val_0, \ts_0) :: \buf_0) :: \fH(\loc)$.~\\
- Trivial with $\buf_1 \eqdef \buf_0$.
- \item $\buf_1 \neq \buf_0$: by Lemma~\ruleref{lem:lesssim-mono} and assumption.
- \end{enumerate}
- \item $\proc \neq \proc_0$: by assumption.
- \qedhere
- \end{enumerate}
- \end{proof}
-\end{lem}
-%
-
-\begin{lem}\label{lem:process-small}
- $\All \fMB, \fH, \proc \in \dom{\fMB}, \buf, \loc, \val,
- \ts$.
- \def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
- \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
- \def\tup{(\loc, \val, \ts)}%
- \[\begin{array}{@{}r@{}l}
- \multicolumn{2}{l}{%
- \fMB(\proc) \bsup \buf%
- \land \buf' \bsub \buf \land \tup :: \buf' \in \fH(\loc)} \\
- {}\implies{} & \tup :: \fMB(\proc) \bsup \tup :: \buf \\
- & {} \land \Exists \buf'' \bsub \fMB(\proc). \tup :: \buf'' \in \fH(\loc)
- \end{array}\]
-\begin{proof}
- We have
- $\fMB(\proc) \bsup \buf$,
- $\buf' \bsub \buf$, and $\tup :: \buf' \in \fH(\loc)$.
- \begin{enumerate}
- \item To show: $\tup :: \fMB(\proc) \bsup \tup :: \buf$. By assumption, and
- monotonicity of $\bsup$.
- \item To show:
- $\Exists \buf'' \bsub \fMB(\proc). \tup :: \buf'' \in \fH(\loc)$.~\\
- We pick $\buf'' \eqdef \buf'$. ~\\
- By transitivity we have $\fMB(\proc) \bsup \buf'$.~\\
- By assumption, $\tup :: \buf \in \fH(\loc)$.
- \qedhere
- \end{enumerate}
-\end{proof}
-\end{lem}
-%
-\begin{lem}[$\DBInv+\SInv$:Process]\label{lem:process-ok}
- $\All \fMB, \fH, \proc, \procB \in \dom{\fMB}, \buf, \loc, \val,
- \ts$.
- \def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
- \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
- \def\tup{(\loc, \val, \ts)}%
- \[\begin{array}{@{}r@{}l}
- \multicolumn{2}{l}{\SInv(\fMB, \SIndex, \STime) \land \DBInv(\fMB, \fH)} \\
- {}\land{} & \state_I(\proc,\procB) < \length{\fMB(\procB)} \\
- {}\land{} & \bnew{\fMB(\proc)}{\fMB(\procB)_{\state_I(\proc,\procB)}} \\
- {}\implies{}& \SInv(\fMBB, \SIndexB, \STime) \\
- & {} \land \DBInv(\fMBB, \fH)
- \end{array}\]
-\begin{proof}
-\janno{TODO} using Lemma~\ruleref{lem:process-small}
-\end{proof}
-\end{lem}
-%
-\begin{lem}[$\DBInv+\SInv$:Process]\label{lem:process-skip}
- $\All \fMB, \fH, \proc, \procB \in \dom{\fMB}, \buf, \loc, \val,
- \ts$.
- \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
- \def\tup{(\loc, \val, \ts)}%
- \[\begin{array}{@{}r@{}l}
- \multicolumn{2}{l}{\SInv(\fMB, \SIndex, \STime)} \\
- {}\land{} & \state_I(\proc,\procB) < \length{\fMB(\procB)} \\
- {}\land{} & \neg\bnew{\fMB(\proc)}{\fMB(\procB)_{\state_I(\proc,\procB)}} \\
- {}\implies{}& \SInv(\fMB, \SIndexB, \STime)
- \end{array}\]
-\begin{proof}
-Trivial. \janno{TODO}
-\end{proof}
-\end{lem}
-%
-%
-\subsubsection{\ruleref{AtomicRead2}}
-%
-\begin{hproofenv}
- Context: $\buf$, $\proc$, $\loc$, $\ts$, $\bseen{\proc}{\buf}$, $(\loc, \_,
- \ts) \in \buf$~\\
- \pline[\top]{\top}~\\
- \begin{psubenv}{open $\ips$}
- Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
- Context: $\fMB(\proc) \bsup \buf$ \mbox{\by def. $\GMB$}~\\
- Context: $\bseen{\proc}{\fMB(\proc)}$~\\
- Context: $\Exists \val, \ts'. \mr{\fMB(\proc)}{(\loc, \val, \ts)}$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \mr{\fMB(\proc)}{(\loc, \val, \ts)}}~\\
- \cdline{\eload{\rtat}{\loc}, \proc}~\\
- \pline[-\set\ips]{\Ret \val'. \ownPhys{(\fMB, \state_I, \state_T)} \ast \val' = \val} \by ~\ruleref{LOAD}
- \end{psubenv}~\\
- \pline[-\set\ips]{\Ret \val. \ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB
- \ast \ofH \ast \mr{\fMB(\proc)}{(\loc, \val, \ts')}}
- \end{psubenv}~\\
- \pline[\top]{\Ret \val. \bseen{\proc}{\fMB(\proc)} \ast \mr{\fMB(\proc)}{(\loc, \val, \ts')} }
-\end{hproofenv}
-%
-%
-\subsubsection{\ruleref{AtomicWrite2}}
-%
-\begin{hproofenv}
- Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$~\\
- \pline[\top]{\estorePreB}~\\
- \pline[\top]{\intr{\estorePreB}(\buf)}~\\
- \begin{psubenv}{open $\ips$}
- Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
- Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
- Context: $\bseen{\proc}{\fMB(\proc)}$~\\
- Context: $\fH(\loc) = \hist$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
- \cdline{\eload{\rtat}{\loc}, \proc}~\\
- Define: $\state_T' \eqdef \Iupd\state_T[\loc -+> 1]$~\\
- \pline[-\set\ips]{\ownPhys{(\Cupd\fMB[\proc -::> (\loc, \val,
- \state_T'(\loc))], \state_I, \state_T')}} \by ~\ruleref{STORE}
- \end{psubenv}~\\
- \pline[-\set\ips]{\Ret \val. \ownPhys{(\Cupd\fMB[\proc -::> (\loc, \val,
- \state_T'(\loc))], \state_I, \state_T')} \ast \ofMB \ast \ofH}~\\
- Define: $\fMB' \eqdef \Cupd\fMB[\proc -::> (\loc, \val,
- \state_T'(\loc))]$.~\\
- Define: $\fH' \eqdef \Cupd\fH[(\loc -::> (\loc, \val, \state_T'(\loc))::\fMB(\proc))]$.~\\
- \pline[-\set\ips]{\Ret \val. \ownPhys{(\fMB', \state_I, \state_T')} \ast \oMB{\fMB'} \ast \oH{\fH'}}
- \by Ghost Update ~\\
- Context: $\PS((\fMB', \state_I, \state_T'), \fMB', \fH')$ \by
- Lemmas~\ruleref{lem:store-sinv},~\ruleref{lem:store-hinv}, and~\ruleref{lem:store-dbinv} ~\\
- \end{psubenv}~\\
- \pline[\top]{\Ret \val. \bseen{\proc}{\fMB(\proc)} \ast \mr{\fMB(\proc)}{(\loc, \val, \ts')} } ~\\
- \pline[\top]{\Ret\val. \ereadPostBI} \with $\buf' = \fMB(\proc)$, $\ts' = \ts'$.
-\end{hproofenv}
-%
-%
-\subsubsection{\ruleref{CAS2}}
-%
-\begin{hproofenv}
- Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$, $\loc$, $\hist$,
- $(\loc, \_, \_) \in \buf$~\\
- \pline[\top]{\estorePreB}~\\
- \begin{psubenv}{open $\ips$}
- Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH
- \ast \lhist{\loc}{\hist}}~\\
- Define: $(\_, \val, \ts) \eqdef \head^2(\hist)$~\\
- Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
- Context: $\bseen{\proc}{\fMB(\proc)}$, $\fH(\loc) = \hist$, $\ts = \state_T(\loc)$~\\
- \begin{psubenv}{$(\loc, \val, \ts) \in \fMB(\proc)$}
- Case: $(\loc, \val, \ts) \in \fMB(\proc)$~\\
- Context:
- $\mr{\fMB(\proc)}{(\loc, \val, \ts)}$ \by $\SInv(\fMB, \state_I, \state_T)$~\\
- Context: $\fMB(\proc) \bsup \head(\hist)$ \by $\DBInv(\fMB, \fH)$~\\
- \begin{psubenv}{$\val = \val_o$}
- Case: $\val = \val_o$~\\
- Context: $\head^2(\hist).\weval = \val_o$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast
- \mr{\fMB(\proc)}{(\loc, \val_o, \ts)}}~\\
- \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc} ~\\
- Define: $\state_T' \eqdef \Iupd\state_T[\loc -+> 1]$~\\
- Define: $\fMB' \eqdef \Cupd\fMB[\proc -::> (\loc, \val_n,
- \state_T'(\loc))]$.~\\
- \pline[-\set\ips]{\Ret\val'. \val' = \Some 1 \ast \ownPhys{(\fMB', \state_I, \state_T')}} \by ~\ruleref{SCAS-OK}
- \end{psubenv}~\\
- Define: $\fH' \eqdef \Cupd\fH[(\loc -::> (\loc, \val_n,
- \state_T'(\loc))::\fMB(\proc))]$.~\\
- \pline[-\set\ips]{\Ret\val'. \val' = \Some 1 \ast \ownPhys{(\fMB',
- \state_I, \state_T')} \ast \oMB{\fMB'} \ast \oH{\fH'} \ast
- \lhist{\loc}{\fH'(loc)}}~\\
- Context: $\PS((\fMB', \state_I, \state_T'), \fMB', \fH')$ \by
- Lemmas~\ruleref{lem:store-sinv},~\ruleref{lem:store-hinv}, and~\ruleref{lem:store-dbinv} ~\\
- \end{psubenv}~\\
- \hline
- \begin{psubenv}{$\val \neq \val_o$}
- Case: $\val \neq \val_o$~\\
- Context: $\head^2(\hist).\weval \neq \val_o$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast
- \mr{\fMB(\proc)}{(\loc, \val, \ts)}}~\\
- \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc} ~\\
- \pline[-\set\ips]{\Ret\val'. \val' = \Some 0 \ast \ownPhys{(\fMB,
- \state_I, \state_T)}} \by ~\ruleref{SCAS-FAIL}
- \end{psubenv}~\\
- \pline[-\set\ips]{\Ret\val'. \val' = \Some 0 \ast \ownPhys{(\fMB,
- \state_I, \state_T)} \ast \ofMB \ast \ofH \ast \lhist{\loc}{\fH(\loc)}}~\\
- \end{psubenv}
- \end{psubenv}~\\
- \hline
- \begin{psubenv}{$(\loc, \val, \ts) \notin \fMB(\proc)$}
- Case: $(\loc, \val, \ts) \notin \fMB(\proc)$~\\
- Context: $\Exists \ts' < \ts.
- \mr{\fMB(\proc)}{(\loc, \_, \ts')}$ \by $\SInv(\fMB,
- \state_I, \state_T)$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast
- \mr{\fMB(\proc)}{(\loc, \_, \ts')}}~\\
- \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc} ~\\
- \pline[-\set\ips]{\Ret\val'. \val' = \None \ast \ownPhys{(\fMB,
- \state_I, \state_T)}} \by \ruleref{SCAS-OLD}~\\
- \end{psubenv}
- \end{psubenv}~\\
- \pline[-\set\ips]{%
- \begin{array}{r@{}l}%
- \multicolumn{2}{l}{
- \Ret\val'. \Exists \fMB', \fH', \state_T'.
- \ownPhys{(\fMB', \state_I, \state_T)}
- \ast \oMB{\fMB'}
- \ast \oH{\fH'}
- \ast \fMB'(\proc) \bsup \fMB(\proc)
- } \\
- \multicolumn{2}{l}{
- {}\ast \lhist{\loc}{\fH'(\loc)} \ast \always \PSInv((\fMB', \state_I, \state_T'), \fMB', \fH')
- } \\
- \multicolumn{2}{l}{
- \ast \left(
- (\val' = \Some 1 \ast \fH'(\loc) = \fMB' :: \fH(\loc)
- \ast \fMB'(\proc) \bsup \fH(\loc)
- \ast \head^2(\fH(\loc)) = \val_o)
- \right.
- } \\
- {}\lor{} & (\val = \Some 0 \ast \fH' = \fH
- \ast \fMB'(\proc) \bsup \hist
- \ast \head^2(\fH(\loc)) \neq \val_o) \\
- {}\lor{} & \left. (\val = \None \ast \fH' = \fH) \right)
- \end{array}%
- }
- \end{psubenv}
- \pline[\top]{%
- \begin{array}{r@{}l}%
- \multicolumn{2}{l}{
- \Ret\val'. \Exists \buf' \bsup \buf, \hist'.
- \bseen{\proc}{\buf'}
- \ast \lhist{\loc}{\hist'}
- } \\
- \multicolumn{2}{l}{
- \ast \left(
- (\val' = \Some 1 \ast \hist' = \buf' :: \hist
- \ast \buf' \bsup \hist
- \ast \head^2(\fH(\loc)) = \val_o)
- \right.
- } \\
- {}\lor{} & (\val = \Some 0
- \ast \hist' = \hist
- \ast \buf' \bsup \hist
- \ast \head^2(\hist) \neq \val_o) \\
- {}\lor{} & \left. (\val = \None \ast \hist' = \hist) \right)
- \end{array}%
- }
-\end{hproofenv}
-%
-\subsubsection{Process}
-%
-\begin{hproofenv}
- Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$~\\
- \pline[\top]{\top}~\\
- \begin{psubenv}{open $\ips$}
- Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
- Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
- \begin{psubenv}{\ruleref{PROCESS-OK}}
- Case: $\Exists \procB. \length{\fMB(\procB)} > \state_I(\proc, \procB)$~\\
- (cont'd): $(\loc, \val, \ts) = \fMB(\procB)_{\state_I(\proc, \procB)}$~\\
- (cont'd): $\bnew{\fMB(\proc)}{(\loc, \val, \ts)}$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
- \cdline{\eprocess, \proc}~\\
- Define: $\fMB' \eqdef \Cupd\fMB[\loc -::> (\loc, \val, \ts)]$~\\
- Define: $\state_I' \eqdef \Iupd\state_I[\proc, \procB -+> 1]$~\\
- \pline[-\set\ips]{\ownPhys{(\fMB', \state_I', \state_T)}} \by \ruleref{PROCESS-OK}
- \end{psubenv}~\\
- \pline[-\set\ips]{\ownPhys{(\fMB', \state_I', \state_T)}
- \ast \oMB{\fMB'}
- \ast \oH{\fH}} \by ghost update~\\
- Context: $\PSInv((\fMB', \state_I', \state_T), \fMB', \fH)$ \by Lemma~\ruleref{lem:process-ok}~\\
- \end{psubenv}~\\
- \hline
- \begin{psubenv}{\ruleref{PROCESS-SKIP}}
- Case: $\Exists \procB. \length{\fMB(\procB)} > \state_I(\proc, \procB)$~\\
- (cont'd): $(\loc, \val, \ts) = \fMB(\procB)_{\state_I(\proc, \procB)}$~\\
- (cont'd): $\neg\bnew{\fMB(\proc)}{(\loc, \val, \ts)}$~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
- \cdline{\eprocess, \proc}~\\
- Define: $\state_I' \eqdef \Iupd\state_I[\proc, \procB -+> 1]$~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I', \state_T)}} \by \ruleref{PROCESS-SKIP}
- \end{psubenv}~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I', \state_T)}
- \ast \oMB{\fMB}
- \ast \oH{\fH}} \by ghost update~\\
- Context: $\PSInv((\fMB, \state_I', \state_T), \fMB, \fH)$ \by Lemma~\ruleref{lem:process-skip}~\\
- \end{psubenv}
- \\\hline
- \begin{psubenv}{all other cases}
- Case: (depends on specific case)~\\
- \begin{psubenv}{Frame}
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
- \cdline{\eprocess, \proc}~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
- \by~\ruleref{PROCESS-ALONE} or~\ruleref{PROCESS-BUSYBEAVER}
- \end{psubenv}~\\
- \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}
- \ast \oMB{\fMB}
- \ast \oH{\fH}}~\\
- Context: $\PSInv((\fMB, \state_I, \state_T), \fMB, \fH)$ \by assumption~\\
- \end{psubenv}~\\
- \pline[\top]{\Exists \fMB', \state_I'.
- \ownPhys{(\fMB', \state_I', \state_T)}
- \ast \always\PSInv((\fMB', \state_I', \state_T), \fMB', \fH)
- }~\\
- \end{psubenv}
- \pline[\top]{\top}
-\end{hproofenv}
-%
-\subsubsection{GFork}
-\begin{hproofenv}
- Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$~\\
- Context: $\All \procB. \gforkU$~\\
- \
-\end{hproofenv}
-%
-%
-\clearpage
-\newcommand{\Prot}[0]{\mathrm{PROT}}
-\newcommand{\ststs}[0]{\mathit{ss}}
-\section{Layer 2: Adding Protocols}
-In this last and final layer, we add GPS protocols.
-Protocols are encoded by Iris state transition systems (STS).
-The key idea here is that the every protocol STS will keep track of the entire history of a single location.
-We do this to retain the duplicable part of GPS's protocol interpretation of past states.
-The STS interpretation will own the locations history from the previous layer.
-
-Formally, an STS is given by a pair of states and a transition relation, $(S, \ra)$.
-In our case, the STS state space \textbf{should} augment the location's history with a protocol state for every entry.
-However, since we ultimately wont care about the value and timestamp of write events, we reduce the state space to a pair of a protocol state and a buffer.
-The projection to the state component results in a monotone list w.r.t $\sqsupseteq_\tau$:
-\begin{align*}
- \mathbb{S}(S) \eqdef \monlist(S \times \monlist(\Loc \times \Value \times \Time, <^{=\Loc}_{\Time}), \sqsubseteq_{S,\tau})
-\end{align*}
-
-For every protocol $\tau$ with state space $\tau.S$ we define the monoid $\Prot_\tau \eqdef \STSMon{\mathbb{S}(\tau.S)}$.
-
-The transition relation is defined as follows
-\begin{mathpar}
- \infer{\\}{\nil \ra_{\Prot{\tau}} ((\stst, \buf)::nil)}
-
- \infer{\stst \ra_\tau \stst' }{((\stst, \buf)::\ststs) \ra_{\Prot{\tau}} ((\stst',\buf')::(\stst, \buf)::\ststs) }
-\end{mathpar}
-
-\janno{TODO: mapping to ghost names}
-
-We do not make use of Iris' tokens for STSs.
-Therefore, we adopt a simplified notational convention for STS assertions.
-In addition, we also define a shorthand asserting that the protocol has been in a particular state at some point.
-\newcommand{\STSat}[2]{\textcolor{OliveGreen}{\ownGhost{#1}{[#2]}}}
-\newcommand{\STSone}[2]{\textcolor{OliveGreen}{\ownGhost{#1}{#2}}}
-\begin{align*}
- \STSat{\gamma_\tau}{\ststs} \eqdef&\; \textcolor{OliveGreen}{\ownGhost{\gamma_\tau}{(\ststs, \uparrow \{\ststs\}, \emptyset) : \Prot{\tau}}} \\
- \STSone{\gamma_\tau}{\stst, \buf} \eqdef&\; \STSat{\gamma_\tau}{(\stst, \buf) :: \_}
-\end{align*}
-
-The invariants in this level are given by the usual STS invariants. We pick the following interpretation predicates.
-\newcommand{\Cons}[0]{\mathrm{Consistent}}
-\def\td{{\always\tau_{\mathrm{dup}}}}%
-\def\intd{\always\intr{\tau_{\mathrm{dup}}}}%
-\def\int{\intr{\tau}}%
-\begin{align*}
- \varphi_\tau(\ststs) \eqdef&\; \Exists h. \oh{\loc}{h} \ast \xi(\ststs, h) \land \Cons(\ststs, h) \land \bigwedge_{\substack{\mathclap{(\stst, \buf) \in \ststs}\\\val = \hd{\buf}.V}} \intd(\stst, \val)(\buf) \\
- \\
- \xi(\ststs) \eqdef&\;
- \begin{cases}
- \int(\stst, \hd{\buf}.V)(\buf) &\mbox{ if } \ststs = (\stst, \buf) :: \_ \\
- \top & \mbox{ ow. }
- \end{cases}
- \\
- %% \ststs \star h \eqdef&\;
- %% \begin{cases}
- %% (\stst, \val, \buf) :: (\ststs' \star h') & \mbox{ if } \ststs = (\ststs, \buf)::\ststs' \land h = (\val, \ts, \buf') :: h' \\
- %% nil & \mbox{ ow.}
- %% \end{cases} \\
- \Cons(\ststs, h) \eqdef&\;
- \begin{cases}
- \Cons(\ststs', h') & \mbox{ if } \ststs = (\stst, \buf) :: \ststs' \land h = \buf :: h' \\
- \top & \mbox{ if } \ststs = \nil \land h = \nil \\
- \bot & \mbox{ ow. }
- \end{cases} \\
-\end{align*}
-
-In our proofs, we do not care about the exact buffer $\buf$ used to justify a protocol state.
-However, we need to know that the processor's buffer is at least as big (in terms of $\bsup$) as that buffer.
-Additionally, the exact value of $\gamma_\tau$ is not important.
-Using Iris' new invariant scheme, we get away with just one existential as we re-use $\gamma$ to encode the island used for the STS assertion.
-Thus, the interpretation of the GPS protocol assertion becomes the following:
-\begin{align*}
- \intr{\protAt{\loc}{\stst}{\tau}} \; \buf \eqdef&\; \Exists \gamma, \buf_0 \bsub \buf. \STSone{\gamma}{\stst,\buf_0} \land \nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}(\tau.S), \varphi_\tau, \gamma)}
-\end{align*}
-
-Note how this assertion intuitively encodes what it means to know a lower bound on the GPS protocol state:
-knowing at least as much as the processor who advanced the protocol to that particular state.
-
-
-\janno{TODO: $\iota \in$ Something}
-
-While hiding $\gamma$ (and the island name) makes for a nice interface, it has counterintuitive consequences:
-we do not know a priori that two protocol assertions on $\loc$ are in any way related, as they could be talking about different $\gamma$ and $\iota$.
-Therefore, we need to manually establish the usual rules for protocol assertions such as:
-\begin{align*}
- \protAt{\loc}{\stst_0}{\tau} \ast \protAt{\loc}{\stst_1}{\tau} \vs&\;
- \begin{cases}
- \protAt{\loc}{\stst}{\tau} & \mbox{ if } \max \{\stst_0, \stst_1\} = \stst \\
- \bot & \mbox{ ow.} \\
- \end{cases}
-\end{align*}
-\janno{TODO: masks}
-\paragraph{Note:} we have to rely on view shifts here because the lemma is not provable without opening invariants.
-
-
-\subsection{Triples}
-The triples for $\fork{e}$ and $\eprocess$ are not affected by the abstractions introduced in this layer.
-
-Instead of stating triples in terms of GPS protocol assertions, we stay on a lower level of abstraction to simplify the proofs.
-The translation to fully flegded GPS triples is straight-forward and will happen in another layer.
-
-%% \def\ereadH {\intr{\All \stst' \sqsupseteq_\tau \stst, \val. \tau(\stst, \val) \ast P \implies \always Q}(\buf)}
-%% \def\ereadPreC {\kmq{\pi}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\tau}{\stst, \buf_0} \ast \intr P(\buf)}%
-%% \def\ereadPostC {\Ret\val'. \; \Exists \buf' \bsup \buf, \stst' \sqsupseteq_\tau \stst. \kmq{\pi}{\buf'} \ast \STSone{\gamma_\tau}{\stst', \buf'} \ast \intr{\always Q}(\buf')}%
-\def\ereadPreC {\kmq{\pi}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\tau}{\stst, \buf_0}}%
-\def\ereadPostC {\Ret\val.
- \begin{aligned}
- & \Exists \buf' \bsup \buf. \kmq{\pi}{\buf'} \ast \hd{\buf'} = (\loc, \val, \_) \\
- & \ast \Exists \stst' \sqsupseteq_\tau \stst. \STSone{\gamma_\tau}{\stst', \buf'} \ast \intd(\stst', \val)(\buf')
- \end{aligned}
-}
-
-\def\estoreHA {\intr{ P \ast P' \vs \tau(\stst'', \val) * Q}(\buf)}
-\def\estoreHB {\intr{\qpure \left( \All \stst' \sqsupseteq_\tau \stst. \tau(\stst', \_) \ast P \implies \stst'' \sqsupseteq_\tau \stst' \right)}(\buf)}
-\def\estoreHC {\intr{\qpure \left( \All \stst, \val. \tau(\stst, \val) \implies \td(\stst, \val) \right)}(\buf)}
-\def\estoreH {\later \varphi(\ststs \doubleplus (\stst, \buf_0) :: \_) \ast \P \vs \Exists q' \bsup \buf. \stst'' \sqsupseteq \hd{\stst' \doubleplus (\stst, \buf_0) :: \_}.S \ast \later \varphi((\stst'', \buf'))}
-\def\estorePreC {\kmq{\pi}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\tau}{\stst, \buf_0} \ast \intr{\qpure P \ast P'}(\buf)}%
-\def\estorePostC {\Exists \buf' \bsup \buf. \kmq{\pi}{\buf'} \ast \STSone{\gamma_\tau}{\stst'', \buf'} \ast \intr Q(\buf')}%
-\def\ecasHA {\intr{\All \stst' \sqsupseteq_\tau \stst. \tau(\stst', \val_o) \ast P \vs \Exists \stst'' \sqsupseteq_\tau \stst. \tau(\stst'', \val_n) * Q}(\buf)}
-\def\ecasHB {\intr{\left( \All \stst, \val. \tau(\stst, \val) \implies \td(\stst, \val) \right)}(\buf)}
-%\def\ecasHB {\intr{\All \stst'' \sqsupseteq_\tau \stst. \All y \neq \val_o. \td(\stst', y) \ast P \implies \always R}(\buf)}
-%\def\ecasHC {\intr{\All \stst'' \sqsupseteq_\tau \stst. \td(\stst', \_) \ast P \implies \always S}(\buf)}
-\def\ecasPreC {
- \begin{aligned}
- \kmq{\pi}{\buf} \ast \Exists \buf_0 \bsub q. \STSone{\gamma_\tau}{\stst, q_0} \ast \intr P(q)
- \end{aligned}
-}
-\def\ecasPostC {\Ret\val'.
- \begin{aligned}
- &\; \Exists \buf' \bsup \buf, \stst'' \sqsupseteq_\tau \stst. \kmq{\pi}{\buf'} \ast \STSone{\gamma_\tau}{\stst'', \buf'} \\
- \ast &\; \intrl(\val' = \Some 1\ast Q) \\
- \lor &\; \;(\val' = \Some 0 \ast (\mr{\buf'}{\loc}).V \neq \val_o \ast \td(\stst'', (\mr{\buf'}{\loc}).V)) \\
- \lor &\; \;(\val' = \None)\intrr(\buf')
- \end{aligned}
-}
-\begin{mathpar}
- \inferH{AtomicRead3}{}{\mathllap{\nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}, \varphi_\tau, \gamma_\tau)}} \vdash \hoare{\ereadPreC }{\eload{\rtat}{\loc}, \pi}{\ereadPostC } } \\
- \inferH{AtomicWrite3}{\estoreHA \\ \estoreHB \\ \estoreHC }{\mathllap{\nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}, \varphi_\tau, \gamma_\tau)}} \vdash \hoare{\estorePreC }{\estore{\wtat}{\loc}{\val}, \pi}{\estorePostC }} \\
- \inferH{CAS3}{\ecasHA \\ \ecasHB }{\mathllap{\nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}, \varphi_\tau, \gamma_\tau)}} \vdash \hoare{\ecasPreC }{\escas{\loc}{v_o}{v_n}, \pi}{\ecasPostC }} \\
- %\inferH{Fork3}{\All \rho. \hoare{\forkUPreC }{e, \rho}{\forkUPostC }}{\hoare{\forkPreC }{\fork(e), \pi}{\forkPostC }} \\
- %\axiomH{Process3}{\hoare{\processPreC }{\eprocess, \pi}{\processPostC }}
-\end{mathpar}
-
-\subsection{Proofs}
-\paragraph{\ruleref{AtomicRead3}:}
-We have a lower bound $\buf$ on processor $\pi$'s buffer and a lower bound on the protocol state of location $\loc$, $\STSone{\gamma_\tau}{\stst,\buf_0}$.
-We know $\buf_0 \bsub \buf$.
-Thus, there is at least one write event for $\loc$ in $\buf$ at some timestamp $\ts$.
-We are now in a position to apply the previous layer's triple.
-However, we first open the STS invariant and immediately frame off everything we acquired by doing this.
-We apply the layer-2 triple for $\eload{\rtat}{\loc}$.
-The return value is $\val$ and we learn a new lower bound on $\pi$'s buffer, $\buf' \bsup \buf$, s.t. $\mr{\buf'}{\loc} = (\loc, \val, \ts)$ with $\ts' \ge \ts$.
-We re-introduce the contents of the STS invariant, stripping off the later modality.
-This yields $\bigwedge_{(\stst, \buf'_0) \in \ststs} \intd(\stst, \hd{\buf'_0}.V)(\buf'_0)$ where $\ststs$ is the authoritative state of the STS.
-We also own the history $h$ for $\loc$.
-From \ruleref{Consistency} and \ruleref{LastEvent}, there exists $\buf'_0 \bsub q'$ s.t. $\buf'_0 \in h$ and $\hd{\buf'_0} = (\loc, \val, \ts',)$.
-From $\Cons(\ststs, h)$, there exists $\stst'$ s.t. $(\stst', \buf'_0) \in \ststs$.
-We extract the correpsonding lower bound $\STSone{\gamma_\tau}{\stst', \buf'_0}$.
-We have $\intd(\stst', \val)(\buf'_0)$.
-From $\ts' \ge \ts$, monotonicity of $h$, monotonicity $\ststs$, and $\Cons(\ststs, h)$, we have $\stst' \sqsupseteq_\tau \stst$. % \janno{TODO: MAKE THIS A LEMMA! IT IS HORRIBLE! ARGH!}
-This completes the proof
-
-\paragraph{\ruleref{AtomicWrite3}:}
-We assume $\mathbf{H_1} \eqdef \estoreHA $, $\mathbf{H_2} \eqdef \estoreHB $, and $\mathbf{H_3} \eqdef \estoreHC $.
-We have a lower bound on processor $\pi$'s buffer, $\buf$, and a lower bound on the protocol state $\stst$ at $\buf_0 \bsub \buf$.
-We own $\intr{\qpure P \ast P'}$ at $\buf$. % and, by $H_{3}$ at $\nil$.
-We open the STS invariant and frame off everything except $\loc$'s history $h$.
-We apply \ruleref{AtomicWrite2}.
-Our new lower bound on $\pi$'s buffer is $\buf' \bsup \buf$ with $\hd{\buf'} = (\loc, \val, \ts)$.
-$\loc$'s history is now $\buf' :: h$.
-We re-introduce the remaining contents of the STS interpretation.
-The authoritative GPS protocol state is $\stst' \sqsupseteq_\tau \stst$ at $\buf'_0$.
-We own $\int(\stst',\hd{\buf'_0}.V)(\buf'_0)$.
-We apply $\mathbf{H_2}$ to get $\stst'' \sqsupseteq_\tau \stst'$ (making use of $\qpure P$ in the process, without consuming it).
-We perform a frame-preserving update to change the authoritative state to $\stst''$ at $\buf'$ and extract a corresponding lower bound.
-We apply $\mathbf{H_3}$ to get $\intd(\stst', \_)(\buf')$.
-Finally, we apply $\mathbf{H_1}$ to acquire $\intr{\tau(\stst'', v)(\buf') \ast Q}(\buf')$, giving up both $\qpure P$ and $P'$.
-We close the STS invariant.
-This concludes the proof.
-
-\paragraph{\ruleref{CAS3}}
-We assume $\mathbf{H_1} \eqdef \ecasHA $ and $\mathbf{H_2} \eqdef \ecasHB $.
-We have a lower bound on processor $\pi$'s buffer, $\buf$, and a lower bound on the protocol state, $\stst$ at $\buf_0 \bsub \buf$.
-We own $P$ at $\buf$.
-We open the STS invariant and frame off everything except for the authoritative STS state $\ststs$ and the authoritative GPS protocol state $\stst' \sqsupseteq_\tau \stst$ at $\buf'_0$, and $\loc$'s history $h$.
-By $\Cons$ we have $\buf'_0 = \hd{h}$.
-By \ruleref{LastEvent} we have $\hd{q_0} = (\loc, \_, \_)$.
-Thus, by $\buf_0 \bsub \buf$ there exists $(\loc, \_, \_) \in \buf$.
-We apply \ruleref{CAS2}.
-The return value is $\val'$.
-We have $\buf' \bsup \buf$ and $h'$.
-$\buf'$ is the new lower bound of $\pi$'s buffer.
-We own $\oh{\loc}{h'}$.
-We re-introduce the remaining contents of the STS invariant, stripping off laters where applicable.
-This gives us $\int(\stst',\hd{\buf'_0}.V)(\buf'_0)$ and $\bigwedge_{(\stst, \buf'_0) \in \ststs} \intd(\stst, \hd{\buf'_0}.V)(\buf'_0)$.
-There are three cases:
-\begin{enumerate}
-\item{$\val' = \Some{1}$:}
- We know $\hd{\buf'} = (\loc, \val_n, \hd{\hd{h}}.T+1)$ and $h' = \buf' :: h$.
- We also know $\buf' \bsup \hd{h}$ and, thus, $\buf' \bsup \buf'_0$.
- Applying $\mathbf{H_2}$, we acquire $\td(\stst', \val_o)$ at $\buf'_0$.
- Finally, we use $\mathbf{H_1}$ to get $\stst'' \sqsupseteq_\tau \stst'$ such that $\intr{\tau(\stst'', \val_n) \ast Q}(\buf')$.
- We change the authoritative protocol state to $\stst''$ at $\buf'$.
- This suffices to re-establish the STS invariant.
-\item{$\val' = \Some{0}$:}
- No write event was generated, i.e. $h' = h$.
- We know $\buf' \bsup \hd{h}$ (and, thus, $\buf' \bsup \buf'_0$), and $(\mr{\buf'}{\loc}).V \neq \val_o$.
- We duplicate $\intd(\stst', \buf'_0)$.
- Since we changed neither state nor history the STS invariant is still true.
-\item{$\val' = \None$:}
- Everything remains as is.
-\end{enumerate}
-We close the STS invariant.
-This concludes the proof.
-
-
\section{Layer 3: Syntactic Sugar}
Finally, we will close the gap between GPS syntax and the triples we defined in this document.
This layer does not introduce additional ghost state or invariants.
@@ -1107,11 +41,11 @@ We now define a $\ecas{\loc}{\val_o}{\val_n}$, a simple loop around the single-s
}
\begin{mathpar}
- \iinferH{AtomicRead4}{\ereadH}{\hoare{\ereadPreD}{\eload{\rtat}{\loc}, \pi}{\ereadPostD}} \and
- \iinferH{AtomicWrite4}{\estoreHA \and \estoreHB \and \estoreHC }{\hoare{\estorePreD }{\estore{\wtat}{\loc}{\val}, \pi}{\estorePostD }} \\
- \iinferH{CAS4}{\ecasHA \and \ecasHC \\ \ecasHB }{\hoare{\ecasPreD }{\ecas{\loc}{v_o}{v_n}, \pi}{\ecasPostD }}% \\
- %\inferH{Fork4}{\All \rho. \hoare{\forkUPreD }{e, \rho}{\forkUPostD }}{\hoare{\forkPreD }{\fork(e), \pi}{\forkPostD }} \\
- %\axiomH{Process4}{\hoare{\processPreD }{\eprocess, \pi}{\processPostD }}
+ \iinferH{AtomicRead4}{\ereadH}{\hoare{\ereadPreD}{\eload{\rtat}{\loc}, \proc}{\ereadPostD}} \and
+ \iinferH{AtomicWrite4}{\estoreHA \and \estoreHB \and \estoreHC }{\hoare{\estorePreD }{\estore{\wtat}{\loc}{\val}, \proc}{\estorePostD }} \\
+ \iinferH{CAS4}{\ecasHA \and \ecasHC \\ \ecasHB }{\hoare{\ecasPreD }{\ecas{\loc}{v_o}{v_n}, \proc}{\ecasPostD }}% \\
+ %\inferH{Fork4}{\All \rho. \hoare{\forkUPreD }{e, \rho}{\forkUPostD }}{\hoare{\forkPreD }{\fork(e), \proc}{\forkPostD }} \\
+ %\axiomH{Process4}{\hoare{\processPreD }{\eprocess, \proc}{\processPostD }}
\end{mathpar}
%%% Local Variables:
diff --git a/intro.tex b/intro.tex
new file mode 100644
index 0000000000000000000000000000000000000000..c24026d0599982df3a7b0e1258130c54f9873044
--- /dev/null
+++ b/intro.tex
@@ -0,0 +1,72 @@
+% CONVENTION:
+% Use \Ra/Lra for the logic and \implies/\iff for the metalogic.
+
+% This short (for now) note lays out a \emph{generic} separation logic which
+% manages sharing through invariants and ownership through (partial commutative)
+% monoids. The logic is generic in that the actual language it applies to is
+% taken as a parameter, giving in particular the atomic (per-thread) reduction
+% relation. Over this, we layer concurrency (by giving a semantics to \kw{fork}
+% and lifting to thread pools). The generic logic provides numerous logical
+% connectives and the semantics of Hoare triples and view shifts, together with a
+% large portion of the proof theory---including, in particular, the structural
+% rules for Hoare logic. Ultimately, these are proved sound relative to some
+% simple assumptions about the language. It should be possible, moreover, to give
+% a generic adequacy proof for Hoare triples as applied to the lifted thread-pool
+% semantics.
+
+% \section{Preliminaries}
+% We need several different generic and specific operations and orders on lists.
+% \subsection{Lists, Buffers}
+% \begin{align*}
+% \hd{\buf} = v \eqdef\;& \Exists e_0, \ldots, e_{n-1}. \buf = [e_0, \ldots, e_{n-1}, v] &\mbox{(Head)}\\
+% \length{\buf} = n \eqdef\;& \Exists e_0, \ldots, e_n. \buf = [e_0, \ldots, e_n] &\mbox{(Length)}\\
+% \btake{\buf}{i} = q' \eqdef\;& i <= \length{\buf} \land \Exists e_0, \ldots, e_{\length{\buf}}. q' = [e_0, \ldots, e_{i-1}] &\mbox{($i$-Prefix, exclusive)}\\
+% \\
+% q' \ge \buf \eqdef\;& \Exists q''. q' = \buf \mdoubleplus q'' & \mbox{(Monoid order)} \\
+% q' \qext \buf \eqdef\;& \Exists n, e_0, \ldots, e_n \in W, k \le n, i_0, \ldots, i_k \in [n].
+% & \mbox{(Subsequence order)}
+% \\
+% & q' = [e_0, \ldots, e_n] \land \buf = [e_{i_0}, \ldots, e_{i_k}] \land i_0 < \ldots < i_k \\
+% \dom{\buf} \eqdef\;& \{ \loc \alt (\loc, \_, \_) \in \buf \} \\
+% \buf[\loc] = \buf' \eqdef\;& \All \buf'' \subseteq \buf. \dom{\buf''} = \{l\} \implies \buf'' \qtxe \buf' &\mathrm{(Filter)} \\
+% \mri{\buf}{\loc} \eqdef\;& \max_{n < \length{\buf} \land \buf_n.L = \loc} n \\
+% \mr{\buf}{\loc} \eqdef\;& \buf_{\mri{\buf}{\loc}} % \max_{(\_, \_, t) \in \buf[\loc]} t & \mbox{with } \max_{\emptyset} t \eqdef -1\\
+% \\
+% \mrp{\buf}{\loc} \eqdef\;& \btake{\buf}{\mri{\buf}{\loc}} \\
+% \buf' \bsup \buf \eqdef\;& \All \loc. \mr{q'}{\loc} \geq \mr{\buf}{\loc} &\mbox{(Subsumption order)} \\
+% %\qprefixes{\buf} \eqdef\;& [\btake{\buf}{1}, \ldots, \btake{\buf}{\length{q}-1}] \\
+% %\zip{\buf}{\buf'} \eqdef\;& \ldots \\
+% e <^{=\Loc}_{\Time} e' \eqdef\;& e.L = e'.L \implies e.T < e'.T &\mathllap{\mbox{(Per-location Timestamp order)}}
+% \end{align*}
+
+% \section{Extensions to Iris}
+% We build upon an undocumented version of Iris that has no fixed notion of fork.
+% Instead, we can now define arbitrary reductions that fork off new threads and, crucially, change the physical state.
+
+% In addition, we make use of a novel interface for invariants which allows us to structure islands hierarchically:
+% \janno{TODO: This is probably wrong; TODO: masks}
+% \begin{mathpar}
+% \axiom{}{\nknowInv{\iota}{P} \eqdef \exists j. \knowInv{\iota.j}{P}}
+% \\
+% \axiom{}{P \vs \nknowInv{\iota}{P}}
+% \end{mathpar}
+%% It provides us with a new kind of state, \textbf{thread state} (denoted by $\ownThread{\threadstate}$, where $\threadstate \subset \mathrm{ThreadId}$).
+%% From this, we derive $\tid{i}$, an exclusive token representing one thread. Only $\fork{}$ creates new thread id tokens.
+%% \begin{align*}
+%% \ownThread{\threadstate} \cdot \ownThread{\threadstate'} &\vs \bot \\
+%% \tid{i} \cdot \tid{i} &\vs \bot
+%% \end{align*}
+%% For all of this to make sense, we also add the ability to execute view shifts around fork.
+%% This enables us to put thread ids into an invariant:
+%% \begin{mathpar}
+%% \infer
+%% {P \vs \ownThread{\threadstate} \ast P'
+%% \\
+%% \hoare{P'}{e}{\top}
+%% \\
+%% \ownThread{\threadstate \uplus i} \vs Q
+%% }
+%% %-------------------------------------------
+%% {\hoare{\later P \ast \later R}{\fork{e}}{i. Q \ast R}}
+%% \end{mathpar}
+%% where $Q$ can mention $i$. \janno{add masks}
\ No newline at end of file
diff --git a/lang.tex b/lang.tex
new file mode 100644
index 0000000000000000000000000000000000000000..dd4e00da6fe79309a978cd0cc5478c3f6105d12b
--- /dev/null
+++ b/lang.tex
@@ -0,0 +1,192 @@
+\section{Instantiating Iris}
+
+\paragraph{Expressions and Evaluation Contexts}
+Our expressions are those of GPS.
+\textbf{Note} that we have two fork constructs. One of them, $\gfork\!\!$, mirros the
+fork expression of GPS and is responsible for creating new processors.
+The second one, $\fork\!\!$, will be used later to concurrently run non-deterministic
+inter-processor communication.
+\janno{Clean this up}
+%
+\begin{align*}
+ \loc \in \Loc ::={}& \ldots \\
+ \expr \in \Expr ::={}&
+ \val \in \Nat
+ \walt \ealloc{\blocks}
+ \walt \eload{\rtype}{\loc}
+ \walt \estore{\wtype}{\loc}{\val}
+ \walt \escas{\loc}{\val}{\val} \\
+ & \walt \gfork \expr \walt \fork \expr \\
+ &
+ \walt \elet{\var}{\expr}{\expr'}
+ \walt \erepeat{\expr}
+ \walt \Some \expr
+ \walt \None
+ \\
+ K \in \ECTX ::={}& \cdot \walt \elet{x}{K}{e} \walt \erepeat{K}
+\end{align*}
+However, the expressions we present to Iris are defined as follows: \[\IExpr = \Expr \times \ThreadId.\]
+
+\paragraph{Physical State}
+\begin{align*}
+ \state \in \Sigma &\eqdef \recordSig[\sbuf][\Sigma_B][\sind][\Sigma_I][\stime][\Sigma_T]
+ & \mbox{(Physical State)}\\
+ \Sigma_B &\eqdef W^{\ast} & \mbox{(Buffer State)} \\
+ W &\eqdef \recordSig[\weloc][\Loc][\weval][\Value][\wetime][\Time] &\; \mbox{(Write event)} \\
+ \Sigma_I &\eqdef \Nat \times \Nat \fpfn \Nat & \mbox{(Index State)}\\
+ \Sigma_T &\eqdef \Loc \fpfn \Nat &\; \mbox{(Timestamp server)} \\
+\end{align*}
+
+
+\paragraph{Atomic stepping relation}
+Essentially as in the SRA paper, with one exception:
+%% \begin{enumerate} %
+%% The original SRA paper has a fixed number of processors. We'd like to generalize that to better fit Iris' style of concurrency.
+%% Therefore,
+%% \item prefork (\textbf{new}):
+%% \begin{align*}
+%% \state; \prefork(\expr) \rightarrow_\thread \fork(\expr) ; \state' & \qquad \text{ if } (\state', \thread') = \textlog{newproc}(\state, \thread)
+%% \end{align*}
+%% where $\textlog{newproc}$ performs the necessary actions to add a new processor as a clone of $\thread$. \\
+%% \item
+We added a new expression called $\eprocess$ that attempts to import a new write event from a random processor into another random processor's buffer.
+It may ignore the write event it found if that event is outdated.
+$\eprocess$ always reduces to $()$.
+Intuitively, this combines SRA's \textbf{process} and \textbf{skip} in a single expression.
+
+The machine step relation is split into two: one with associated events and one without. The former is used for every expression that changes the machine state except $\eprocess$, whereas the latter is used exclusively for $\eprocess$.
+\\
+Example reductions:
+\begin{mathpar}
+ \def\lstate{(\state_B, \state_I, \state_T)}
+ \inferH{LOAD}%
+ {\mr{\state_B(\proc)}{(\loc, \val, \_)}}%
+ {\lstate; (\eload{\rtat}{\loc}, \proc) \rightarrow \lstate; (\val, \proc)}%
+ %
+ \and\inferH{STORE}%
+ {\state_B' = \Cupd\state_B[\proc -::> (\loc, \val, \state_T(\loc)+1)]
+ \\
+ \state_T' = \Iupd\state_T[\loc -+> 1]
+ }%
+ {\lstate; (\estore{\wtat}{\loc}{\val}, \proc) \rightarrow
+ (\state_B', \state_I, \state_T'); (\unitval, \proc)}%
+ %
+ \and\inferH{SCAS-OK}
+ {\mr{\state_B(\proc)}{(\loc, \val_o, \state_T(\loc))}
+ \\ \state_B' = \state_B[\proc \pointsto (\loc, \val_n, \state_T'(\loc)) :: \state_B(\proc)]
+ \\ \state_T' = \state_T[\loc \pointsto \state_T(\loc)+1]}
+ {\lstate; (\escas{\loc}{\val_o}{\val_n}, \proc) \rightarrow (\state_B', \state_I, \state_T'); (\Some{1}, \proc)}
+ %
+ \and\inferH{SCAS-FAIL}
+ {\mr{\state_B(\proc)}{(\loc, \val_r, \state_T(\loc))}
+ \\ \val_r \neq \val_o
+ }
+ {\lstate; (\escas{\loc}{\val_o}{\val_n}, \proc) \rightarrow \lstate; (\Some{0}, \proc)}
+ %
+ \and\inferH{SCAS-OLD}
+ {\mr{\state_B(\proc)}{(\loc, \_, t)}
+ \\ t < \state_T(\loc)
+ }
+ {\lstate; (\escas{\loc}{\val_o}{\val_n}, \proc) \rightarrow \lstate; (\None, \proc)}%
+ %
+ \and\inferH
+ {PROCESS-OK}
+ {\proc \neq \procB
+ \\ k = \state_I(\proc, \procB)
+ \\ \length{\state_B(\procB)} > k
+ \\ (\loc, \val, \ts) = \state_B(\procB)_k
+ \\ \bnew{\state_B(\proc)}{(\loc, \val, \ts)}
+ }
+ {\lstate; (process, \proc) \rightarrow
+ (\fpfnupd{\state_B}{\proc}{(\loc,\val,\ts) :: \state_B(\proc)},
+ \fpfnupd{\state_I}{(\proc, \procB)}{k+1}, \state_T)
+ ; ((), \proc)}
+ %
+ \and\inferH
+ {PROCESS-SKIP}
+ {\proc \neq \procB
+ \\ k = \state_I(\proc,\procB)
+ \\ \length{\state_B(\procB)} > k
+ \\ (\loc, \val, \ts) = \state_B(\procB)_k
+ \\ \neg \bnew{\state_B(\proc)}{(\loc, \val, \ts)}
+ }
+ {\lstate; (process, \proc) \rightarrow
+ (\state_B, \fpfnupd{\state_I}{(\proc,\procB)}{k+1}, \state_T)
+ ; ((), \proc)}
+ %
+ \and\inferH
+ {PROCESS-ALONE}
+ {\dom{\state_B} = \emptyset \lor \Exists \procB. \dom{\state_B} = \set{\procB}}
+ {\lstate; (process, \proc) \rightarrow
+ (\state_B, \state_I, \state_T)
+ ; ((), \proc)}
+ %
+ \and\inferH
+ {PROCESS-BUSYBEAVER}
+ {\All \procB \in \dom{\state_B}. \state_I(\proc, \procB) = \length{\state_B(\procB)}}
+ {\lstate; (process, \proc) \rightarrow
+ (\state_B, \state_I, \state_T)
+ ; ((), \proc)}
+\end{mathpar}
+\\
+To illustrate the impact of the $\ThreadId$ component in $\IExpr$, we give the reduction rule of fork. This rule is the only one in which the $\ThreadId$ plays an important role.
+In addition, it showcases the new way to do fork in Iris.
+Note how the right-hand side of the reduction lists two expressions.
+The second expressions represents the ``forked'' thread.
+
+We have to take care of ``cloning'' the original processor and everything that
+is related to it in the physical state.
+%
+\janno{This rule is a little long}
+%% \end{enumerate}
+\begin{mathpar}
+ \inferH{FORK}
+ {\proc \in \dom{\state.\sbuf} \\
+ \procB \not\in \dom{\state.\sbuf} \\
+ }
+ {(\state_B, \state_I, \state_T); (\gfork{e}, \proc)
+ \rightarrow
+ (\Fupd\state_B[\procB -> \state_B(\proc)],
+ \Fupd{%
+ \Fupd\state_I[\proc, \procB -> \length{\state_B(\proc)}]%
+ }[\All \proc'. \procB, \proc' -> \state_I(\proc, \proc')],
+ \state_T
+ ); (\procB, \proc); (e, \procB)}
+\end{mathpar}
+%
+Additionally, we have the second fork expression, which will not create a new
+processor.
+Instead, it creates an Iris thread which will run in the context of the original processor.
+\begin{mathpar}
+ \inferH{GFORK}
+ {\proc \in \dom{\state.\sbuf}}
+ {\state; (\fork{e}, \proc)
+ \rightarrow
+ \state; (\unitval, \proc); (e, \proc)}
+\end{mathpar}
+
+\paragraph{\textlog{atomic} on expressions}
+
+\begin{align*}
+ &\textlog{atomic}((\eload{\rtype}{\loc}, \proc)) \\
+ &\textlog{atomic}((\estore{\wtype}{\expr}{\expr'}, \proc)) \\
+ &\textlog{atomic}((\escas{\loc}{V_O}{\val_n}, \proc)) \\
+ &\textlog{atomic}((\gfork{e}, \proc))
+\end{align*}
+
+\paragraph{Monoids}
+We split the construction of ghost space into two layers.
+%
+\begin{enumerate}
+\item
+ We introduce lower bounds for buffers so that the buffers can be updated concurrently.
+ At the same time, we introduce logical per-location histories.
+ In these, we keep track of the timestamps, values, and the committing processor's buffer (including the new write event).
+ We call the entries of these histories historic events.
+\item
+ The last layer adds STS encodings of GPS protocols.
+ The STS states are lists of protocol states paired with historic events.
+ The STS invariant will tie the STS state to the previous layer's histories.
+\end{enumerate}
+
+We introduce the required monoids step-by-step while explaining and proving every layer of abstraction.
\ No newline at end of file
diff --git a/layer1.tex b/layer1.tex
new file mode 100644
index 0000000000000000000000000000000000000000..7fdb3bc0dcc3f303933f10adbada56cb8dd8204d
--- /dev/null
+++ b/layer1.tex
@@ -0,0 +1,541 @@
+\pagebreak
+\section{Layer 1}
+Our first layer will introduce lower bounds on processor buffers.
+We introduce a new monoid $\GMB \eqdef \auth{\Nat \fpfn \OrdHist(\Loc \times \Value \times \Time, <^{=\Loc}_{\Time})}$.
+$\OrdHist$ has only duplicable elements that represent lower bounds on the buffers.
+
+In addition, we introduce a definite history for every location. These histories consist of a list of buffers.
+Every buffer in $\loc$'s part of the map represents a write event to location $\loc$ in that the buffer is a snapshot
+of the committing processor's buffer at the time of the write access, including the newly preoduced write event.
+%\janno{This is confusing. TODO: talk about MO}
+\begin{align*}
+ \GH \eqdef \auth{\Loc \fpfn \ex{\List(\OrdList(\Loc \times \Value \times \Time, <^{=\Loc}_{\Time})}}
+\end{align*}
+%
+We write $\head^2(\hist)$ to refer to the first entry of the first buffer in a
+locations's history $\hist$.
+
+We impose a consistency condition:
+every write event in a processor's buffer has to be justified by a write event in the respective location's history.
+
+\[\begin{array}{rlr}
+ \PSInv \eqdef{}& \Exists \state_I, \state_T, \fMB, \fH. \ownPhys{(\fMB, \state_I, \state_T)} \ast \oMB{\fMB} \ast \oH{\fH} \\
+ & {}\ast \always \PS((\fMB, \state_I, \state_T), \fMB, \fH) \\
+ \PS(\state, \fMB, \fH) \eqdef{}& \SInv(\state.B, \state.I, \state.T) \land \HInv(\state.T, \fH)
+ \land \DBHInv(\fMB, \fH) \\
+ \SInv(\SProcs, \SIndex, \STime) \eqdef{}
+ & \dom{\SIndex} = \dom{\SProcs}^2 \\
+ & {}\land \All \proc \in \dom{\SProcs}, (\loc, \_, \ts) \in \SProcs(\proc). \ts \le \STime(\loc) \\
+ &{}\land \All (\proc,\procB) \in \dom{\SIndex}. \\
+ & \begin{array}{r@{}l}%
+ & \SIndex(\proc, \procB) \le \length{\SProcs(\procB)} \\
+ {}\land{}& \SProcs(\proc) \bsup \btake(\SProcs(\procB),\SIndex(\proc,\procB))
+ \end{array}%
+ \\
+ \HInv(\STime, \fH) \eqdef{}& \dom{\fH} = \dom{\STime} \\
+ & {}\land \All \loc \in \dom{\fH}. \\
+ & \begin{array}{@{\qquad}l}
+ \length{\fH(\loc)} > 0 \\
+ {}\implies \head^2(\fH(\loc)).\wetime = \STime(\loc)
+ \end{array}
+ \\
+ \buf \lesssim \fH \eqdef{}& \All \buf_0, \loc, \val, \ts. \buf = \_ \doubleplus (\loc, \val, \ts) :: \buf_0
+ \implies \Exists \buf'_0 \bsub \buf_0. (\loc,\val,\ts)::\buf'_0 \in \fH(\loc)
+ \\
+ \DBHInv(\fMB, \fH) \eqdef{}& \All {{\proc \in \dom{\fMB}}}. \fMB(\proc) \lesssim \fH
+\end{array}\]
+%
+\paragraph{Intuition} The $\lesssim$ relation enforces that, if processor $\proc$ commits a write event, every processor that learns of this write event
+must also have at least processor $\proc$'s knowledge (in terms of write events) up to that event.
+This knowledge is represented by the buffer in the location's history.
+
+Interestingly, we do not rely on enforcing exactly this condition.
+Instead, we simply do not record the origin of a write event.
+Only the processor's buffer is recorded.
+It is not necessary to know that the buffers in the locations history came from
+a processor.
+%
+\subsection{Laws}
+%
+We give the reasoning principles we want to use in this layer.
+The island name $\ips$ referes to the island that stores $\PSInv$.
+%
+\[\begin{array}{lrcl}
+ &\bseen{\proc}{\buf} &\implies{}& \always\bseen{\proc}{\buf} \\
+ \buf \bsub \buf_0 \vdash& \bseen{\proc}{\buf} &\implies{}& \bseen{\proc}{\buf_0} \\
+ &\bseen{\proc}{\buf_1} \ast \bseen{\proc}{\buf_2} &\vs[\ips][\ips]& \begin{cases} \bseen{\proc}{\buf} & \mbox{ if } b = \max_\bsup(\buf_1, \buf_2) \\ \bot & \mbox{ ow. } \end{cases} \\
+ &\lhist{\loc}{\hist} \ast \lhist{\loc}{\hist'} &\implies{}& \bot \\
+ &\lhist{\loc}{\buf::\hist} &\vs[\ips][\ips]& \lhist{\loc}{\buf::\hist} \ast \head(\buf).L = \loc \\
+ \mr{\buf}{(\loc, \val, \ts)} \vdash& \bseen{\proc}{\buf} \ast \lhist{\loc}{\hist} &\vs[\ips][\ips]& \always (\buf \bsup \btill{\hist(\loc)}{\ts}) \ast \lhist{\loc}{\hist}
+\end{array}\]
+%
+%
+\subsection{Definitions}
+%
+\begin{align*}
+ \bseen{\proc}{\buf} \eqdef{}& \always\kmq{\proc}{\buf} \\
+ \lhist{\loc}{\hist} \eqdef{}& \oh{\loc}{\hist} \\
+ \btill{\hist}{\ts} \eqdef{}& \argmax_{\substack{i < \length{\hist} \\ \mr{\hist_i}{(\loc, \_, \ts}}} \hist_i
+\end{align*}
+%
+%
+\subsection{GPS Assertions}
+The lower bounds on buffers introduced in this layer are sufficient to provide
+the interpretation of GPS triples.
+Note that we frequently leave out the return value $\val$ when the expression
+reduces to $\unitval$.
+%
+\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' \bsub \buf. \bseen{\proc}{\buf'} \ast \intr {Q}(\buf')} \\
+\end{align*}
+%
+%
+\subsection{Triples}
+We provide the first set of triples.
+The pre- and post-conditions of the triples are not monotone buffer predicates.
+Thus, the triples are \textbf{not} representable in GPS.
+
+\begin{mathpar}
+ \inferH{AtomicRead}{}{\ereadHyp \vdash \hoare{\ereadPreB
+ }{\eload{\rtat}{\loc}, \proc}{\ereadPostB } } \\
+ \and\inferH{AtomicWrite}{}{\estoreHyp \vdash \hoare{\estorePreB
+ }{\estore{\wtat}{\loc}{\val}, \proc}{\estorePostB }} \\
+ \and\inferH{CAS}{}{\ecasHyp \vdash \hoare{\ecasPreB }{\escas{\loc}{\val_o}{\val_n}}{\ecasPostB }} \\
+ \and\inferH{Process}{}{\processHyp \vdash \hoare{\top}{\eprocess, \proc}{\processPostB}}
+ \and\inferH{GFork}{\gforkU}
+ {\gforkHyp \vdash \hoare{\gforkPreB}{\gfork(e), \proc}{\gforkPostB}} \\
+ \and\inferH{Fork}{\forkU}
+ {\forkHyp \vdash \hoare{\forkPreB}{\fork(e), \proc}{\forkPostB}} \\
+\end{mathpar}
+
+
+\subsection{Proofs}
+%
+\subsubsection{Lemmas}
+\begin{lem}[$\SInv$:Store]\label{lem:store-sinv}
+ $\All \SProcs, \SIndex, \STime, \proc_0 \in \dom{\SProcs}, \loc_0 \in
+ \dom{\STime}, \val_0.$
+ \def\STimeB{\Iupd\STime[\loc_0 -+> 1]}%
+ \def\SProcsB{\Cupd\SProcs[\proc_0 -::> (\loc_0, \val_0, \STime(\loc)+1)]}%
+ \begin{align*}
+ \SInv(\SProcs, \SIndex, \STime) \Ra \SInv(
+ & \SProcsB, \\
+ & \SIndex, \\
+ & \STimeB).
+ \end{align*}
+ \begin{proof}~\\
+ We have $\dom{\SIndex} = \dom{\SProcs}^2$,
+ $\All \proc \in \dom{\SProcs}, (\loc, \_, \ts) \in \SProcs(\proc). \ts \le \STime(\loc)$,~\\
+ and $\All (\proc, \procB) \in \dom{\SIndex}.
+ \SIndex(\proc, \procB) \le \length{\SProcs(\procB)} \land \SProcs(\proc) \bsup \btake(\SProcs(\procB), \SIndex(\proc, \procB))$.
+ \begin{enumerate}
+ \item $\dom{\SIndex} = \dom{\SProcs}^2$. By assumption.
+ \item Suppose $\proc \in \dom{\SProcs}$, $(\loc, \val, \ts) \in \SProcsB(\proc)$.~\\
+ To show: $\ts \le \STimeB(\loc)$.
+ \begin{enumerate}
+ \item $\proc = \proc_0$, $(\loc',\val',\ts) = (\loc_0, \val_0, \STime(\loc)+1)$: ~\\
+ We have $\ts = \STimeB(\loc_0) = \STime(\loc_0)+1$.
+ \item Otherwise:
+ by assumption.
+ \end{enumerate}
+
+ \item Suppose $(\proc, \procB) \in \dom{\SIndex}$.
+ \begin{enumerate}
+ \item To show: $\SIndex(\proc, \procB) \le \length{\SProcsB(\procB)}$.~\\
+ By assumption and the fact that we only increase the length of a buffer.
+ \item To show: $\SProcs(\proc) \bsup \btake(\SProcsB(\procB), \SIndex(\proc, \procB))$.~\\
+ By assumption and the fact that we only grow a buffer (but not the
+ indices).
+ \end{enumerate}
+ \qedhere
+ \end{enumerate}
+ \end{proof}
+\end{lem}
+%
+%
+\begin{lem}[$\HInv$:Store]\label{lem:store-hinv}
+ $\All \STime, \fH, \loc_0 \in \dom{\STime}, \val_0, \buf_0.$
+ \def\STimeB{\Iupd\STime[\loc_0 -+> 1]}%
+ \def\fHB{\Cupd\fH[\loc_0 -::> ((\loc_0, \val_0, \STime(\loc_0)+1) :: \buf_0)]}%
+ \begin{align*}
+ \HInv(\STime, \fH) \Ra \HInv(
+ & \STimeB, \\
+ & \fHB)
+ \end{align*}
+ \begin{proof}~\\
+ We have $\dom{\fH} = \dom{\STime}$,
+ and $\All \loc \in \dom{\fH}. \head^2(\fH(\loc)).\wetime = \STime(\loc)$.
+ \begin{enumerate}
+ \item To show: $\dom{\fH} = \dom{\STimeB}$. By assumption.
+ \item Suppose $\loc \in \dom{\fHB}$, $\length{\fHB{\loc}} > 0$. ~\\
+ To show: $\head^2(\fHB(\loc)).\wetime = \STimeB(\loc)$.
+ \begin{enumerate}
+ \item $\loc = \loc_0$. By reflexivity.
+ \item Otherwise: by assumption.
+ \end{enumerate}
+ \qedhere
+ \end{enumerate}
+ \end{proof}
+\end{lem}
+%
+%
+\begin{lem}\label{lem:lesssim-mono}
+ $\All \buf, \fH_1, \fH_2. $~\\
+ $(\All \loc. \Exists \hist. \fH_2(\loc) = \fH_1(\loc) \mdoubleplus \hist)
+ \Ra \buf \lesssim \fH_1 \Ra \buf \lesssim \fH_2$
+ \begin{proof}~\\
+ Suppose $\buf_0, \loc, \val, \ts. \buf = \_ \doubleplus (\loc, \val, \ts) ::
+ \buf_0$.~\\
+ To show: $\Exists \buf'_0 \bsub \buf_0. (\loc,\val,\ts)::\buf'_0 \in
+ \fH_2(\loc)$.~\\
+ We have $\buf_1 \bsub \buf_0$ \st $(\loc, \val, \ts) :: \buf_1 \in
+ \fH_1(\loc)$.~\\
+ We pick $\buf'_0 \eqdef \buf_1$.~\\
+ By assumption, $(\loc, \val, \ts) :: \buf'_0 \in \fH_2(\loc)$.
+ \end{proof}
+\end{lem}
+%
+%
+\begin{lem}[$\DBInv$:Store]\label{lem:store-dbinv}
+ $\All \fMB, \fH, \proc_0 \in \dom{\fMB}, \loc_0 \in \dom{\fH}, \val_0, \ts_0, \buf_0.$
+ \def\fHB{\Cupd\fH[\loc_0 -::> ((\loc_0, \val_0, \ts_0) :: \buf_0)]}%
+ \def\fMBB{\Cupd\fMB[\proc_0 -::> (\loc_0, \val_0, \ts_0)]}%
+ \begin{align*}
+ \DBInv(\fMB, \fH) \Ra \DBInv(
+ & \fMBB, \\
+ & \Fupd\fH[\loc_0 -> (\loc_0, \val_0, \ts_0) :: \fMB(\proc_0)])
+ \end{align*}
+ \begin{proof}~\\
+ We have $\All {{\proc \in \dom{\fMB}}}. \fMB(\proc) \lesssim \fH$. ~\\
+ Suppose $\proc \in \dom{\fMBB}$. ~\\
+ To show: $\fMBB(\proc) \lesssim \fHB$.
+ \begin{enumerate}
+ \item $\proc = \proc_0$:~\\
+ To show: $(\loc_0, \val_0, \ts_0) :: \buf_0 \lesssim \fHB$.~\\
+ Suppose $\buf_1, \loc \in \dom{\fHB}, \val, \ts$.~\\
+ Suppose $(\loc_0, \val_0, \ts_0) :: \buf_0 = \_
+ \doubleplus (\loc, \val, \ts) :: \buf_1$.~\\
+ To show: $\Exists \buf_1' \bsup \buf_1. (\loc, \val, \ts) :: \buf_1 \in \fHB(\loc)$.
+ \begin{enumerate}
+ \item $\buf_1 = \buf_0$:~\\
+ We have $(\loc, \val, \ts) = (\loc_0, \val_0, \ts_0)$.~\\
+ To show $\Exists \buf_1' \bsup \buf_0. (\loc_0, \val_0, \ts_0) :: \buf_1'
+ \in ((\loc_0, \val_0, \ts_0) :: \buf_0) :: \fH(\loc)$.~\\
+ Trivial with $\buf_1 \eqdef \buf_0$.
+ \item $\buf_1 \neq \buf_0$: by Lemma~\ruleref{lem:lesssim-mono} and assumption.
+ \end{enumerate}
+ \item $\proc \neq \proc_0$: by assumption.
+ \qedhere
+ \end{enumerate}
+ \end{proof}
+\end{lem}
+%
+
+\begin{lem}\label{lem:process-small}
+ $\All \fMB, \fH, \proc \in \dom{\fMB}, \buf, \loc, \val,
+ \ts$.
+ \def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
+ \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
+ \def\tup{(\loc, \val, \ts)}%
+ \[\begin{array}{@{}r@{}l}
+ \multicolumn{2}{l}{%
+ \fMB(\proc) \bsup \buf%
+ \land \buf' \bsub \buf \land \tup :: \buf' \in \fH(\loc)} \\
+ {}\implies{} & \tup :: \fMB(\proc) \bsup \tup :: \buf \\
+ & {} \land \Exists \buf'' \bsub \fMB(\proc). \tup :: \buf'' \in \fH(\loc)
+ \end{array}\]
+\begin{proof}
+ We have
+ $\fMB(\proc) \bsup \buf$,
+ $\buf' \bsub \buf$, and $\tup :: \buf' \in \fH(\loc)$.
+ \begin{enumerate}
+ \item To show: $\tup :: \fMB(\proc) \bsup \tup :: \buf$. By assumption, and
+ monotonicity of $\bsup$.
+ \item To show:
+ $\Exists \buf'' \bsub \fMB(\proc). \tup :: \buf'' \in \fH(\loc)$.~\\
+ We pick $\buf'' \eqdef \buf'$. ~\\
+ By transitivity we have $\fMB(\proc) \bsup \buf'$.~\\
+ By assumption, $\tup :: \buf \in \fH(\loc)$.
+ \qedhere
+ \end{enumerate}
+\end{proof}
+\end{lem}
+%
+\begin{lem}[$\DBInv+\SInv$:Process]\label{lem:process-ok}
+ $\All \fMB, \fH, \proc, \procB \in \dom{\fMB}, \buf, \loc, \val,
+ \ts$.
+ \def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
+ \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
+ \def\tup{(\loc, \val, \ts)}%
+ \[\begin{array}{@{}r@{}l}
+ \multicolumn{2}{l}{\SInv(\fMB, \SIndex, \STime) \land \DBInv(\fMB, \fH)} \\
+ {}\land{} & \state_I(\proc,\procB) < \length{\fMB(\procB)} \\
+ {}\land{} & \bnew{\fMB(\proc)}{\fMB(\procB)_{\state_I(\proc,\procB)}} \\
+ {}\implies{}& \SInv(\fMBB, \SIndexB, \STime) \\
+ & {} \land \DBInv(\fMBB, \fH)
+ \end{array}\]
+\begin{proof}
+\janno{TODO} using Lemma~\ruleref{lem:process-small}
+\end{proof}
+\end{lem}
+%
+\begin{lem}[$\DBInv+\SInv$:Process]\label{lem:process-skip}
+ $\All \fMB, \fH, \proc, \procB \in \dom{\fMB}, \buf, \loc, \val,
+ \ts$.
+ \def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
+ \def\tup{(\loc, \val, \ts)}%
+ \[\begin{array}{@{}r@{}l}
+ \multicolumn{2}{l}{\SInv(\fMB, \SIndex, \STime)} \\
+ {}\land{} & \state_I(\proc,\procB) < \length{\fMB(\procB)} \\
+ {}\land{} & \neg\bnew{\fMB(\proc)}{\fMB(\procB)_{\state_I(\proc,\procB)}} \\
+ {}\implies{}& \SInv(\fMB, \SIndexB, \STime)
+ \end{array}\]
+\begin{proof}
+Trivial. \janno{TODO}
+\end{proof}
+\end{lem}
+%
+%
+\subsubsection{\ruleref{AtomicRead}}
+%
+\begin{hproofenv}
+ Context: $\buf$, $\proc$, $\loc$, $\ts$, $\bseen{\proc}{\buf}$, $(\loc, \_,
+ \ts) \in \buf$~\\
+ \pline[\top]{\top}~\\
+ \begin{psubenv}{open $\ips$}
+ Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
+ Context: $\fMB(\proc) \bsup \buf$ \mbox{\by def. $\GMB$}~\\
+ Context: $\bseen{\proc}{\fMB(\proc)}$~\\
+ Context: $\Exists \val, \ts'. \mr{\fMB(\proc)}{(\loc, \val, \ts)}$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \mr{\fMB(\proc)}{(\loc, \val, \ts)}}~\\
+ \cdline{\eload{\rtat}{\loc}, \proc}~\\
+ \pline[-\set\ips]{\Ret \val'. \ownPhys{(\fMB, \state_I, \state_T)} \ast \val' = \val} \by ~\ruleref{LOAD}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{\Ret \val. \ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB
+ \ast \ofH \ast \mr{\fMB(\proc)}{(\loc, \val, \ts')}}
+ \end{psubenv}~\\
+ \pline[\top]{\Ret \val. \bseen{\proc}{\fMB(\proc)} \ast \mr{\fMB(\proc)}{(\loc, \val, \ts')} }
+\end{hproofenv}
+%
+%
+\subsubsection{\ruleref{AtomicWrite}}
+%
+\begin{hproofenv}
+ Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$~\\
+ \pline[\top]{\estorePreB}~\\
+ \pline[\top]{\intr{\estorePreB}(\buf)}~\\
+ \begin{psubenv}{open $\ips$}
+ Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
+ Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
+ Context: $\bseen{\proc}{\fMB(\proc)}$~\\
+ Context: $\fH(\loc) = \hist$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
+ \cdline{\eload{\rtat}{\loc}, \proc}~\\
+ Define: $\state_T' \eqdef \Iupd\state_T[\loc -+> 1]$~\\
+ \pline[-\set\ips]{\ownPhys{(\Cupd\fMB[\proc -::> (\loc, \val,
+ \state_T'(\loc))], \state_I, \state_T')}} \by ~\ruleref{STORE}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{\Ret \val. \ownPhys{(\Cupd\fMB[\proc -::> (\loc, \val,
+ \state_T'(\loc))], \state_I, \state_T')} \ast \ofMB \ast \ofH}~\\
+ Define: $\fMB' \eqdef \Cupd\fMB[\proc -::> (\loc, \val,
+ \state_T'(\loc))]$.~\\
+ Define: $\fH' \eqdef \Cupd\fH[(\loc -::> (\loc, \val, \state_T'(\loc))::\fMB(\proc))]$.~\\
+ \pline[-\set\ips]{\Ret \val. \ownPhys{(\fMB', \state_I, \state_T')} \ast \oMB{\fMB'} \ast \oH{\fH'}}
+ \by Ghost Update ~\\
+ Context: $\PS((\fMB', \state_I, \state_T'), \fMB', \fH')$ \by
+ Lemmas~\ruleref{lem:store-sinv},~\ruleref{lem:store-hinv}, and~\ruleref{lem:store-dbinv} ~\\
+ \end{psubenv}~\\
+ \pline[\top]{\Ret \val. \bseen{\proc}{\fMB(\proc)} \ast \mr{\fMB(\proc)}{(\loc, \val, \ts')} } ~\\
+ \pline[\top]{\Ret\val. \ereadPostBI} \with $\buf' = \fMB(\proc)$, $\ts' = \ts'$.
+\end{hproofenv}
+%
+%
+\subsubsection{\ruleref{CAS}}
+%
+\begin{hproofenv}
+ Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$, $\loc$, $\hist$,
+ $(\loc, \_, \_) \in \buf$~\\
+ \pline[\top]{\estorePreB}~\\
+ \begin{psubenv}{open $\ips$}
+ Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH
+ \ast \lhist{\loc}{\hist}}~\\
+ Define: $(\_, \val, \ts) \eqdef \head^2(\hist)$~\\
+ Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
+ Context: $\bseen{\proc}{\fMB(\proc)}$, $\fH(\loc) = \hist$, $\ts = \state_T(\loc)$~\\
+ \begin{psubenv}{$(\loc, \val, \ts) \in \fMB(\proc)$}
+ Case: $(\loc, \val, \ts) \in \fMB(\proc)$~\\
+ Context:
+ $\mr{\fMB(\proc)}{(\loc, \val, \ts)}$ \by $\SInv(\fMB, \state_I, \state_T)$~\\
+ Context: $\fMB(\proc) \bsup \head(\hist)$ \by $\DBInv(\fMB, \fH)$~\\
+ \begin{psubenv}{$\val = \val_o$}
+ Case: $\val = \val_o$~\\
+ Context: $\head^2(\hist).\weval = \val_o$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast
+ \mr{\fMB(\proc)}{(\loc, \val_o, \ts)}}~\\
+ \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc} ~\\
+ Define: $\state_T' \eqdef \Iupd\state_T[\loc -+> 1]$~\\
+ Define: $\fMB' \eqdef \Cupd\fMB[\proc -::> (\loc, \val_n,
+ \state_T'(\loc))]$.~\\
+ \pline[-\set\ips]{\Ret\val'. \val' = \Some 1 \ast \ownPhys{(\fMB', \state_I, \state_T')}} \by ~\ruleref{SCAS-OK}
+ \end{psubenv}~\\
+ Define: $\fH' \eqdef \Cupd\fH[(\loc -::> (\loc, \val_n,
+ \state_T'(\loc))::\fMB(\proc))]$.~\\
+ \pline[-\set\ips]{\Ret\val'. \val' = \Some 1 \ast \ownPhys{(\fMB',
+ \state_I, \state_T')} \ast \oMB{\fMB'} \ast \oH{\fH'} \ast
+ \lhist{\loc}{\fH'(loc)}}~\\
+ Context: $\PS((\fMB', \state_I, \state_T'), \fMB', \fH')$ \by
+ Lemmas~\ruleref{lem:store-sinv},~\ruleref{lem:store-hinv}, and~\ruleref{lem:store-dbinv} ~\\
+ \end{psubenv}~\\
+ \hline
+ \begin{psubenv}{$\val \neq \val_o$}
+ Case: $\val \neq \val_o$~\\
+ Context: $\head^2(\hist).\weval \neq \val_o$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast
+ \mr{\fMB(\proc)}{(\loc, \val, \ts)}}~\\
+ \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc} ~\\
+ \pline[-\set\ips]{\Ret\val'. \val' = \Some 0 \ast \ownPhys{(\fMB,
+ \state_I, \state_T)}} \by ~\ruleref{SCAS-FAIL}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{\Ret\val'. \val' = \Some 0 \ast \ownPhys{(\fMB,
+ \state_I, \state_T)} \ast \ofMB \ast \ofH \ast \lhist{\loc}{\fH(\loc)}}~\\
+ \end{psubenv}
+ \end{psubenv}~\\
+ \hline
+ \begin{psubenv}{$(\loc, \val, \ts) \notin \fMB(\proc)$}
+ Case: $(\loc, \val, \ts) \notin \fMB(\proc)$~\\
+ Context: $\Exists \ts' < \ts.
+ \mr{\fMB(\proc)}{(\loc, \_, \ts')}$ \by $\SInv(\fMB,
+ \state_I, \state_T)$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast
+ \mr{\fMB(\proc)}{(\loc, \_, \ts')}}~\\
+ \cdline{\ecas{\loc}{\val_o}{\val_n}, \proc} ~\\
+ \pline[-\set\ips]{\Ret\val'. \val' = \None \ast \ownPhys{(\fMB,
+ \state_I, \state_T)}} \by \ruleref{SCAS-OLD}~\\
+ \end{psubenv}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{%
+ \begin{array}{r@{}l}%
+ \multicolumn{2}{l}{
+ \Ret\val'. \Exists \fMB', \fH', \state_T'.
+ \ownPhys{(\fMB', \state_I, \state_T)}
+ \ast \oMB{\fMB'}
+ \ast \oH{\fH'}
+ \ast \fMB'(\proc) \bsup \fMB(\proc)
+ } \\
+ \multicolumn{2}{l}{
+ {}\ast \lhist{\loc}{\fH'(\loc)} \ast \always \PSInv((\fMB', \state_I, \state_T'), \fMB', \fH')
+ } \\
+ \multicolumn{2}{l}{
+ \ast \left(
+ (\val' = \Some 1 \ast \fH'(\loc) = \fMB' :: \fH(\loc)
+ \ast \fMB'(\proc) \bsup \fH(\loc)
+ \ast \head^2(\fH(\loc)) = \val_o)
+ \right.
+ } \\
+ {}\lor{} & (\val = \Some 0 \ast \fH' = \fH
+ \ast \fMB'(\proc) \bsup \hist
+ \ast \head^2(\fH(\loc)) \neq \val_o) \\
+ {}\lor{} & \left. (\val = \None \ast \fH' = \fH) \right)
+ \end{array}%
+ }
+ \end{psubenv}
+ \pline[\top]{%
+ \begin{array}{r@{}l}%
+ \multicolumn{2}{l}{
+ \Ret\val'. \Exists \buf' \bsup \buf, \hist'.
+ \bseen{\proc}{\buf'}
+ \ast \lhist{\loc}{\hist'}
+ } \\
+ \multicolumn{2}{l}{
+ \ast \left(
+ (\val' = \Some 1 \ast \hist' = \buf' :: \hist
+ \ast \buf' \bsup \hist
+ \ast \head^2(\fH(\loc)) = \val_o)
+ \right.
+ } \\
+ {}\lor{} & (\val = \Some 0
+ \ast \hist' = \hist
+ \ast \buf' \bsup \hist
+ \ast \head^2(\hist) \neq \val_o) \\
+ {}\lor{} & \left. (\val = \None \ast \hist' = \hist) \right)
+ \end{array}%
+ }
+\end{hproofenv}
+%
+\subsubsection{Process}
+%
+\begin{hproofenv}
+ Context: $\buf$, $\proc$, $\bseen{\proc}{\buf}$~\\
+ \pline[\top]{\top}~\\
+ \begin{psubenv}{open $\ips$}
+ Context: $\PS((\fMB, \state_I, \state_T), \fMB, \fH)$~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)} \ast \ofMB \ast \ofH}~\\
+ Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
+ \begin{psubenv}{\ruleref{PROCESS-OK}}
+ Case: $\Exists \procB. \length{\fMB(\procB)} > \state_I(\proc, \procB)$~\\
+ (cont'd): $(\loc, \val, \ts) = \fMB(\procB)_{\state_I(\proc, \procB)}$~\\
+ (cont'd): $\bnew{\fMB(\proc)}{(\loc, \val, \ts)}$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
+ \cdline{\eprocess, \proc}~\\
+ Define: $\fMB' \eqdef \Cupd\fMB[\loc -::> (\loc, \val, \ts)]$~\\
+ Define: $\state_I' \eqdef \Iupd\state_I[\proc, \procB -+> 1]$~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB', \state_I', \state_T)}} \by \ruleref{PROCESS-OK}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB', \state_I', \state_T)}
+ \ast \oMB{\fMB'}
+ \ast \oH{\fH}} \by ghost update~\\
+ Context: $\PSInv((\fMB', \state_I', \state_T), \fMB', \fH)$ \by Lemma~\ruleref{lem:process-ok}~\\
+ \end{psubenv}~\\
+ \hline
+ \begin{psubenv}{\ruleref{PROCESS-SKIP}}
+ Case: $\Exists \procB. \length{\fMB(\procB)} > \state_I(\proc, \procB)$~\\
+ (cont'd): $(\loc, \val, \ts) = \fMB(\procB)_{\state_I(\proc, \procB)}$~\\
+ (cont'd): $\neg\bnew{\fMB(\proc)}{(\loc, \val, \ts)}$~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
+ \cdline{\eprocess, \proc}~\\
+ Define: $\state_I' \eqdef \Iupd\state_I[\proc, \procB -+> 1]$~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I', \state_T)}} \by \ruleref{PROCESS-SKIP}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I', \state_T)}
+ \ast \oMB{\fMB}
+ \ast \oH{\fH}} \by ghost update~\\
+ Context: $\PSInv((\fMB, \state_I', \state_T), \fMB, \fH)$ \by Lemma~\ruleref{lem:process-skip}~\\
+ \end{psubenv}
+ \\\hline
+ \begin{psubenv}{all other cases}
+ Case: (depends on specific case)~\\
+ \begin{psubenv}{Frame}
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
+ \cdline{\eprocess, \proc}~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}}~\\
+ \by~\ruleref{PROCESS-ALONE} or~\ruleref{PROCESS-BUSYBEAVER}
+ \end{psubenv}~\\
+ \pline[-\set\ips]{\ownPhys{(\fMB, \state_I, \state_T)}
+ \ast \oMB{\fMB}
+ \ast \oH{\fH}}~\\
+ Context: $\PSInv((\fMB, \state_I, \state_T), \fMB, \fH)$ \by assumption~\\
+ \end{psubenv}~\\
+ \pline[\top]{\Exists \fMB', \state_I'.
+ \ownPhys{(\fMB', \state_I', \state_T)}
+ \ast \always\PSInv((\fMB', \state_I', \state_T), \fMB', \fH)
+ }~\\
+ \end{psubenv}
+ \pline[\top]{\top}
+\end{hproofenv}
+%
+%
+%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "appendix"
+%%% End:
diff --git a/layer1def.tex b/layer1def.tex
index 52d4b67bfd1abbe6dc02b63bac76975cd623ad30..01acfa9358ec46ec1a6b518b6a5792d56a856edd 100644
--- a/layer1def.tex
+++ b/layer1def.tex
@@ -60,7 +60,7 @@
\newcommand\gforkUHyp{\bseen{\procB}{\buf'}}
\newcommand\gforkUPreB{Q}
\newcommand\gforkUPostB{\top}
-\newcommand\gforkU[0]{\gforkUHyp \vdash \hoare{\gforkUPreB}{\expr, \procB}{\gforkUPostB}}
+\newcommand\gforkU[0]{\All \procB, \buf'. \gforkUHyp \vdash \hoare{\gforkUPreB}{\expr, \procB}{\gforkUPostB}}
\newcommand\gforkHyp{\bseen{\proc}{\buf}}
\newcommand\gforkPreB{Q}
\newcommand\gforkPostB{\Ret\rho. \Exists \buf' \bsup \buf. \bseen{\proc}{\buf'} \ast \bseen{\procB}{\buf'}}
@@ -68,6 +68,7 @@
\newcommand\forkUHyp{\bseen{\proc}{\buf'}}
\newcommand\forkUPreB{Q}
\newcommand\forkUPostB{\top}
+\newcommand\forkU[0]{\All \buf'. \forkUHyp \vdash \hoare{\forkUPreB}{\expr, \proc}{\forkUPostB}}
\newcommand\forkHyp{\bseen{\proc}{\buf}}
\newcommand\forkPreB{Q}
\newcommand\forkPostB{\Ret\unitval. \Exists \buf' \bsup \buf. \bseen{\proc}{\buf'}}
diff --git a/layer2.tex b/layer2.tex
new file mode 100644
index 0000000000000000000000000000000000000000..54292173fb740da8cde03c10c3cad3a4c134d892
--- /dev/null
+++ b/layer2.tex
@@ -0,0 +1,220 @@
+\clearpage
+\newcommand{\Prot}[0]{\mathrm{PROT}}
+\newcommand{\ststs}[0]{\mathit{ss}}
+\section{Layer 2: Adding Protocols}
+In this last and final layer, we add GPS protocols.
+Protocols are encoded by Iris state transition systems (STS).
+The key idea here is that the every protocol STS will keep track of the entire history of a single location.
+We do this to retain the duplicable part of GPS's protocol interpretation of past states.
+The STS interpretation will own the locations history from the previous layer.
+
+Formally, an STS is given by a pair of states and a transition relation, $(S, \ra)$.
+In our case, the STS state space \textbf{should} augment the location's history with a protocol state for every entry.
+However, since we ultimately wont care about the value and timestamp of write events, we reduce the state space to a pair of a protocol state and a buffer.
+The projection to the state component results in a monotone list w.r.t $\sqsupseteq_\tau$:
+\begin{align*}
+ \mathbb{S}(S) \eqdef \OrdList(S \times \monlist(\Loc \times \Value \times \Time, <^{=\Loc}_{\Time}), \sqsubseteq_{S,\tau})
+\end{align*}
+
+For every protocol $\tau$ with state space $\tau.S$ we define the monoid $\Prot_\tau \eqdef \STSMon{\mathbb{S}(\tau.S)}$.
+
+The transition relation is defined as follows
+\begin{mathpar}
+ \infer{\\}{\nil \ra_{\Prot{\tau}} ((\stst, \buf)::nil)}
+
+ \infer{\stst \ra_\tau \stst' }{((\stst, \buf)::\ststs) \ra_{\Prot{\tau}} ((\stst',\buf')::(\stst, \buf)::\ststs) }
+\end{mathpar}
+
+\janno{TODO: mapping to ghost names}
+
+We do not make use of Iris' tokens for STSs.
+Therefore, we adopt a simplified notational convention for STS assertions.
+In addition, we also define a shorthand asserting that the protocol has been in a particular state at some point.
+\newcommand{\STSat}[2]{\textcolor{OliveGreen}{\ownGhost{#1}{[#2]}}}
+\newcommand{\STSone}[2]{\textcolor{OliveGreen}{\ownGhost{#1}{#2}}}
+\begin{align*}
+ \STSat{\gamma_\tau}{\ststs} \eqdef&\; \textcolor{OliveGreen}{\ownGhost{\gamma_\tau}{(\ststs, \uparrow \{\ststs\}, \emptyset) : \Prot{\tau}}} \\
+ \STSone{\gamma_\tau}{\stst, \buf} \eqdef&\; \STSat{\gamma_\tau}{(\stst, \buf) :: \_}
+\end{align*}
+
+The invariants in this level are given by the usual STS invariants. We pick the following interpretation predicates.
+\newcommand{\Cons}[0]{\mathrm{Consistent}}
+\def\td{{\always\tau_{\mathrm{dup}}}}%
+\def\intd{\always\intr{\tau_{\mathrm{dup}}}}%
+\def\int{\intr{\tau}}%
+\begin{align*}
+ \varphi_\tau(\ststs) \eqdef&\; \Exists h. \oh{\loc}{h} \ast \xi(\ststs, h) \land \Cons(\ststs, h) \land \bigwedge_{\substack{\mathclap{(\stst, \buf) \in \ststs}\\\val = \hd{\buf}.V}} \intd(\stst, \val)(\buf) \\
+ \\
+ \xi(\ststs) \eqdef&\;
+ \begin{cases}
+ \int(\stst, \hd{\buf}.V)(\buf) &\mbox{ if } \ststs = (\stst, \buf) :: \_ \\
+ \top & \mbox{ ow. }
+ \end{cases}
+ \\
+ %% \ststs \star h \eqdef&\;
+ %% \begin{cases}
+ %% (\stst, \val, \buf) :: (\ststs' \star h') & \mbox{ if } \ststs = (\ststs, \buf)::\ststs' \land h = (\val, \ts, \buf') :: h' \\
+ %% nil & \mbox{ ow.}
+ %% \end{cases} \\
+ \Cons(\ststs, h) \eqdef&\;
+ \begin{cases}
+ \Cons(\ststs', h') & \mbox{ if } \ststs = (\stst, \buf) :: \ststs' \land h = \buf :: h' \\
+ \top & \mbox{ if } \ststs = \nil \land h = \nil \\
+ \bot & \mbox{ ow. }
+ \end{cases} \\
+\end{align*}
+
+In our proofs, we do not care about the exact buffer $\buf$ used to justify a protocol state.
+However, we need to know that the processor's buffer is at least as big (in terms of $\bsup$) as that buffer.
+Additionally, the exact value of $\gamma_\tau$ is not important.
+Using Iris' new invariant scheme, we get away with just one existential as we re-use $\gamma$ to encode the island used for the STS assertion.
+Thus, the interpretation of the GPS protocol assertion becomes the following:
+\begin{align*}
+ \intr{\protAt{\loc}{\stst}{\tau}} \; \buf \eqdef&\; \Exists \gamma, \buf_0 \bsub \buf. \STSone{\gamma}{\stst,\buf_0} \land \nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}(\tau.S), \varphi_\tau, \gamma)}
+\end{align*}
+
+Note how this assertion intuitively encodes what it means to know a lower bound on the GPS protocol state:
+knowing at least as much as the processor who advanced the protocol to that particular state.
+
+
+\janno{TODO: $\iota \in$ Something}
+
+While hiding $\gamma$ (and the island name) makes for a nice interface, it has counterintuitive consequences:
+we do not know a priori that two protocol assertions on $\loc$ are in any way related, as they could be talking about different $\gamma$ and $\iota$.
+Therefore, we need to manually establish the usual rules for protocol assertions such as:
+\begin{align*}
+ \protAt{\loc}{\stst_0}{\tau} \ast \protAt{\loc}{\stst_1}{\tau} \vs&\;
+ \begin{cases}
+ \protAt{\loc}{\stst}{\tau} & \mbox{ if } \max \{\stst_0, \stst_1\} = \stst \\
+ \bot & \mbox{ ow.} \\
+ \end{cases}
+\end{align*}
+\janno{TODO: masks}
+\paragraph{Note:} we have to rely on view shifts here because the lemma is not provable without opening invariants.
+
+
+\subsection{Triples}
+The triples for $\fork{e}$ and $\eprocess$ are not affected by the abstractions introduced in this layer.
+
+Instead of stating triples in terms of GPS protocol assertions, we stay on a lower level of abstraction to simplify the proofs.
+The translation to fully flegded GPS triples is straight-forward and will happen in another layer.
+
+%% \def\ereadH {\intr{\All \stst' \sqsupseteq_\tau \stst, \val. \tau(\stst, \val) \ast P \implies \always Q}(\buf)}
+%% \def\ereadPreC {\kmq{\proc}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\tau}{\stst, \buf_0} \ast \intr P(\buf)}%
+%% \def\ereadPostC {\Ret\val'. \; \Exists \buf' \bsup \buf, \stst' \sqsupseteq_\tau \stst. \kmq{\proc}{\buf'} \ast \STSone{\gamma_\tau}{\stst', \buf'} \ast \intr{\always Q}(\buf')}%
+\def\ereadPreC {\kmq{\proc}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\tau}{\stst, \buf_0}}%
+\def\ereadPostC {\Ret\val.
+ \begin{aligned}
+ & \Exists \buf' \bsup \buf. \kmq{\proc}{\buf'} \ast \hd{\buf'} = (\loc, \val, \_) \\
+ & \ast \Exists \stst' \sqsupseteq_\tau \stst. \STSone{\gamma_\tau}{\stst', \buf'} \ast \intd(\stst', \val)(\buf')
+ \end{aligned}
+}
+
+\def\estoreHA {\intr{ P \ast P' \vs \tau(\stst'', \val) * Q}(\buf)}
+\def\estoreHB {\intr{\qpure \left( \All \stst' \sqsupseteq_\tau \stst. \tau(\stst', \_) \ast P \implies \stst'' \sqsupseteq_\tau \stst' \right)}(\buf)}
+\def\estoreHC {\intr{\qpure \left( \All \stst, \val. \tau(\stst, \val) \implies \td(\stst, \val) \right)}(\buf)}
+\def\estoreH {\later \varphi(\ststs \doubleplus (\stst, \buf_0) :: \_) \ast \P \vs \Exists q' \bsup \buf. \stst'' \sqsupseteq \hd{\stst' \doubleplus (\stst, \buf_0) :: \_}.S \ast \later \varphi((\stst'', \buf'))}
+\def\estorePreC {\kmq{\proc}{\buf} \ast \Exists \buf_0 \bsub \buf. \STSone{\gamma_\tau}{\stst, \buf_0} \ast \intr{\qpure P \ast P'}(\buf)}%
+\def\estorePostC {\Exists \buf' \bsup \buf. \kmq{\proc}{\buf'} \ast \STSone{\gamma_\tau}{\stst'', \buf'} \ast \intr Q(\buf')}%
+\def\ecasHA {\intr{\All \stst' \sqsupseteq_\tau \stst. \tau(\stst', \val_o) \ast P \vs \Exists \stst'' \sqsupseteq_\tau \stst. \tau(\stst'', \val_n) * Q}(\buf)}
+\def\ecasHB {\intr{\left( \All \stst, \val. \tau(\stst, \val) \implies \td(\stst, \val) \right)}(\buf)}
+%\def\ecasHB {\intr{\All \stst'' \sqsupseteq_\tau \stst. \All y \neq \val_o. \td(\stst', y) \ast P \implies \always R}(\buf)}
+%\def\ecasHC {\intr{\All \stst'' \sqsupseteq_\tau \stst. \td(\stst', \_) \ast P \implies \always S}(\buf)}
+\def\ecasPreC {
+ \begin{aligned}
+ \kmq{\proc}{\buf} \ast \Exists \buf_0 \bsub q. \STSone{\gamma_\tau}{\stst, q_0} \ast \intr P(q)
+ \end{aligned}
+}
+\def\ecasPostC {\Ret\val'.
+ \begin{aligned}
+ &\; \Exists \buf' \bsup \buf, \stst'' \sqsupseteq_\tau \stst. \kmq{\proc}{\buf'} \ast \STSone{\gamma_\tau}{\stst'', \buf'} \\
+ \ast &\; \intrl(\val' = \Some 1\ast Q) \\
+ \lor &\; \;(\val' = \Some 0 \ast (\mr{\buf'}{\loc}).V \neq \val_o \ast \td(\stst'', (\mr{\buf'}{\loc}).V)) \\
+ \lor &\; \;(\val' = \None)\intrr(\buf')
+ \end{aligned}
+}
+\begin{mathpar}
+ \inferH{AtomicRead2}{}{\mathllap{\nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}, \varphi_\tau, \gamma_\tau)}} \vdash \hoare{\ereadPreC }{\eload{\rtat}{\loc}, \proc}{\ereadPostC } } \\
+ \inferH{AtomicWrite2}{\estoreHA \\ \estoreHB \\ \estoreHC }{\mathllap{\nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}, \varphi_\tau, \gamma_\tau)}} \vdash \hoare{\estorePreC }{\estore{\wtat}{\loc}{\val}, \proc}{\estorePostC }} \\
+ \inferH{CAS2}{\ecasHA \\ \ecasHB }{\mathllap{\nknowInv{\iota.\gamma}{\STSInv(\mathbb{S}, \varphi_\tau, \gamma_\tau)}} \vdash \hoare{\ecasPreC }{\escas{\loc}{v_o}{v_n}, \proc}{\ecasPostC }} \\
+ %\inferH{Fork2}{\All \rho. \hoare{\forkUPreC }{e, \rho}{\forkUPostC }}{\hoare{\forkPreC }{\fork(e), \proc}{\forkPostC }} \\
+ %\axiomH{Process2}{\hoare{\processPreC }{\eprocess, \proc}{\processPostC }}
+\end{mathpar}
+
+\subsection{Proofs}
+\paragraph{\ruleref{AtomicRead2}:}
+We have a lower bound $\buf$ on processor $\proc$'s buffer and a lower bound on the protocol state of location $\loc$, $\STSone{\gamma_\tau}{\stst,\buf_0}$.
+We know $\buf_0 \bsub \buf$.
+Thus, there is at least one write event for $\loc$ in $\buf$ at some timestamp $\ts$.
+We are now in a position to apply the previous layer's triple.
+However, we first open the STS invariant and immediately frame off everything we acquired by doing this.
+We apply the layer-2 triple for $\eload{\rtat}{\loc}$.
+The return value is $\val$ and we learn a new lower bound on $\proc$'s buffer, $\buf' \bsup \buf$, s.t. $\mr{\buf'}{\loc} = (\loc, \val, \ts)$ with $\ts' \ge \ts$.
+We re-introduce the contents of the STS invariant, stripping off the later modality.
+This yields $\bigwedge_{(\stst, \buf'_0) \in \ststs} \intd(\stst, \hd{\buf'_0}.V)(\buf'_0)$ where $\ststs$ is the authoritative state of the STS.
+We also own the history $h$ for $\loc$.
+From \ruleref{Consistency} and \ruleref{LastEvent}, there exists $\buf'_0 \bsub q'$ s.t. $\buf'_0 \in h$ and $\hd{\buf'_0} = (\loc, \val, \ts',)$.
+From $\Cons(\ststs, h)$, there exists $\stst'$ s.t. $(\stst', \buf'_0) \in \ststs$.
+We extract the correpsonding lower bound $\STSone{\gamma_\tau}{\stst', \buf'_0}$.
+We have $\intd(\stst', \val)(\buf'_0)$.
+From $\ts' \ge \ts$, monotonicity of $h$, monotonicity $\ststs$, and $\Cons(\ststs, h)$, we have $\stst' \sqsupseteq_\tau \stst$. % \janno{TODO: MAKE THIS A LEMMA! IT IS HORRIBLE! ARGH!}
+This completes the proof
+
+\paragraph{\ruleref{AtomicWrite2}:}
+We assume $\mathbf{H_1} \eqdef \estoreHA $, $\mathbf{H_2} \eqdef \estoreHB $, and $\mathbf{H_3} \eqdef \estoreHC $.
+We have a lower bound on processor $\proc$'s buffer, $\buf$, and a lower bound on the protocol state $\stst$ at $\buf_0 \bsub \buf$.
+We own $\intr{\qpure P \ast P'}$ at $\buf$. % and, by $H_{3}$ at $\nil$.
+We open the STS invariant and frame off everything except $\loc$'s history $h$.
+We apply \ruleref{AtomicWrite}.
+Our new lower bound on $\proc$'s buffer is $\buf' \bsup \buf$ with $\hd{\buf'} = (\loc, \val, \ts)$.
+$\loc$'s history is now $\buf' :: h$.
+We re-introduce the remaining contents of the STS interpretation.
+The authoritative GPS protocol state is $\stst' \sqsupseteq_\tau \stst$ at $\buf'_0$.
+We own $\int(\stst',\hd{\buf'_0}.V)(\buf'_0)$.
+We apply $\mathbf{H_2}$ to get $\stst'' \sqsupseteq_\tau \stst'$ (making use of $\qpure P$ in the process, without consuming it).
+We perform a frame-preserving update to change the authoritative state to $\stst''$ at $\buf'$ and extract a corresponding lower bound.
+We apply $\mathbf{H_3}$ to get $\intd(\stst', \_)(\buf')$.
+Finally, we apply $\mathbf{H_1}$ to acquire $\intr{\tau(\stst'', v)(\buf') \ast Q}(\buf')$, giving up both $\qpure P$ and $P'$.
+We close the STS invariant.
+This concludes the proof.
+
+\paragraph{\ruleref{CAS2}}
+We assume $\mathbf{H_1} \eqdef \ecasHA $ and $\mathbf{H_2} \eqdef \ecasHB $.
+We have a lower bound on processor $\proc$'s buffer, $\buf$, and a lower bound on the protocol state, $\stst$ at $\buf_0 \bsub \buf$.
+We own $P$ at $\buf$.
+We open the STS invariant and frame off everything except for the authoritative STS state $\ststs$ and the authoritative GPS protocol state $\stst' \sqsupseteq_\tau \stst$ at $\buf'_0$, and $\loc$'s history $h$.
+By $\Cons$ we have $\buf'_0 = \hd{h}$.
+By \ruleref{LastEvent} we have $\hd{q_0} = (\loc, \_, \_)$.
+Thus, by $\buf_0 \bsub \buf$ there exists $(\loc, \_, \_) \in \buf$.
+We apply \ruleref{CAS}.
+The return value is $\val'$.
+We have $\buf' \bsup \buf$ and $h'$.
+$\buf'$ is the new lower bound of $\proc$'s buffer.
+We own $\oh{\loc}{h'}$.
+We re-introduce the remaining contents of the STS invariant, stripping off laters where applicable.
+This gives us $\int(\stst',\hd{\buf'_0}.V)(\buf'_0)$ and $\bigwedge_{(\stst, \buf'_0) \in \ststs} \intd(\stst, \hd{\buf'_0}.V)(\buf'_0)$.
+There are three cases:
+\begin{enumerate}
+\item{$\val' = \Some{1}$:}
+ We know $\hd{\buf'} = (\loc, \val_n, \hd{\hd{h}}.T+1)$ and $h' = \buf' :: h$.
+ We also know $\buf' \bsup \hd{h}$ and, thus, $\buf' \bsup \buf'_0$.
+ Applying $\mathbf{H_2}$, we acquire $\td(\stst', \val_o)$ at $\buf'_0$.
+ Finally, we use $\mathbf{H_1}$ to get $\stst'' \sqsupseteq_\tau \stst'$ such that $\intr{\tau(\stst'', \val_n) \ast Q}(\buf')$.
+ We change the authoritative protocol state to $\stst''$ at $\buf'$.
+ This suffices to re-establish the STS invariant.
+\item{$\val' = \Some{0}$:}
+ No write event was generated, i.e. $h' = h$.
+ We know $\buf' \bsup \hd{h}$ (and, thus, $\buf' \bsup \buf'_0$), and $(\mr{\buf'}{\loc}).V \neq \val_o$.
+ We duplicate $\intd(\stst', \buf'_0)$.
+ Since we changed neither state nor history the STS invariant is still true.
+\item{$\val' = \None$:}
+ Everything remains as is.
+\end{enumerate}
+We close the STS invariant.
+This concludes the proof.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "appendix"
+%%% End:
diff --git a/setup.tex b/setup.tex
index 4710db7ce95b8a5487ed8226d5deac24a4df77a7..5e7b2818f91f1118ca9083d0995b804396b7b9ac 100644
--- a/setup.tex
+++ b/setup.tex
@@ -40,6 +40,8 @@
\newcommand{\loc}{\ell}
\newcommand{\thread}{i}
\newcommand{\ts}{t}
+\newcommand{\we}{e}
+\newcommand{\werel}{<^{=\Loc}_{\Time}}
\newcommand{\Time}{\mathit{Time}}
\newcommand{\stst}{s}
@@ -1237,7 +1239,7 @@ $\infer{#1}{#2}$
%\newcommand{\region}[4]
-\newcommand{\SET}[2]{
+\newcommand{\setComp}[2]{
\left\{%
#1%
\;\middle|\;%
@@ -1441,16 +1443,42 @@ $\infer{#1}{#2}$
\newcommand\st{s.t.\ }
-
\NewDocumentCommand\recordSig{d[] d[] d[] d[] d[] d[] d[] d[]}{%
\begin{array}[t]{@{} r@{\;} r @{} l @{} r}%
- \IfNoValueF{#1}{\left\{\vphantom{#1#2#3#4#5#6#7#8}\right. :{}& #2}%
- \IfNoValueF{#3}{,\\ & #3 :{}& #4}%
- \IfNoValueF{#5}{,\\ & #5 :{}& #6}%
- \IfNoValueF{#7}{,\\ & #7 :{}& #8}%
+ \IfNoValueF{#1}{\left\{\vphantom{#1#2#3#4#5#6#7#8}\right. \in{}& #2}%
+ \IfNoValueF{#3}{,\\ & #3 \in{}& #4}%
+ \IfNoValueF{#5}{,\\ & #5 \in{}& #6}%
+ \IfNoValueF{#7}{,\\ & #7 \in{}& #8}%
+ \,\left.\vphantom{#1#2#3#4#5#6#7#8}\right\}%
+ \end{array}%
+}
+\NewDocumentCommand\record{d[] d[] d[] d[] d[] d[] d[] d[]}{%
+ \begin{array}[t]{@{} r@{\;} r @{} l @{} r}%
+ \IfNoValueF{#1}{\left\{\vphantom{#1#2#3#4#5#6#7#8}\right. :={}& #2}%
+ \IfNoValueF{#3}{,\\ & #3 :={}& #4}%
+ \IfNoValueF{#5}{,\\ & #5 :={}& #6}%
+ \IfNoValueF{#7}{,\\ & #7 :={}& #8}%
\,\left.\vphantom{#1#2#3#4#5#6#7#8}\right\}%
\end{array}%
}
+\NewDocumentCommand\irecordSig{d[] d[] d[] d[] d[] d[] d[] d[]}{%
+ %\begin{array}[t]{@{} r@{\;} r @{} l @{} r}%
+ \IfNoValueF{#1}{\left\{\vphantom{#1#2#3#4#5#6#7#8}\right. #1 \in #2}%
+ \IfNoValueF{#3}{, #3 \in #4}%
+ \IfNoValueF{#5}{, #5 \in #6}%
+ \IfNoValueF{#7}{, #7 \in #8}%
+ \left.\vphantom{#1#2#3#4#5#6#7#8}\right\}%
+ %\end{array}%
+}
+\NewDocumentCommand\irecord{d[] d[] d[] d[] d[] d[] d[] d[]}{%
+ %\begin{array}[t]{@{} r@{\;} r @{} l @{} r}%
+ \IfNoValueF{#1}{\left\{\vphantom{#1#2#3#4#5#6#7#8}\right. #1 := #2}%
+ \IfNoValueF{#3}{, #3 := #4}%
+ \IfNoValueF{#5}{, #5 := #6}%
+ \IfNoValueF{#7}{, #7 := #8}%
+ \left.\vphantom{#1#2#3#4#5#6#7#8}\right\}%
+ %\end{array}%
+}
\newcommand\Nat{\mathbb{N}}
@@ -1462,6 +1490,7 @@ $\infer{#1}{#2}$
\newcommand{\weval}{\mathrm{val}}
\newcommand{\wetime}{\mathrm{time}}
+\newcommand*{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
\newcommand{\newinv}[1]{\expandafter\newcommand\csname #1\endcsname{\mathtt{#1}}}
@@ -1480,7 +1509,9 @@ $\infer{#1}{#2}$
\newcommand{\Value}[0]{\mathit{Val}}
-\newcommand{\Loc}[0]{\ensuremath{\mathit{Loc}}}
+\newcommand{\Loc}[0]{\mathit{Loc}}
+\newcommand{\Buf}[0]{\mathit{Buffer}}
+\newcommand{\WriteEvent}[0]{\mathit{Event}}
\newcommand{\duplicable}[1]{\textrm{duplicable}\; {#1}}
\newcommand{\exc}[0]{\textsc{Ex}}
@@ -1580,9 +1611,12 @@ $\infer{#1}{#2}$
\newcommand{\Dup}[1]{\ensuremath{\textsc{Dup}(#1)}}
\newcommand{\ex}[1]{\ensuremath{\textsc{Ex}(#1)}}
\newcommand{\DC}[1]{\ensuremath{#1\downarrow}}
-\newcommand{\listty}[0]{\ensuremath{\textsc{List}}}
-\newcommand{\monlist}[0]{\ensuremath{\textsc{MonList}}}
-\newcommand{\monhist}[0]{\ensuremath{\textsc{MonDupList}}}
+\newcommand{\List}[0]{\textsc{List}}
+\newcommand{\OrdList}[0]{\textsc{OrdList}}
+\newcommand{\OrdBuf}[0]{\textsc{OrdBuffer}}
+\newcommand{\OrdHist}[0]{\textsc{OrdHist}}
+\newcommand{\Monoid}[0]{\mathcal{M}}
+\newcommand{\BufMon}[0]{\textsc{BufMon}}
%% GPS Interpretation
@@ -1619,3 +1653,8 @@ $\infer{#1}{#2}$
\newcommand{\GPSPred}[1]{#1 \rightarrow \GPSProp}
\newcommand{\qpure}{\dagger}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "appendix"
+%%% End: