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