Sockeye TN: Start updating checks section
[barrelfish] / doc / 025-sockeye / Sockeye.tex
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 % Copyright (c) 2017, ETH Zurich.
3 % All rights reserved.
4 %
5 % This file is distributed under the terms in the attached LICENSE file.
6 % If you do not find this file, copies can be found by writing to:
7 % ETH Zurich D-INFK, Universitaetstr 6, CH-8092 Zurich. Attn: Systems Group.
8 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9
10 \providecommand{\pgfsyspdfmark}[3]{}
11
12 \documentclass[a4paper,11pt,twoside]{report}
13 \usepackage[T1]{fontenc}
14 \usepackage{amsmath}
15 \usepackage{bftn}
16 \usepackage{calc}
17 \usepackage{verbatim}
18 \usepackage{xspace}
19 \usepackage{pifont}
20 \usepackage{pxfonts}
21 \usepackage{textcomp}
22
23 \usepackage{multirow}
24 \usepackage{listings}
25 \usepackage{todonotes}
26 \usepackage{hyperref}
27
28 \title{Sockeye in Barrelfish}
29 \author{Barrelfish project}
30 % \date{\today}   % Uncomment (if needed) - date is automatic
31 \tnnumber{025}
32 \tnkey{Sockeye}
33
34
35 \lstdefinelanguage{Sockeye}{
36     morekeywords={accept, are, as, at, import, in, input, is, map, module, output, over, reserved, to, with},
37     sensitive=true,
38     morecomment=[l]{//},
39     morecomment=[s]{/*}{*/},
40     morestring=[b]",
41 }
42
43 \presetkeys{todonotes}{inline}{}
44
45 \begin{document}
46 \maketitle      % Uncomment for final draft
47
48 \begin{versionhistory}
49 \vhEntry{0.1}{15.06.2017}{DS}{Initial Version}
50 \vhEntry{0.2}{26.07.2017}{DS}{Describe Modularity Features}
51 \end{versionhistory}
52
53 % \intro{Abstract}    % Insert abstract here
54 % \intro{Acknowledgements}  % Uncomment (if needed) for acknowledgements
55 \tableofcontents    % Uncomment (if needed) for final draft
56 % \listoffigures    % Uncomment (if needed) for final draft
57 % \listoftables     % Uncomment (if needed) for final draft
58 \cleardoublepage
59 \setcounter{secnumdepth}{2}
60
61 \newcommand{\fnname}[1]{\textit{\texttt{#1}}}%
62 \newcommand{\datatype}[1]{\textit{\texttt{#1}}}%
63 \newcommand{\varname}[1]{\texttt{#1}}%
64 \newcommand{\keywname}[1]{\textbf{\texttt{#1}}}%
65 \newcommand{\pathname}[1]{\texttt{#1}}%
66 \newcommand{\tabindent}{\hspace*{3ex}}%
67 \newcommand{\Sockeye}{\lstinline[language=Sockeye]}
68 \newcommand{\Prolog}{\lstinline[language=Prolog]}
69 \newcommand{\ccode}{\lstinline[language=C]}
70
71 \lstset{
72   basicstyle=\ttfamily \small,
73   keywordstyle=\bfseries,
74   flexiblecolumns=false,
75   basewidth={0.5em,0.45em},
76   boxpos=t,
77   captionpos=b,
78   frame=single,
79   breaklines=true,
80   postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space}
81 }
82
83
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
85 \chapter{Introduction and Usage}
86 \label{chap:introduction}
87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
88
89 \emph{Sockeye}\footnote{Sockeye salmon (Oncorhynchus nerka), also called red salmon, kokanee salmon, or blueback salmon, is an anadromous species of salmon found in the Northern Pacific Ocean and rivers discharging into it. This species is a Pacific salmon that is primarily red in hue during spawning. They can grow up to 84 cm in length and weigh 2.3 to 7 kg. 
90 Source: \href{https://en.wikipedia.org/wiki/Sockeye_salmon}{Wikipedia}}
91 is a domain specific language to describe SoCs (Systems on a Chip).
92
93 Achermann~et~al.~\cite{achermann:mars17} propose a formal model to describe address spaces and interrupt routes in a system as a directed graph.
94 They call such a graph a ``decoding net''.
95 Each node in the graph can accept a set of addresses and translate another (not necessarily disjunct) set of addresses (when describing interrupt routes the accept or translate interrupt vectors).
96 Starting at a specific node, addresses can be resolved by following the appropriate edges in the decoding net.
97 When a node translates an address, resolution is continued on that node.
98 When a node accepts an address, resolution terminates
99
100 Achermann~et~al.~\cite{achermann:mars17} also propose a concrete syntax for specifying decoding nets.
101 Sockeye is an implementation of the proposed language but adds some features to address issues encountered in practice.
102
103 The Sockeye compiler is written in Haskell using the Parsec parsing library. It
104 generates Prolog files from the Sockeye files. These Prolog files contain facts that represent a decoding net (see Chapter~\ref{chap:prolog}).
105 The Prolog files can then be loaded into Barrelfish's System Knowledgebase (SKB).
106
107 The source code for Sockeye can be found in \pathname{SOURCE/tools/sockeye}.
108
109
110 \section{Command Line Options}
111
112 \begin{verbatim}
113 $ sockeye [options] file
114 \end{verbatim}
115
116
117 The available options are:
118 \begin{description}
119 \item[-P] Generate a Prolog file that can be loaded into the SKB.
120 \item[-i] Add a directory to the search path where Sockeye looks for imports.
121 \item[-o] \varname{filename} The path to the output file
122 \item[-h] show usage information
123 \end{description}
124
125 The backend (capital letter options) specified last takes precedence.
126
127 Multiple directories can be added by giving the \texttt{-i} options multiple times.
128 Sockeye will first look for files in the current directory and then check the given directories in the order they were given.
129
130 The Sockeye file to compile is given via the \texttt{file} parameter.
131
132
133 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
134 \chapter{Lexical Conventions}
135 \label{chap:lexer}
136 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
137
138 The Sockeye parser follows a similar convention as opted by modern day 
139 programming languages like C and Java. Hence, Sockeye uses a Java-style-like
140 parser based on the Haskell Parsec Library. The following conventions are used:
141
142 \begin{description}
143 \item[Encoding] The file should be encoded using plain text.
144 \item[Whitespace:]  As in C and Java, Sockeye considers sequences of
145   space, newline, tab, and carriage return characters to be
146   whitespace.  Whitespace is generally not significant. 
147
148 \item[Comments:] Sockeye supports C-style comments.  Single line comments
149   start with \texttt{//} and continue until the end of the line.
150   Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
151   anything in between is ignored and treated as white space.
152   Nested comments are not supported.
153
154 \item[Identifiers:] Valid Sockeye identifiers are sequences of numbers
155   (0-9), letters (a-z, A-Z), the underscore character ``\texttt{\_}'' and the dash character ``\textendash''. They
156   must start with a letter.
157   \begin{align*}
158   identifier & \rightarrow letter (letter \mid digit \mid \text{\_} \mid \text{\textendash})^{\textrm{*}} \\
159   letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
160   digit & \rightarrow (\textsf{0 \ldots 9})
161     \end{align*}
162
163 \item[Case sensitivity:] Sockeye is case sensitive hence identifiers \Sockeye{node1} and \Sockeye{Node2} are not the same.
164   
165 \item[Integer Literals:] A Sockeye integer literal is a sequence of
166   digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
167   literals have no specifier and hexadecimal literals start with
168   \texttt{0x}.
169
170 \begin{align*}
171 decimal & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
172 hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
173 \end{align*}
174
175 \item[Reserved words:] The following are reserved words in Sockeye:
176 \begin{verbatim}
177 accept, are, as, at, import, in, input, is, map,
178 module, output, over, reserved, to, with
179 \end{verbatim}
180
181 \end{description}
182
183
184 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
185 \chapter{Syntax}
186 \label{chap:declaration}
187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
188
189 In this chapter we define the layout of a Sockeye file.
190 The node declarations in a Sockeye file describe a single decoding net.
191 Parts of a decoding net can be packaged into reusable modules (see Section~\ref{sec:modules}).
192 With imports (see Section~\ref{sec:imports}) modules can also be put into separate files.
193 Also, a SoC can be split into multiple decoding nets e.g. one for the address spaces and another one for the interrupt routes.
194
195 In the following sections we use EBNF to specify the Sockeye syntax. Terminals are \textbf{bold} while non-terminals are \textit{italic}.
196 The non-terminals \textit{iden}, \textit{letter}, \textit{decimal} and \textit{hexadecimal} correspond to the ones defined in Chapter~\ref{chap:lexer}.
197
198 \section{Basic Syntax}
199 This section describes the basic syntax for Sockeye.
200 It closely corresponds to the concrete syntax described in \cite{achermann:mars17}.
201 If there are important syntactic or semantic differences it is stated so in the description of the respective syntactical construct.
202
203 \subsection{Node Declarations}
204 A node declaration contains one or more identifiers and the node specification.
205 The order in which the nodes are declared does not matter.
206
207 \paragraph{Syntax}
208 \begin{align*}
209 \textit{net}_s & \mathop{=}
210     \Big\{
211         \textit{iden}\ \textbf{is}\ \textit{node}_s\
212     \Big|\
213         \textit{iden}\bigl\{\textbf{,}\ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
214     \Big\} \\
215 \end{align*}
216
217 \clearpage
218 \paragraph{Example}
219 \begin{syntax}
220     node1 \textbf{is} \ldots
221
222     node2,
223     node3 \textbf{are} \ldots
224 \end{syntax}
225
226 \subsection{Node Specifications}
227 A node specification consists of a type, a set of accepted address blocks, a set of address mappings to other nodes, a set of reserved address blocks and an overlay.
228 All of these are optional.
229 The reserved address blocks are only relevant in conjunction with overlays and are used to exclude some addresses from the overlay.
230 The overlay is specified as a node identifier and a number of address bits.
231 The overlay will span addresses from \texttt{0x0} to \(\texttt{0x2}^\texttt{bits} - \texttt{1}\).
232
233 \paragraph{Syntax}
234 \begin{align*}
235 \textit{node}_s & \mathop{=}
236     \Big[\ 
237        \textit{type}\ 
238     \Big]\  
239     \Big[
240        \textit{accept}\ 
241     \Big]\ 
242     \Big[\ 
243        \textit{map}\ 
244     \Big]\ 
245     \Big[\ 
246         \textit{reserved}\ 
247     \Big]\ 
248     \Big[\ 
249         \textit{overlay}\ 
250     \Big]\\
251 \textit{accept} & \mathop{=}
252     \textbf{accept [}\ \big\{\ \textit{block}_s\ \big\}\ \textbf{]}\\
253 \textit{map} & \mathop{=}
254     \textbf{map [}\ \big\{\ \textit{map}_s\ \big\}\ \textbf{]}\\
255 \textit{reserved} & \mathop{=}
256     \textbf{reserved [}\ \big\{\ \textit{block}_s\ \big\}\ \textbf{]}\\
257 \textit{overlay} & \mathop{=}
258     \textbf{over}\ \textit{iden}\textbf{/}\textit{decimal}\\
259 \end{align*}
260
261 \paragraph{Example}
262 \begin{syntax}
263     node1 \textbf{is} \textit{<type>} \textbf{accept} [\ldots]
264     node2 \textbf{is} \textbf{map} [\ldots]
265     node3 \textbf{is} \textbf{reserved} [\ldots] \textbf{over} node2/32
266 \end{syntax}
267
268 \subsection{Node Type}
269 Currently there are two types: \Sockeye{device} and \Sockeye{memory}. A third internal type \Sockeye{other} is given to nodes for which no type is specified.
270 The \Sockeye{device}-type specifies that the accepted addresses are device registers while the \Sockeye{memory}-type is for memory nodes like RAM or ROM.
271
272 \paragraph{Syntax}
273 \begin{align*}
274 \textit{type} & \mathop{=}
275     \textbf{device}\
276     |\
277     \textbf{memory} \\
278 \end{align*}
279
280 \paragraph{Example}
281 \begin{syntax}
282     node1 \textbf{is} memory \textbf{accept} [\ldots]
283     node2 \textbf{is} device \textbf{accept} [\ldots]
284 \end{syntax}
285
286 \subsection{Addresses}
287 Addresses are specified as hexadecimal literals.
288
289 \paragraph{Syntax}
290 \begin{align*}
291 \textit{addr} & \mathop{=} \textit{hexadecimal} \\
292 \end{align*}
293
294 \subsection{Block Specifications}
295 A block is specified by its start and end address.
296 If the start and end address are the same, the end address can be omitted.
297 Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
298 A block from \Sockeye{0x0} to \Sockeye{0xFFF} with a size of 4kB can be specified as \Sockeye{0x0/12}.
299
300 \paragraph{Syntax}
301 \begin{align*}
302 \textit{block}_s & \mathop{=} \textit{addr}\
303     \Big[
304         \textbf{-}\ \textit{addr}\ 
305     \Big|\
306         \textbf{/}\textit{decimal}
307     \Big] \\
308 \end{align*}
309
310 \paragraph{Example}
311 \begin{syntax}
312     node1 is \textbf{accept} [0x42-0x51]
313     node2 is \textbf{accept} [0x42]      // \textit{same as \textup{0x42-0x42}}
314     node3 is \textbf{accept} [0x0/12]    // \textit{same as \textup{0x0-0xFFF}}
315 \end{syntax}
316
317 \subsection{Map Specification}
318 A map specification is a source address block, a target node identifier and optionally a target base address to which the source block is translated within the target node.
319 If no target base address is given, the block is translated to the target node starting at \Sockeye{0x0}.
320 Note that this is different from the concrete syntax described in \cite{achermann:mars17} where in this case the base address of the source block is used.
321 This was changed due to the mapping to \Sockeye{0x0} being used more often in practice.
322 Multiple translation targets can be specified by giving a comma-separated list of targets.
323
324 \paragraph{Syntax}
325 \begin{align*}
326 \textit{map}_s & \mathop{=}
327 \textit{block}_s\ \textbf{to}\ \textit{iden}\ 
328     \Big[
329         \textbf{at}\ \textit{addr}
330     \Big]\
331     \Big\{
332         \textbf{,}\ \textit{iden}\ 
333         \Big[
334             \textbf{at}\ \textit{addr}
335         \Big]
336     \Big\}\\
337 \end{align*}
338
339 \paragraph{Example}
340 \begin{syntax}
341     /* \textit{Translate \textup{0x0-0xFF} to \textup{node2} at \textup{0x300-0x3FF}:} */
342     node1 is \textbf{map} [0x0/8 \textbf{to} node2 \textbf{at} 0x300] 
343
344     /* \textit{This is the same as \textup{0x300/8 \textbf{to} node1 \textbf{at} 0x0}:} */
345     node2 is \textbf{map} [0x300/8 \textbf{to} node1]
346
347     /* \textit{Multiple translation targets, \textup{0x0-0xFF} is translated to
348        - \textup{node1} at \textup{0x0-0xFF}
349        - \textup{node2} at \textup{0x300-0x3FF}:} */
350     node3 is \textbf{map} [0x0/8 \textbf{to} node1, node2 \textbf{at} 0x300]
351 \end{syntax}
352
353 \section{Modules}
354 \label{sec:modules}
355 A module encapsulates a decoding net which can be integrated into a larger decoding net.
356 A module instantiation always creates a namespace inside the current one.
357 Normally nodes can only be referenced by nodes in the same namespace but there needs to be away to reference nodes inside a module and also a way for nodes inside the module to reference nodes outside of it.
358 This is done via ports.
359 There are input ports, which create a connection into the module and output ports which create connections from the module to outside nodes.
360 A port has always a width, specified as the number of address bits the port spans.
361 All declared input ports must have a corresponding node declaration in the module body.
362
363 When a module is instantiated a list of port mappings can be specified.
364 An input port mapping creates a node outside the module that overlays the node inside the module.
365 An output port mapping creates a node inside the module that overlays the node outside the module.
366 Not all ports a module declares have to be mapped.
367 Not mapping an input port simply means there is no connection to the corresponding node inside the module.
368 For unmapped output ports there will be an empty node inside the module, which is a dead end for address resolution.
369
370 Additionally a module can also be parametrized.
371 It will then be a module template that only becomes a fully defined module when instantiated with concrete arguments.
372 Module parameters are typed and the Sockeye compiler checks that they are used in a type safe way.
373 There are two types of parameters, address parameters and natural parameters.
374 Address parameters allow to parametrize addresses in node specifications.
375 Natural parameters are used in combination with interval template identifiers (see Section~\ref{sec:template_idens}).
376 Parameters can also be passed as arguments to module template instantiations in the module body.
377
378 \subsection{Module Declarations}
379 A module declaration starts with the keyword \Sockeye{module} and a unique module name.
380 If the module is a template, a list of typed parameters can be specified.
381 The module body is enclosed in curly braces and starts with the port definitions.
382 The rest of the body are node declarations and module instantiations.
383 If the module has address parameters the name of the parameter can be used wherever in the body an address is expected.
384
385 \paragraph{Syntax}
386 \begin{align*}
387     \textit{param\_type} & \mathop{=}
388         \textbf{addr}\ |\ \textbf{nat}\\
389     \textit{parameter} & \mathop{=}
390         \textit{param\_type}\ \textit{iden}\\
391     \textit{param\_list} & \mathop{=}
392         \textbf{(}\big[\ 
393             \textit{parameter}\big\{\textbf{,}\ \textit{parameter}\big\}\ 
394         \big] \textbf{)}\\
395     \textit{input\_port} & \mathop{=}
396         \textbf{input}\ \textit{iden}\textbf{/}\textit{decimal}
397         \big\{
398             \textbf{,}\ \textit{iden}\textbf{/}\textit{decimal}
399         \big\}\\
400     \textit{output\_port} & \mathop{=}
401         \textbf{output}\ \textit{iden}\textbf{/}\textit{decimal}
402         \big\{
403             \textbf{,}\ \textit{iden}\textbf{/}\textit{decimal}
404         \big\}\\
405     \textit{body}_s & \mathop{=}
406         \big\{\ 
407             \textit{net}_s\ |\ \textit{mod\_inst}_s\ 
408         \big\}\\
409     \textit{mod\_decl}_s & \mathop{=}
410         \textbf{module}\ \textit{iden} \big[\textit{param\_list}\big]\ 
411         \textbf{\{}\ 
412             \big\{\textit{input\_port}\ |\ \textit{output\_port}\big\}\ 
413             \textit{body}_s\ 
414         \textbf{\}}\\
415 \end{align*}
416
417 \subsection{Module Instantiations}
418 Module instantiations start with the module name and in the case of a module template with the list of arguments.
419 After that the identifier of the namespace in which to instantiate the module has to be given followed by an optional list of port mappings.
420
421 \paragraph{Syntax}
422 \begin{align*}
423     \textit{argument} & \mathop{=}
424         \textit{decimal}\ |\ \textit{hexadecimal}\ |\ \textit{iden}\\
425     \textit{arg\_list} & \mathop{=}
426         \textbf{(}\big[\ 
427             \textit{argument}\big\{\textbf{,}\ \textit{argument}\big\}\ 
428         \big] \textbf{)}\\
429     \textit{mod\_inst}_s & \mathop{=}
430         \textit{iden} \big[\textit{arg\_list}\big]\ \textbf{as}\ \textit{iden}\ \big[\ 
431             \textbf{with}\ \big\{\textit{input\_map}\ |\ \textit{output\_map}\big\}\ 
432         \big]\\
433     \textit{input\_map} & \mathop{=}
434         \textit{iden}\ \textbf{>}\ \textit{iden}\\
435     \textit{output\_map} & \mathop{=}
436         \textit{iden}\ \textbf{<}\ \textit{iden}\\
437 \end{align*}
438
439 \clearpage
440 \paragraph{Example}
441 \begin{syntax}
442     /* Instantiate module 'SomeModule' in namespace 'subspace' /*
443     SomeModule \textbf{as} subspace
444
445     /* Pass arguments to module template */
446     TemplModule(0x0, 42) \textbf{as} templSubspace
447
448     /* Declare port mappings:
449        - map 'Node1' to ouptut port 'Out'
450        - map input port 'In' to 'Node2' */
451     SomeModule \textbf{as} subspace \textbf{with}
452         Node1 > Out
453         Node2 < In
454 \end{syntax}
455
456 \section{Templated Identifiers}
457 \label{sec:template_idens}
458 Templated identifiers allow to declare multiple nodes and ports at once and instantiate a module multiple times at once.
459 There are two forms of templated identifiers:
460 \begin{description}
461     \item[Interval template]
462         The template contains one or several intervals.
463         The identifier will be instantiated for all possible combinations of values in the intervals.
464         Index variables can optionally be named so they can be referenced later.
465     \item[Simple template]
466         Simple templates work very similar to interval templates.
467         The only difference is, that a simple template can only reference index variables declared in the same context.
468         It can not contain intervals to declare new index variables.
469 \end{description}
470
471 Interval templates can be used in identifiers of node declarations (to declare multiple nodes), port declarations (to declare multiple ports) and namespace identifiers of module instantiations (to instantiate a module multiple times).
472 The scope of index variables is the corresponding syntactic construct the interval template was used in.
473 Simple templates can be used in any place a node identifier is expected.
474 This includes the places where interval templates can be used, translation destination node identifiers and overlays but not module parameter or index variable names.
475
476 An important thing to note is that the limits of an interval can reference module parameters of type \Sockeye{nat}.
477 This allows module parameters to control how many ports or nodes are instantiated from a certain interval template.
478
479 \paragraph{Syntax}
480 \begin{align*}
481     \textit{var} & \mathop{=}
482         \textit{iden}\\
483     \textit{limit} & \mathop{=}
484         \textit{decimal}\ |\ \textit{iden} \\
485     \textit{interval} & \mathop{=}
486         \textbf{[}\textit{limit}\textbf{..}\textit{limit}\textbf{]}\\
487     \textit{interval\_templ}_s & \mathop{=}
488         \textit{iden}\textbf{\{}\textit{var}\ \textbf{in}\ \textit{interval}\textbf{\}}
489         \Big[
490             \textit{iden}\ |\ \textit{templ\_iden}_s\ |\ \textit{for\_iden}_s
491         \Big]\\
492     \textit{simple\_templ}_s & \mathop{=}
493         \textit{iden}\textbf{\{}\textit{var}\textbf{\}}\Big[\textit{iden}\ |\ \textit{templ\_iden}_s\Big]\\
494 \end{align*}
495
496 \paragraph{Example}
497 \begin{syntax}
498     /* Declare similar nodes
499        (Note that interval templates in node declarations
500        always require the usage of '\textbf{are}') */
501     Device_\verb+{+[1..5]\verb+}+ \textbf{are} device \textbf{accept} [0x0/8]
502
503     /* Use the index in the node definition */
504     Map_\verb+{+m in [1..5]\verb+}+ \textbf{is} \textbf{map} [0x100/8 to Device_\verb+{+m\verb+}+]
505
506     /* Declare similar module ports
507        (possibly depending on module parameters) */
508     \textbf{module} SomeModule(nat num) \verb+{+
509         output Out_\verb+{+[1..num]\verb+}+
510         \ldots
511     \verb+}+
512
513     /* Instantiate module multiple times
514        and use index variable in port mappings */
515     SomeModule(3) \textbf{as} sub_module_\verb+{+m in [1..2]\verb+}+ \textbf{with}
516         Node_\verb+{+m\verb+}+_\verb+{+o in [1..3]\verb+}+ > Out_\verb+{+o\verb+}+
517 \end{syntax}
518
519 \section{Imports}
520 \label{sec:imports}
521 Imports allow a specification to be divided over several files.
522 They also allow the reuse of declared modules.
523 Imports have to be specified at the very top of a Sockeye file.
524 An import will cause the compiler to load all modules from \pathname{<import\_path>.soc}
525 Nodes declared outside of modules will not be loaded.
526 The compiler will first look for files in the current directory and then check the directories passed with the \texttt{-i} option in the order they were given.
527
528 \paragraph{Syntax}
529 \begin{align*}
530 \textit{import}_s & \mathop{=}
531     \textbf{import}\ \big\{\ \textit{letter}\ |\ \textbf{/}\ \big\}
532 \end{align*}
533
534 \paragraph{Example}
535 \begin{syntax}
536     /* Invoked with 'sockeye -i imports -i modules' the following
537        will cause the compiler to look for the files
538        - ./subdir/core.soc
539        - imports/subdir/core.soc
540        - modules/subdir/core.soc
541        and import all modules from the first one that exists. */
542     \textbf{import} subdir/core
543 \end{syntax}
544
545 \section{Sockeye Files}
546 A sockeye file consists of imports, module declarations and the specification body (node declarations and module instantiations).
547
548 \paragraph{Syntax}
549 \begin{align*}
550     \textit{sockeye}_s & \mathop{=}
551         \big\{\ 
552             \textit{import}_s\ 
553         \big\}\ 
554         \big\{\ 
555             \textit{mod\_decl}_s\ 
556         \big\}\ 
557         \big\{\ 
558             \textit{net}_s\ |\ \textit{mod\_inst}_s\ 
559         \big\}
560 \end{align*}
561
562 \paragraph{Example}
563 Listing~\ref{lst:sockeye_example} shows an example Sockeye specification.
564 The specification for the Texas Instruments OMAP4460 SoC used on the PandaboardES can serve as a real world example. It is located in \pathname{SOURCE/socs/omap44xx.soc}.
565
566 \clearpage
567 \lstinputlisting[caption={Example Sockeye specification}, label={lst:sockeye_example}, language=Sockeye]{example.soc}
568
569
570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
571 \chapter{Checks on the AST}
572 \label{chap:checks}
573 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
574 The Sockeye compiler performs two sets of checks.
575 The first checks are on a module level.
576 Without concrete arguments to the modules not everything can be checked at module level.
577 That is why the second set of checks is run when the modules are fully instantiated.
578
579 \section{Module Level Checks}
580
581
582 \section{Decoding Net Level Checks}
583 \subsection{No Module Instantiation Loops}
584 This check makes sure, that there are no loops in module instantiations which would cause the compiler to not terminate.
585
586 \subsection{No Duplicate Ports}
587 This check makes sure, that there are no duplicate input or output ports.
588 Not that having the same node declared as an input and an output port is allowed and results in the node being passed through the module.
589
590 \todo{This check is currently not implemented.
591 For input ports the error will go unnoticed but it also has no effect on the well-formedness of the decoding net.
592 For output ports it will result in a \texttt{DuplicateIdentifier} error (see Section~\ref{sec:check_dupl_ident}).}
593
594 \subsection{No Duplicate Port Mapping}
595 This check makes sure that a port is not mapped twice in the same module instantiation.
596
597 \subsection{No Map to Undefined Port}
598 This check makes sure that there are no port mappings to ports not declared by the instantiated module.
599
600 \todo{This check is currently not implemented.
601 For input ports the error will result in a \texttt{UndefinedReference} error.
602 For output ports the error will go unnoticed}
603
604 \subsection{No Duplicate Identifiers}
605 \label{sec:check_dupl_ident}
606 This check makes sure that there aren't two node declarations with the same identifier.
607
608 \subsection{No References to Undefined Nodes}
609 This check makes sure that all nodes referenced in translation sets and overlays are declared.
610
611
612 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
613 \chapter{Prolog Mapping for Sockeye}
614 \label{chap:prolog}
615 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
616 The Sockeye compiler generates \(\text{ECL}^i\text{PS}^e\)-Prolog\footnote{\href{http://eclipseclp.org/}{http://eclipseclp.org/}} to be used within the SKB.
617 A decoding net is expressed by the predicate \Prolog{net/2}. The first argument to the predicate is the node identifier represented as a functor \Prolog{nodeId} with the first argument being the node's name represented as an atom and the second the (possibly nested) namespace it is in, represented as a list of atoms.
618 The second argument is the node specification, a Prolog functor with the name \Prolog{node} and an arity of three.
619 The arguments of the functor are the node type, the list of accepted addresses and the list of translated addresses.
620 The overlay is translated to address mappings and added to the list of translated addresses during compilation.
621
622 The node type is one of three atoms: \Prolog{device}, \Prolog{memory} or \Prolog{other}.
623 The accepted addresses are a list of address blocks where each block is represented through the functor \Prolog{block/2} with the start and end addresses as arguments.
624 The translated addresses are a list of mappings to other nodes, represented by the functor \Prolog{map/3} where the first argument is the translated address block, the second one is the node identifier of the target node and the third one is the base address for the mapping in the target node.
625
626 There is a predicate clause for \Prolog{net/2} for every node specified. 
627 Listings~\ref{lst:prolog_example} shows the generated Prolog code for the Sockeye example in Listing~\ref{lst:sockeye_example}.
628
629 \lstinputlisting[caption={Generated Prolog code},label={lst:prolog_example},language=Prolog]{example.pl}
630
631
632 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
633 \chapter{Compiling Sockeye Files with Hake}
634 \label{chap:hake}
635 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
636 SoC descriptions are placed in the directory \pathname{SOURCE/socs} with the file extension \pathname{soc}.
637 Each top-level Sockeye file has to be added to the list of SoCs in the Hakefile in the same directory.
638 When passed a filename (without extension), the function \verb|sockeye :: String -> HRule| creates a rule to compile the file \pathname{SOURCE/socs/<filename>.soc} to \pathname{BUILD/sockeyefacts/<filename>.pl}.
639 The rule will also generate \pathname{BUILD/sockeyefacts/<filename>.pl.depend} (with the \texttt{-d} option of the Sockeye compiler) and include it in the Makefile.
640 This causes \texttt{make} to rebuild the file also when imported files are changed.
641 To add a compiled Sockeye specification to the SKB RAM-disk, the filename can be added to the \varname{sockeyeFiles} list in the SKBs Hakefile.
642
643
644 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
645 \bibliographystyle{abbrv}
646 \bibliography{defs,barrelfish}
647
648 \end{document}