Small section on linear annotations
This commit is contained in:
Cédric Pasteur
parent
a2b694602f
commit
9e17900f13
3 changed files with 33 additions and 12 deletions
Binary file not shown.
|
|
@ -617,6 +617,27 @@ tel
|
|||
|
||||
If the backend support parametricity (like in Java), static parameters are kept in the generated code. Otherwise, a pass of the compiler generates all the versions of the node that are needed. If a parametrized node defined in a file \texttt{f1.ept} is used in \texttt{f2.ept}, it is necessary to first compile \texttt{f1.ept} with the \texttt{-c} option (and without any \texttt{-target}), that generates a binary file \texttt{f1.epo}. The compilation of the second file, this time with the \texttt{-target} option, will generate all the necessary nodes, from \texttt{f1.ept} and \texttt{f2.ept}.
|
||||
|
||||
\subsection{Location annotations}
|
||||
|
||||
Memory allocation~\cite{Gerard:2012} avoids unnecessary array copies within the nodes automatically (it can be enable with the \texttt{-memalloc} or \texttt{-O} options). In order to avoid copies when calling nodes, the user must add \emph{location annotations}. We will give here only a short introduction, the interested reader can refer to~\cite{Gerard:2012} for more details. They express the fact that a function modifies in-place its argument. For instance, consider this node that swaps two elements in an array:
|
||||
\begin{lstlisting}
|
||||
node swap(i, j:int; t_in:float^100 at r) returns (t_out:float^100 at r)
var t_tmp:float^100 at r;
|
||||
let
t_tmp = [ t_in with [i] = t_in[>j<] ];
|
||||
t_out = [ t_tmp with [j] = t_in[>i<] ];
tel
|
||||
\end{lstlisting}
|
||||
The location annotations are introduced by the keyword \lstinline{at} followed by a location name. All the streams with the same location name are guaranteed to be stored together in the generated code, so the function generated for \texttt{swap} will directly modify its argument in-place.
|
||||
|
||||
Located variables are called \emph{semilinear}: they can only be updated once, but they can be read many times. An update is a function that modify its argument in-place, for instance a node that inputs and outputs located variables, and a read is any other function. For instance, modifying one element in an array is an update, but accessing one element is a read.
|
||||
|
||||
Only located variables can be given to a function that expects located arguments. A located variable can only be obtained by updating another located variable or by explicitly initializing a new location with the \lstinline+init+ construction:
|
||||
\begin{lstlisting}
|
||||
node shuffle(i_arr, j_arr : int^m; q : int) = (v : float)
|
||||
var t, t_prev : float^n at r;
|
||||
let
init<<r>> t_prev = t_0 fby t;
|
||||
t = fold<<m>> swap(i_arr, j_arr, t_prev);
|
||||
v = t[>q<];
tel
|
||||
\end{lstlisting}
|
||||
|
||||
|
||||
\subsection{Interfaces}
|
||||
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@
|
|||
|
||||
\lstdefinelanguage{Heptagon}
|
||||
{%
|
||||
keywords={node,returns,let,tel,var,pre,fby,when,whenot,merge,if,then,else,or,not},%
|
||||
keywords={node,returns,let,tel,var,pre,fby,when,whenot,merge,if,then,else,or,not,at,init,map,fold,mapdold,foldi,mapi},%
|
||||
morekeywords=[2]{automaton,state,until,unless,end,present,switch,inlined},%
|
||||
morekeywords=[2]{contract,assume,enforce,with},%
|
||||
otherkeywords={->,&,=},%
|
||||
|
|
@ -62,7 +62,7 @@
|
|||
% morekeywords={link,to},%
|
||||
% }[keywords,comments]
|
||||
|
||||
%% règles d'inférence
|
||||
%% rËgles d'infÈrence
|
||||
|
||||
\RequirePackage{mathpartir}
|
||||
|
||||
|
|
@ -96,7 +96,7 @@
|
|||
%\newcommand{\ovfun}[1]{\xrightarrow{#1}}
|
||||
\newcommand{\ovfun}[1]{{\;-\mskip-1.5\thinmuskip\langle{#1}\rangle\!\!\!\rightarrow\;}}
|
||||
|
||||
%% Typage --- général
|
||||
%% Typage --- gÈnÈral
|
||||
|
||||
\DeclareMathOperator{\FV}{FV}
|
||||
\DeclareMathOperator{\FTV}{FTV}
|
||||
|
|
@ -111,7 +111,7 @@
|
|||
|
||||
\newcommand{\mergeenv}{\uplus}
|
||||
|
||||
%% Types de données
|
||||
%% Types de donnÈes
|
||||
|
||||
\newcommand{\type}[3]{\ensuremath{#1\vdash#2:#3}}
|
||||
|
||||
|
|
@ -194,7 +194,7 @@
|
|||
|
||||
\newcommand{\subck}{\ensuremath{<:}}
|
||||
|
||||
%% Sémantique synchrone
|
||||
%% SÈmantique synchrone
|
||||
|
||||
\newcommand{\clock}[1]{\ensuremath{\langle#1\rangle}}
|
||||
|
||||
|
|
@ -264,7 +264,7 @@
|
|||
\shortcal{Y}
|
||||
\shortcal{Z}
|
||||
|
||||
%% mots-clés
|
||||
%% mots-clÈs
|
||||
|
||||
\newcommand{\m@thspace}{%
|
||||
\ifmmode\ \fi%
|
||||
|
|
@ -309,7 +309,7 @@
|
|||
\newcommand{\unop}[2]{\begkw{#1}{#2}}
|
||||
\newcommand{\funct}[2]{\begkw{#1}{#2}}
|
||||
|
||||
%% Mots-clés Lucid Synchrone
|
||||
%% Mots-clÈs Lucid Synchrone
|
||||
|
||||
\begkw{\Assume}{assume}
|
||||
\begkw{\Automaton}{automaton}
|
||||
|
|
@ -374,7 +374,7 @@
|
|||
|
||||
\newcommand{\Nil}{\ensuremath{\mathit{nil}}}
|
||||
|
||||
%% Mots-clés répartition
|
||||
%% Mots-clÈs rÈpartition
|
||||
|
||||
\midkw{\At}{at}
|
||||
\begkw{\Site}{site}
|
||||
|
|
@ -408,7 +408,7 @@
|
|||
\ |\ \False \rightarrow #3
|
||||
}
|
||||
|
||||
%% Théorèmes, définitions, remarques...
|
||||
%% ThÈorËmes, dÈfinitions, remarques...
|
||||
|
||||
\RequirePackage{amsmath}
|
||||
|
||||
|
|
@ -429,7 +429,7 @@
|
|||
\newcommand{\noeuds}{n\oe uds\xspace}
|
||||
\newcommand{\Noeuds}{N\oe uds\xspace}
|
||||
|
||||
%% Macros mathématiques
|
||||
%% Macros mathÈmatiques
|
||||
|
||||
\providecommand{\tonfirst}{}
|
||||
\newcommand{\ton}[1][1]{\renewcommand{\tonfirst}{#1}\tonbis}
|
||||
|
|
@ -465,7 +465,7 @@
|
|||
|
||||
|
||||
|
||||
%% Flots de données
|
||||
%% Flots de donnÈes
|
||||
|
||||
\newenvironment{streams}[1]{%
|
||||
\setlength{\arraycolsep}{0.3cm}
|
||||
|
|
@ -495,7 +495,7 @@
|
|||
|
||||
\renewenvironment{amodifier}{}{}
|
||||
|
||||
%% Boîte-noeud code
|
||||
%% BoÓte-noeud code
|
||||
|
||||
\RequirePackage{alltt}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue