GFork proof, WIP

framework.tex

@@ -252,8 +252,7 @@ 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 by
-  processors and the communication process.
+  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.
@@ -353,7 +352,7 @@ every write event in a processor's buffer has to be justified by a write event i
     \DBHInv(\fMB, \fH) \eqdef{}& \All {{\proc \in \dom{\fMB}}}. \fMB(\proc) \lesssim \fH
 \end{array}\]
 %
-\paragraph{Intution} The $\lesssim$ relation enforces that, if processor $\pi$ commits a write event, every processor that learns of this write event
+\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.
 
@@ -399,10 +398,9 @@ reduces to $\unitval$.
 %
 %
 \subsection{Triples}
-We prove our first set of triples.
-This layer's triples are not sufficiently high-level enough to express their pre- and post-conditions purely in GPS assertions.
-Thus, we make use of the injection of predicates over buffers defined in Section~\ref{sec:new-assertions}.
-We skip the binder of the predicate whenever the meta-level assertions does not depend on the buffer. 
+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
@@ -411,8 +409,10 @@ We skip the binder of the predicate whenever the meta-level assertions does not
     }{\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}{\forkUHyp \vdash \hoare{\forkUPreB}{e, \procB}{\forkUPostB}}
-  {\forkHyp \vdash \hoare{\forkPreB}{\gfork(e), \proc}{\forkPostB}} \\
+  \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}
 
 
@@ -840,7 +840,13 @@ Trivial. \janno{TODO}
   \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}}

layer1def.tex

@@ -57,12 +57,20 @@
     \lor &\; (\val' = \None \ast \hist' = \hist)
   \end{aligned}
 }
-\newcommand\forkUHyp{\bseen{\procB}{\buf'}}
+\newcommand\gforkUHyp{\bseen{\procB}{\buf'}}
+\newcommand\gforkUPreB{Q}
+\newcommand\gforkUPostB{\top}
+\newcommand\gforkU[0]{\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'}}
+
+\newcommand\forkUHyp{\bseen{\proc}{\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\forkPostB{\Ret\unitval. \Exists \buf' \bsup \buf. \bseen{\proc}{\buf'}}
 
 \newcommand\processHyp{\bseen{\proc}{\buf}}
 \newcommand\processPreB{\bseen{\proc}{\buf}}