diff --git a/framework.tex b/framework.tex
index 3929752e965bf72b57ffa1a3ff04e85b858a2d38..dfe35930a2872a17e83ed9280f5ef5dda575fdbc 100644
--- a/framework.tex
+++ b/framework.tex
@@ -75,21 +75,28 @@
\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 &::=
+ \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 \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}
+ 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.\]
@@ -161,7 +168,7 @@ Example reductions:
\\ k = \state_I(\proc, \procB)
\\ \length{\state_B(\procB)} > k
\\ (\loc, \val, \ts) = \state_B(\procB)_k
- \\ \Exists \ts' < \ts. \mr{\state_B(\proc)}{(\loc, \_, \ts')}
+ \\ \bnew{\state_B(\proc)}{(\loc, \val, \ts)}
}
{\lstate; (process, \proc) \rightarrow
(\fpfnupd{\state_B}{\proc}{(\loc,\val,\ts) :: \state_B(\proc)},
@@ -174,7 +181,7 @@ Example reductions:
\\ k = \state_I(\proc,\procB)
\\ \length{\state_B(\procB)} > k
\\ (\loc, \val, \ts) = \state_B(\procB)_k
- \\ \Exists \ts' \ge \ts. \mr{\state_B(\proc)}{(\loc, \_, \ts')}
+ \\ \neg \bnew{\state_B(\proc)}{(\loc, \val, \ts)}
}
{\lstate; (process, \proc) \rightarrow
(\state_B, \fpfnupd{\state_I}{(\proc,\procB)}{k+1}, \state_T)
@@ -196,18 +203,39 @@ Example reductions:
\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:
+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}
- {
- \pi \in \state.\theta
- \\
- \rho \not\in \state.\theta
- \\
- \state' = \kw{ext}^\rho_\pi(\state)
+ \inferH{GFORK}
+ {\proc \in \dom{\state.\sbuf} \\
+ \procB \not\in \dom{\state.\sbuf} \\
}
- {\state; (\fork{e}, \pi) \rightarrow \fpfnupd{\state'}{\rho}{\state'.P(\pi)}; (\rho, \pi); (e, \rho)}
+ {(\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}
@@ -216,7 +244,7 @@ In addition, it showcases the new way to do fork in Iris:
&\textlog{atomic}((\eload{\rtype}{\loc}, \pi)) \\
&\textlog{atomic}((\estore{\wtype}{\expr}{\expr'}, \pi)) \\
&\textlog{atomic}((\escas{\loc}{V_O}{\val_n}, \pi)) \\
- &\textlog{atomic}((\fork{e}, \pi))
+ &\textlog{atomic}((\gfork{e}, \pi))
\end{align*}
\paragraph{Monoids}
@@ -313,7 +341,7 @@ every write event in a processor's buffer has to be justified by a write event i
&{}\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)}
+ {}\land{}& \SProcs(\proc) \bsup \btake(\SProcs(\procB),\SIndex(\proc,\procB))
\end{array}%
\\
\HInv(\STime, \fH) \eqdef{}& \dom{\fH} = \dom{\STime} \\
@@ -382,9 +410,9 @@ We skip the binder of the predicate whenever the meta-level assertions does not
\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{Fork2}{\hoare{\forkUPreB }{e}{\forkUPostB }}{\hoare{\forkPreB
- }{\fork(e), proc}{\forkPostB }} \\
+ \and\inferH{Process2}{}{\processHyp \vdash \hoare{\top}{\eprocess, \proc}{\processPostB}}
+ \and\inferH{Fork2}{\forkUHyp \vdash \hoare{\forkUPreB}{e, \procB}{\forkUPostB}}
+ {\forkHyp \vdash \hoare{\forkPreB}{\gfork(e), \proc}{\forkPostB}} \\
\end{mathpar}
@@ -516,14 +544,27 @@ We skip the binder of the predicate whenever the meta-level assertions does not
\def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
\def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
\def\tup{(\loc, \val, \ts)}%
- \begin{align*}
- \multicolumn{2}{l}{\fMB(\proc) \bsup \buf
- \land (\Exists \buf' \bsub \buf. \tup :: \buf' \in \fH(\loc))} \\
+ \[\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{align*}
-\begin{proof}
-\janno{TODO}
+ \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}
%
@@ -533,13 +574,31 @@ We skip the binder of the predicate whenever the meta-level assertions does not
\def\fMBB{\Cupd\fMB[\proc -::> (\loc, \val, \ts)]}%
\def\SIndexB{\Iupd\SIndex[\proc, \proc_1 -+> 1]}%
\def\tup{(\loc, \val, \ts)}%
- \begin{align*}
+ \[\begin{array}{@{}r@{}l}
\multicolumn{2}{l}{\SInv(\fMB, \SIndex, \STime) \land \DBInv(\fMB, \fH)} \\
- \multicolumn{2}{l}{\state_I(\proc,\proc_1) < }
- {}\implies{}
- \end{align*}
+ {}\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}
+\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}
%
@@ -610,11 +669,11 @@ We skip the binder of the predicate whenever the meta-level assertions does not
\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}~\\
- Context: $\fMB(\proc) \bsup \buf$ \by def. $\GMB$~\\
- Context: $\bseen{\proc}{\fMB(\proc)}$, $\fH(\loc) = \hist$~\\
+ \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: $\ts = \state_T(\loc)$~\\
+ 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:
@@ -730,30 +789,60 @@ We skip the binder of the predicate whenever the meta-level assertions does not
\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): $\Exists \ts' < \ts. \mr{\fMB(\proc)}{(\loc, \_, \ts')}$~\\
+ (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)}}~\\
- \end{psubenv}
- \end{psubenv}
+ \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}}
- \pline[-\set\ips]{}~\\
+ 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
+ \\\hline
\begin{psubenv}{all other cases}
- \pline[-\set\ips]{}~\\
- \end{psubenv}
- \pline[\top]{\top}~\\
+ 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}
%
%
%
+\clearpage
\newcommand{\Prot}[0]{\mathrm{PROT}}
\newcommand{\ststs}[0]{\mathit{ss}}
\section{Layer 2: Adding Protocols}
diff --git a/layer1def.tex b/layer1def.tex
index bff8c0805a51fb3526971b8d6e91e2202d4b3043..cd8bb89c345b2cd037e28005994abcc0997a7894 100644
--- a/layer1def.tex
+++ b/layer1def.tex
@@ -57,10 +57,13 @@
\lor &\; (\val' = \None \ast \hist' = \hist)
\end{aligned}
}
-\newcommand\forkUPreB {Q}
-\newcommand\forkUPostB {\top}
-\newcommand\forkPreB {Q}
-\newcommand\forkPostB {\Ret\rho. \lam \buf'. \bseen{\rho}{\buf'}}
+\newcommand\forkUHyp{\bseen{\procB}{\buf'}}
+\newcommand\forkUPreB{Q}
+\newcommand\forkUPostB{\top}
+\newcommand\forkHyp{\bseen{\proc}{\buf}}
+\newcommand\forkPreB{Q}
+\newcommand\forkPostB{\Ret\rho. \Exists \buf' \bsup \buf. \bseen{\proc}{\buf'} \ast \bseen{\procB}{\buf'}}
+
\newcommand\processHyp{\bseen{\proc}{\buf}}
-\newcommand\processPreB {\bseen{\proc}{\buf}}
-\newcommand\processPostB {\top}
\ No newline at end of file
+\newcommand\processPreB{\bseen{\proc}{\buf}}
+\newcommand\processPostB{\top}
\ No newline at end of file
diff --git a/setup.tex b/setup.tex
index 628be6e6b1c265d0fd64c92c86c95f0d27527468..4710db7ce95b8a5487ed8226d5deac24a4df77a7 100644
--- a/setup.tex
+++ b/setup.tex
@@ -1383,7 +1383,7 @@ $\infer{#1}{#2}$
\newcommand{\hproof}[1]{\vspace{0.5em}\hproofnospace{#1}\vspace{0.5em}} %
\newcommand\psub[2]{%
\begin{tabu}{ m{0.9em} | X[1,l,m] }%
- \begin{sideways}#1\end{sideways} &%
+ \begin{sideways}\;#1\;\end{sideways} &%
\tabubox{#2}%
\end{tabu}%
}%
@@ -1490,6 +1490,7 @@ $\infer{#1}{#2}$
\newcommand{\hd}[1]{\ensuremath{\mathrm{hd}(#1)}}
\newcommand\doubleplus{\mathbin{+\kern-1.0ex+}}
\newcommand\mdoubleplus{\mathbin{+\kern-1.0ex+}}
+\newcommand{\bnew}[2]{\mathrm{New}({#1}, {#2})}
\newcommand{\Some}[1]{\mathbf{Some}\;{#1}}
\newcommand{\None}[0]{\mathbf{None}}
@@ -1534,6 +1535,7 @@ $\infer{#1}{#2}$
\newcommand{\Expr}{\mathrm{Expr}}
\newcommand{\IExpr}{\mathrm{IExpr}}
\newcommand{\ThreadId}{\mathrm{ThreadId}}
+\newcommand{\gfork}[1]{\kw{gfork}\;{#1}}
\newcommand{\ownThread}[1]{\ensuremath{\ceil{#1}}}
\newcommand{\threadstate}[0]{\ensuremath{\xi}}