Commit 904f1c47 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge branch 'arrays' of gitlab.inria.fr:gmevel/cosmo into arrays

parents 88a6121f 44813a5f
\begin{figure}
\begin{codeblock}
\Let* \pipeline {g,f,\refXArray} {%
\LetIn \nbelems {\Length \refXArray} \\
\LetIn \refYQueue {\make\;\Unit} \\
\Fork* {%
\For* \idx 0 {\nbelems-1} {%
\LetIn x {\ArrayReadNA \refXArray \idx} \\
\LetIn y {f\;x} \\
\enqueue\;\refYQueue\;{z}
}
} \\
\LetIn \refZArray {\ArrayAllocNA \nbelems \Unit} \\
\For* \idx 0 {\nbelems-1} {%
\LetIn y {\dequeue\;\refYQueue} \\
\LetIn z {g\;y} \\
\ArrayWriteNA \refZArray \offset {z}
} ; \\
\refZArray
}
\end{codeblock}
\Description{\mocaml implementation of a pipeline.}
\caption{Implementation of a pipeline}
\label{fig:pipeline:impl}
\end{figure}
\begin{figure}
\[\begin{array}{rcl}
% the queue:
\gqueue
& :
& ...
% \authm requires an unitary cmra; here we omit \optionm
\\
% cursors of f and g:
\gcurf,\;\gcurg
& :
& \authm(\exm(\nat))
% \authm requires an unitary cmra; here we omit \optionm
\\ \hline
% invariant (outer):
\pipelineInv R
& \eqdef
& \Exists \queue, \gqueue, \gcurf, \gcurg. \queueInv \isep \knowInv{}{\pipelineInvInner R}
\\
% invariant (inner):
\pipelineInvInner R
& \eqdef &
%\\
%\multicolumn{3}{r}{%
\left\{\begin{array}{l}
\Exists \curf, \curg, \yElemViewListInv<\curg><\curf>*[].
\\ \quad \ISep{%
\curg \leq \curf
\isep \ownGhost \gcurf {\authfull \curf}
\isep \ownGhost \gcurg {\authfull \curg}
\cr \isQueue \emptyview \emptyview {\yElemViewListInv<\curg><\curf>}
\cr \displaystyle\Sep_{\curg \leq \idx < \curf}
\left(\wpre {g\;\yElem_\idx} {\Lam z. R\;\idx\;z}\right) \opat \view_\idx
}%end of the main \ISep of the invariant
\end{array}\right.% end of the definition of \queueInvInner
%}% end of \multicolumn
\\ \hline
% invariant local to thread f:
\pipelineF R \curf \refXArray \xElemList
& \eqdef
& \ISep{%
\curf \leq \nbelems
\isep \ownGhost \gcurf {\authfull \curf}
\cr \arraypointstoNA \refXArray \xElemList
\cr \displaystyle\Sep_{\curf \leq \idx < \nbelems}
\wpre {f\;x_\idx} {\Lam y. \wpre {g\;y} {\Lam z. R\;\idx\;z}}
}
\\ \hline
% invariant local to thread g:
\pipelineG R \curg \refZArray \zElemList
& \eqdef
& \ISep{%
\curg \leq \nbelems
\isep \ownGhost \gcurg {\authfull \curg}
\cr \arraypointstoNA \refZArray \zElemList
\cr \displaystyle\Sep_{0 \leq \idx < \curg}
R\;\idx\;z_\idx
}
\end{array}\]
\Description{Internal invariant of the pipeline.}
\caption{Internal invariant of the pipeline}
\label{fig:pipeline:invariant}
\end{figure}
\begin{figure}
\[\small\begin{array}{@{}l@{}}
\hoareV
{\hphantom{\Lam \refZArray. \Exists \zElemList*[].}
\haslength \refXArray \nbelems
\isep \arraypointstoNA \refXArray \xElemList
\isep \displaystyle\Sep_{0 \leq \idx < \nbelems}
%\hoare {} {f\;x_\idx} {\Lam y. \hoare {} {g\;y} {\Lam z. R\;\idx\;z}\vphantom{\displaystyle\sum}}
\wpre {f\;x_\idx} {\Lam y. \wpre {g\;y} {\Lam z. R\;\idx\;z}}
}
{\pipeline\;g\;f\;\refXArray}
{\Lam \refZArray. \Exists \zElemList*[].
\haslength \refZArray \nbelems
\isep \arraypointstoNA \refZArray \zElemList
\isep \displaystyle\Sep_{0 \leq \idx < \nbelems} R\;\idx\;z_\idx
}
\end{array}\]
\Description{A specification for the pipeline.}
\caption{A specification for the pipeline}
\label{fig:pipeline:spec}
\end{figure}
\begin{figure}
\[\small\begin{array}{@{}l@{}}
\infer{~}{\persistent{\queueInv}}
\qquad
\infer{~}{\objective{\isQueue \tview \hview \elemViewList}}
\\\\\\
\hoareV
{\seen\view_0}
{\make~\Unit}
{\Lam \queue. \Exists \gqueue.
\queueInv
\isep \isQueue {\view_0} {\view_0} {[]}
\isep \persistent{\queueInv}
}
\\\\\\
......
......@@ -91,6 +91,7 @@
\email{francois.pottier@inria.fr}
\begin{abstract}
% TODO:
%\input{abstract}
\end{abstract}
......@@ -105,6 +106,7 @@
\input{intro}
\input{lang}
\input{queue}
\input{pipeline}
% ------------------------------------------------------------------------------
% Bibliography.
......
......@@ -198,7 +198,15 @@
\newcommand{\Tuple}[1]{(#1)}
% concurrency:
\newcommand{\Fork}[1]{\texttt{fork}\;#1}
\NewDocumentCommand \Fork {sm} {%
\IfBooleanTF#1{%
\texttt{fork \{} \\
\quad \begin{codeblock} #2 \end{codeblock} \\
\texttt\}
}{%
\texttt{fork}\;#2%
}
}
% memory:
% accesses to references:
......@@ -242,6 +250,9 @@
\newcommand{\ArrayAllocAT}[2]{\texttt{array\AT}[#1]\;#2}
\newcommand{\ArrayAllocANY}[2]{\texttt{array\ACCMODEANY}[#1]\;#2}
% length of an array:
\newcommand{\Length}[1]{\texttt{length}\;#1}
% any operator:
\newcommand{\AnyOp}{\odot}
......@@ -312,6 +323,9 @@
% lifting a formula from iProp to vProp:
\newcommand{\liftobj}[1]{\lceil#1\rceil}
% pure fact that an assertion is objective:
\newcommand{\objective}[1]{\textlog{objective}(#1)}
% access modes:
\newcommand{\accmodeNA}{\textrm{na}}
\newcommand{\accmodeAT}{\textrm{at}}
......@@ -357,6 +371,9 @@
\showfraction{#1}{#2}\mathbin{\leadsto\AT^*} {#3}%
}
% physical length of an array:
\newcommand{\haslength}[2]{|#1| = #2}
% name of a function/predicate of the metalanguage:
\newcommand{\fname}[1]{\ensuremath{\mathsf{{#1}}}\xspace}
......@@ -770,3 +787,35 @@
\newcommand{\rulenametrydequeue}{queue-TryDequeue}
\newcommand{\ruletryenqueue}{\RULE{\rulenametryenqueue}}
\newcommand{\ruletrydequeue}{\RULE{\rulenametrydequeue}}
% ------------------------------------------------------------------------------
% Notations for the pipeline.
% program notations:
\newcommand{\pipeline}{\pname{pipeline}}
\newcommand{\refXArray}{\pname{xs}}
\newcommand{\refYQueue}{\pname{ys}}
\newcommand{\refZArray}{\pname{zs}}
% ghost names:
\newcommand{\gcurf}{\gname\sub{f}} % was: {\mathit{curF}}
\newcommand{\gcurg}{\gname\sub{g}} % was: {\mathit{curG}}
% assertions:
\newcommand{\pipelineInv}[1]{\fname{PipeInv}\;g\;f\;{#1}}
\newcommand{\pipelineInvInner}[1]{\fname{PipeInvInner}\;g\;f\;{#1}\;\gqueue\;\gcurf\;\gcurg}
\newcommand{\pipelineF}[4]{\fname{PipeF}\;g\;f\;{#1}\;\gqueue\;\gcurf\;{#2}\;{#3}\;{#4}}
\newcommand{\pipelineG}[4]{\fname{PipeG}\;g\;f\;{#1}\;\gqueue\;\gcurg\;{#2}\;{#3}\;{#4}}
% canonical variable names:
\newcommand{\xElem}{\ensuremath{x}}
\newcommand{\yElem}{\ensuremath{y}}
\newcommand{\zElem}{\ensuremath{z}}
\newcommand{\nthXElem}[1]{\xElem_{#1}}
\newcommand{\nthZElem}[1]{\zElem_{#1}}
\newcommand{\xElemList}{\mkList\nthXElem\idx\nbelems:}
\newcommand{\zElemList}{\mkList\nthZElem\idx\nbelems:}
\newcommand{\nthYElemView}[1]{(\yElem_{#1},\view_{#1})}
\newcommand{\yElemViewListInv}{\mkList\nthYElemView\idx{\curf-\curg}:}
\newcommand{\curf}{\ensuremath{\nbelems\sub{f}}}
\newcommand{\curg}{\ensuremath{\nbelems\sub{g}}}
\subsection{Implementation of the Pipeline}
\label{sec:pipeline:impl}
\input{figure-pipeline-impl}
\subsection{Proof of the Specification for the Pipeline}
\label{sec:pipeline:proof}
\input{figure-pipeline-invariant}
\subsection{Specification of the Pipeline}
\label{sec:pipeline:spec}
\input{figure-pipeline-spec}
\section{A Simple Pipeline} % TODO: better title: producer-consumer stream?
\label{sec:pipeline}
\input{pipeline-impl}
\input{pipeline-spec}
\input{pipeline-proof}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment