Sockeye TN: Update chapter on checks
[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}{03.08.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 they 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 at the referenced 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 In the future the compiler should also be able to generate Isabelle code from Sockeye specifications to be able to verify hardware designs.
108
109 The source code for Sockeye can be found in \pathname{SOURCE/tools/sockeye}.
110
111 \clearpage
112 \section{Command Line Options}
113
114 \begin{verbatim}
115 $ sockeye [options] file
116 \end{verbatim}
117
118
119 The available options are:
120 \begin{description}
121 \item[-P] Generate a Prolog file that can be loaded into the SKB (default).
122 \item[-i] Add a directory to the search path where Sockeye looks for imports.
123 \item[-o] \varname{filename} The path to the output file (required)
124 \item[-d] \varname{filename} The path to the dependency output file (optional)
125 \item[-h] show usage information
126 \end{description}
127
128 The backend (capital letter options) specified last takes precedence.
129 At the moment there is only a backend for generating Prolog for use in Barrelfish's SKB.
130
131 Multiple directories can be added by giving the \texttt{-i} options multiple times.
132 Sockeye will first look for files in the current directory and then check the given directories in the order they were given.
133
134 When invoked with the \texttt{-d} option, the compiler will generate a dependency file for GNU make to be able to track changes in imported files.
135
136 The Sockeye file to compile is given via the \texttt{file} parameter.
137
138
139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
140 \chapter{Lexical Conventions}
141 \label{chap:lexer}
142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
143
144 The Sockeye parser follows a similar convention as opted by modern day 
145 programming languages like C and Java. Hence, Sockeye uses a Java-style-like
146 parser based on the Haskell Parsec Library. The following conventions are used:
147
148 \begin{description}
149 \item[Encoding] The file should be encoded using plain text.
150 \item[Whitespace:]  As in C and Java, Sockeye considers sequences of
151   space, newline, tab, and carriage return characters to be
152   whitespace.  Whitespace is generally not significant. 
153
154 \item[Comments:] Sockeye supports C-style comments.  Single line comments
155   start with \texttt{//} and continue until the end of the line.
156   Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
157   anything in between is ignored and treated as white space.
158   Nested comments are not supported.
159
160 \item[Identifiers:] Valid Sockeye identifiers are sequences of numbers
161   (0-9), letters (a-z, A-Z), the underscore character ``\texttt{\_}'' and the dash character ``\textendash''. They
162   must start with a letter.
163   \begin{align*}
164   identifier & \rightarrow letter (letter \mid digit \mid \text{\_} \mid \text{\textendash})^{\textrm{*}} \\
165   letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
166   digit & \rightarrow (\textsf{0 \ldots 9})
167     \end{align*}
168
169 \item[Case sensitivity:] Sockeye is case sensitive hence identifiers \Sockeye{node1} and \Sockeye{Node2} are not the same.
170   
171 \item[Integer Literals:] A Sockeye integer literal is a sequence of
172   digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
173   literals have no specifier and hexadecimal literals start with
174   \texttt{0x}.
175
176 \begin{align*}
177 decimal & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
178 hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
179 \end{align*}
180
181 \item[Reserved words:] The following are reserved words in Sockeye:
182 \begin{verbatim}
183 accept, are, as, at, import, in, input, is, map,
184 module, output, over, reserved, to, with
185 \end{verbatim}
186
187 \end{description}
188
189
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
191 \chapter{Syntax}
192 \label{chap:declaration}
193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
194
195 In this chapter we define the layout of a Sockeye file.
196 The node declarations in a Sockeye file describe a single decoding net.
197 Parts of a decoding net can be packaged into reusable modules (see Section~\ref{sec:modules}).
198 With imports (see Section~\ref{sec:imports}) modules can also be put into separate files.
199
200 In the following sections we use EBNF to describe the Sockeye syntax. Terminals are \textbf{bold} while non-terminals are \textit{italic}.
201 The non-terminals \textit{iden}, \textit{letter}, \textit{decimal} and \textit{hexadecimal} correspond to the ones defined in Chapter~\ref{chap:lexer}.
202
203 \section{Basic Syntax}
204 This section describes the basic syntax for Sockeye.
205 It closely corresponds to the concrete syntax described in \cite{achermann:mars17}.
206 If there are important syntactic or semantic differences it is stated explicitly in the description of the respective syntactical construct.
207
208 \subsection{Node Declarations}
209 A node declaration contains one or more identifiers and the node specification.
210 The order in which the nodes are declared does not matter.
211
212 \paragraph{Syntax}
213 \begin{align*}
214 \textit{net}_s & \mathop{=}
215     \Big\{
216         \textit{iden}\ \textbf{is}\ \textit{node}_s\
217     \Big|\
218         \textit{iden}\bigl\{\textbf{,}\ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
219     \Big\} \\
220 \end{align*}
221
222 \clearpage
223 \paragraph{Example}
224 \begin{syntax}
225     node1 \textbf{is} \ldots
226
227     node2,
228     node3 \textbf{are} \ldots
229 \end{syntax}
230
231 \subsection{Node Specifications}
232 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.
233 All of these are optional.
234 The reserved address blocks are only relevant in conjunction with overlays and are used to exclude some addresses from the overlay.
235 The overlay is specified as a node identifier and a number of address bits.
236 The overlay will span addresses from \texttt{0x0} to \(\texttt{0x2}^\texttt{bits} - \texttt{1}\).
237
238 \paragraph{Syntax}
239 \begin{align*}
240 \textit{node}_s & \mathop{=}
241     \Big[\ 
242        \textit{type}\ 
243     \Big]\  
244     \Big[
245        \textit{accept}\ 
246     \Big]\ 
247     \Big[\ 
248        \textit{map}\ 
249     \Big]\ 
250     \Big[\ 
251         \textit{reserved}\ 
252     \Big]\ 
253     \Big[\ 
254         \textit{overlay}\ 
255     \Big]\\
256 \textit{accept} & \mathop{=}
257     \textbf{accept [}\ \big\{\ \textit{block}_s\ \big\}\ \textbf{]}\\
258 \textit{map} & \mathop{=}
259     \textbf{map [}\ \big\{\ \textit{map}_s\ \big\}\ \textbf{]}\\
260 \textit{reserved} & \mathop{=}
261     \textbf{reserved [}\ \big\{\ \textit{block}_s\ \big\}\ \textbf{]}\\
262 \textit{overlay} & \mathop{=}
263     \textbf{over}\ \textit{iden}\textbf{/}\textit{decimal}\\
264 \end{align*}
265
266 \paragraph{Example}
267 \begin{syntax}
268     node1 \textbf{is} \textit{<type>} \textbf{accept} [\ldots]
269     node2 \textbf{is} \textbf{map} [\ldots]
270     node3 \textbf{is} \textbf{reserved} [\ldots] \textbf{over} node2/32
271 \end{syntax}
272
273 \subsection{Node Type}
274 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.
275 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.
276
277 \paragraph{Syntax}
278 \begin{align*}
279 \textit{type} & \mathop{=}
280     \textbf{device}\
281     |\
282     \textbf{memory} \\
283 \end{align*}
284
285 \paragraph{Example}
286 \begin{syntax}
287     node1 \textbf{is} memory \textbf{accept} [\ldots]
288     node2 \textbf{is} device \textbf{accept} [\ldots]
289 \end{syntax}
290
291 \subsection{Addresses}
292 Addresses are specified as hexadecimal literals.
293
294 \paragraph{Syntax}
295 \begin{align*}
296 \textit{addr} & \mathop{=} \textit{hexadecimal} \\
297 \end{align*}
298
299 \subsection{Block Specifications}
300 A block is specified by its start and end address.
301 If the start and end address are the same, the end address can be omitted.
302 Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
303 A block from \Sockeye{0x0} to \Sockeye{0xFFF} with a size of 4kB can be specified as \Sockeye{0x0/12}.
304
305 \paragraph{Syntax}
306 \begin{align*}
307 \textit{block}_s & \mathop{=} \textit{addr}\
308     \Big[
309         \textbf{-}\ \textit{addr}\ 
310     \Big|\
311         \textbf{/}\textit{decimal}
312     \Big] \\
313 \end{align*}
314
315 \paragraph{Example}
316 \begin{syntax}
317     node1 is \textbf{accept} [0x42-0x51]
318     node2 is \textbf{accept} [0x42]      // \textit{same as \textup{0x42-0x42}}
319     node3 is \textbf{accept} [0x0/12]    // \textit{same as \textup{0x0-0xFFF}}
320 \end{syntax}
321
322 \subsection{Map Specification}
323 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.
324 If no target base address is given, the block is translated to the target node starting at \Sockeye{0x0}.
325 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.
326 This was changed due to the mapping to \Sockeye{0x0} being used more often in practice.
327 Multiple translation targets can be specified by giving a comma-separated list of targets.
328
329 \paragraph{Syntax}
330 \begin{align*}
331 \textit{map}_s & \mathop{=}
332 \textit{block}_s\ \textbf{to}\ \textit{iden}\ 
333     \Big[
334         \textbf{at}\ \textit{addr}
335     \Big]\
336     \Big\{
337         \textbf{,}\ \textit{iden}\ 
338         \Big[
339             \textbf{at}\ \textit{addr}
340         \Big]
341     \Big\}\\
342 \end{align*}
343
344 \paragraph{Example}
345 \begin{syntax}
346     /* \textit{Translate \textup{0x0-0xFF} to \textup{node2} at \textup{0x300-0x3FF}:} */
347     node1 is \textbf{map} [0x0/8 \textbf{to} node2 \textbf{at} 0x300] 
348
349     /* \textit{This is the same as \textup{0x300/8 \textbf{to} node1 \textbf{at} 0x0}:} */
350     node2 is \textbf{map} [0x300/8 \textbf{to} node1]
351
352     /* \textit{Multiple translation targets, \textup{0x0-0xFF} is translated to
353        - \textup{node1} at \textup{0x0-0xFF}
354        - \textup{node2} at \textup{0x300-0x3FF}:} */
355     node3 is \textbf{map} [0x0/8 \textbf{to} node1, node2 \textbf{at} 0x300]
356 \end{syntax}
357
358 \section{Modules}
359 \label{sec:modules}
360 A module encapsulates a decoding net which can be integrated into a larger decoding net.
361 A module instantiation always creates a namespace inside the current one.
362 Normally nodes can only be referenced by nodes in the same namespace.
363 To properly integrate a module into a larger decoding net we need a mechanism to connect the module to the enclosing decoding net.
364 This is done via ports.
365 There are input ports, which create a connection into the module and output ports which create connections from the module to outside nodes.
366 A port has always a width, specified as the number of address bits the port spans.
367 All declared input ports must have a corresponding node declaration in the module body.
368
369 When a module is instantiated a list of port mappings can be specified.
370 An input port mapping creates a node outside the module that overlays the node inside the module.
371 An output port mapping creates a node inside the module that overlays the node outside the module.
372 Not all ports a module declares have to be mapped.
373 Not mapping an input port simply means there is no connection to the corresponding node inside the module.
374 For unmapped output ports an empty node inside the module will be generated, acting as a dead end for address resolution.
375
376 Additionally a module can be parametrized.
377 It will then be a module template that only becomes a fully defined module when instantiated with concrete arguments.
378 Module parameters are typed and the Sockeye compiler checks that they are used in a type safe way.
379 There are two types of parameters: address parameters and natural parameters.
380 Address parameters allow to parametrize addresses in node specifications.
381 Natural parameters are used in combination with interval template identifiers (see Section~\ref{sec:template_idens}).
382 Parameters can also be passed as arguments to module template instantiations in the module body.
383
384 \subsection{Module Declarations}
385 A module declaration starts with the keyword \Sockeye{module} and a unique module name.
386 If the module is a template, a list of typed parameters can be specified.
387 The module body is enclosed in curly braces and starts with the port definitions.
388 The rest of the body are node declarations and module instantiations.
389 If the module has address parameters the name of the parameter can be used wherever in the body an address is expected.
390
391 \paragraph{Syntax}
392 \begin{align*}
393     \textit{param\_type} & \mathop{=}
394         \textbf{addr}\ |\ \textbf{nat}\\
395     \textit{parameter} & \mathop{=}
396         \textit{param\_type}\ \textit{iden}\\
397     \textit{param\_list} & \mathop{=}
398         \textbf{(}\big[\ 
399             \textit{parameter}\big\{\textbf{,}\ \textit{parameter}\big\}\ 
400         \big] \textbf{)}\\
401     \textit{input\_port} & \mathop{=}
402         \textbf{input}\ \textit{iden}\textbf{/}\textit{decimal}
403         \big\{
404             \textbf{,}\ \textit{iden}\textbf{/}\textit{decimal}
405         \big\}\\
406     \textit{output\_port} & \mathop{=}
407         \textbf{output}\ \textit{iden}\textbf{/}\textit{decimal}
408         \big\{
409             \textbf{,}\ \textit{iden}\textbf{/}\textit{decimal}
410         \big\}\\
411     \textit{body}_s & \mathop{=}
412         \big\{\ 
413             \textit{net}_s\ |\ \textit{mod\_inst}_s\ 
414         \big\}\\
415     \textit{mod\_decl}_s & \mathop{=}
416         \textbf{module}\ \textit{iden} \big[\textit{param\_list}\big]\ 
417         \textbf{\{}\ 
418             \big\{\textit{input\_port}\ |\ \textit{output\_port}\big\}\ 
419             \textit{body}_s\ 
420         \textbf{\}}\\
421 \end{align*}
422
423 \subsection{Module Instantiations}
424 Module instantiations start with the module name and in the case of a module template with the list of arguments.
425 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.
426
427 \paragraph{Syntax}
428 \begin{align*}
429     \textit{argument} & \mathop{=}
430         \textit{decimal}\ |\ \textit{hexadecimal}\ |\ \textit{iden}\\
431     \textit{arg\_list} & \mathop{=}
432         \textbf{(}\big[\ 
433             \textit{argument}\big\{\textbf{,}\ \textit{argument}\big\}\ 
434         \big] \textbf{)}\\
435     \textit{mod\_inst}_s & \mathop{=}
436         \textit{iden} \big[\textit{arg\_list}\big]\ \textbf{as}\ \textit{iden}\ \big[\ 
437             \textbf{with}\ \big\{\textit{input\_map}\ |\ \textit{output\_map}\big\}\ 
438         \big]\\
439     \textit{input\_map} & \mathop{=}
440         \textit{iden}\ \textbf{>}\ \textit{iden}\\
441     \textit{output\_map} & \mathop{=}
442         \textit{iden}\ \textbf{<}\ \textit{iden}\\
443 \end{align*}
444
445 \clearpage
446 \paragraph{Example}
447 \begin{syntax}
448     /* Instantiate module 'SomeModule' in namespace 'subspace' /*
449     SomeModule \textbf{as} subspace
450
451     /* Pass arguments to module template */
452     TemplModule(0x0, 42) \textbf{as} templSubspace
453
454     /* Declare port mappings:
455        - map 'Node1' to ouptut port 'Out'
456        - map input port 'In' to 'Node2' */
457     SomeModule \textbf{as} subspace \textbf{with}
458         Node1 > Out
459         Node2 < In
460 \end{syntax}
461
462 \section{Templated Identifiers}
463 \label{sec:template_idens}
464 Templated identifiers allow to declare multiple nodes and ports at once and instantiate a module multiple times at once.
465 There are two forms of templated identifiers:
466 \begin{description}
467     \item[Interval template]
468         The template contains one or several intervals.
469         The identifier will be instantiated for all possible combinations of values in the intervals.
470         Index variables can optionally be named so they can be referenced later.
471     \item[Simple template]
472         Simple templates work very similar to interval templates.
473         The only difference is, that a simple template can only reference index variables declared in the same context.
474         It can not contain intervals to declare new index variables.
475 \end{description}
476
477 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).
478 The scope of index variables is the corresponding syntactic construct the interval template was used in.
479 Simple templates can be used in any place a node identifier is expected.
480 This includes the places where interval templates can be used, identifiers of translation destination nodes and overlays but not module parameter or index variable names.
481
482 An important thing to note is that the limits of an interval can reference module parameters of type \Sockeye{nat}.
483 This allows module parameters to control how many ports or nodes are instantiated from a certain interval template.
484
485 \paragraph{Syntax}
486 \begin{align*}
487     \textit{var} & \mathop{=}
488         \textit{iden}\\
489     \textit{limit} & \mathop{=}
490         \textit{decimal}\ |\ \textit{iden} \\
491     \textit{interval} & \mathop{=}
492         \textbf{[}\textit{limit}\textbf{..}\textit{limit}\textbf{]}\\
493     \textit{interval\_templ}_s & \mathop{=}
494         \textit{iden}\textbf{\{}\textit{var}\ \textbf{in}\ \textit{interval}\textbf{\}}
495         \Big[
496             \textit{iden}\ |\ \textit{templ\_iden}_s\ |\ \textit{for\_iden}_s
497         \Big]\\
498     \textit{simple\_templ}_s & \mathop{=}
499         \textit{iden}\textbf{\{}\textit{var}\textbf{\}}\Big[\textit{iden}\ |\ \textit{templ\_iden}_s\Big]\\
500 \end{align*}
501
502 \paragraph{Example}
503 \begin{syntax}
504     /* Declare similar nodes
505        (Note that interval templates in node declarations
506        always require the usage of '\textbf{are}') */
507     Device_\verb+{+[1..5]\verb+}+ \textbf{are} device \textbf{accept} [0x0/8]
508
509     /* Use the index in the node definition */
510     Map_\verb+{+m in [1..5]\verb+}+ \textbf{is} \textbf{map} [0x100/8 to Device_\verb+{+m\verb+}+]
511
512     /* Declare similar module ports
513        (possibly depending on module parameters) */
514     \textbf{module} SomeModule(nat num) \verb+{+
515         output Out_\verb+{+[1..num]\verb+}+
516         \ldots
517     \verb+}+
518
519     /* Instantiate module multiple times
520        and use index variable in port mappings */
521     SomeModule(3) \textbf{as} sub_module_\verb+{+m in [1..2]\verb+}+ \textbf{with}
522         Node_\verb+{+m\verb+}+_\verb+{+o in [1..3]\verb+}+ > Out_\verb+{+o\verb+}+
523 \end{syntax}
524
525 \section{Imports}
526 \label{sec:imports}
527 Imports allow a specification to be split across several files.
528 They also allow the reuse of modules.
529 Imports have to be specified at the very top of a Sockeye file.
530 An import will cause the compiler to load all modules from \pathname{<import\_path>.soc}
531 Nodes declared outside of modules will not be loaded.
532 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.
533
534 \paragraph{Syntax}
535 \begin{align*}
536 \textit{import}_s & \mathop{=}
537     \textbf{import}\ \big\{\ \textit{letter}\ |\ \textbf{/}\ \big\}
538 \end{align*}
539
540 \paragraph{Example}
541 \begin{syntax}
542     /* Invoked with 'sockeye -i imports -i modules' the following
543        will cause the compiler to look for the files
544        - ./subdir/core.soc
545        - imports/subdir/core.soc
546        - modules/subdir/core.soc
547        and import all modules from the first one that exists. */
548     \textbf{import} subdir/core
549 \end{syntax}
550
551 \section{Sockeye Files}
552 A sockeye file consists of imports, module declarations and the specification body (node declarations and module instantiations).
553
554 \paragraph{Syntax}
555 \begin{align*}
556     \textit{sockeye}_s & \mathop{=}
557         \big\{\ 
558             \textit{import}_s\ 
559         \big\}\ 
560         \big\{\ 
561             \textit{mod\_decl}_s\ 
562         \big\}\ 
563         \big\{\ 
564             \textit{net}_s\ |\ \textit{mod\_inst}_s\ 
565         \big\}
566 \end{align*}
567
568 \paragraph{Example}
569 Listing~\ref{lst:sockeye_example} shows an example Sockeye specification.
570 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}.
571
572 \clearpage
573 \lstinputlisting[caption={Example Sockeye specification}, label={lst:sockeye_example}, language=Sockeye]{example.soc}
574
575
576 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
577 \chapter{Checks on the AST}
578 \label{chap:checks}
579 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
580 The compiler performs the transformation from parsed Sockeye to decoding nets in three steps:
581 \begin{enumerate}
582     \item Type checker
583     \item Instantiator
584     \item Net builder
585 \end{enumerate}
586 In each of the steps some checks are performed.
587 The type checker checks that all referenced symbols (modules, parameters and index variables) are defined and ensures module template parameter type safety.
588 The instantiator instantiates module and identifier templates and ensures that each identifier is declared only once.
589 The net builder instantiates the modules and ensures referential integrity in the generated decoding net. It also transforms overlays to translation sets.
590 The checks are detailed in the following sections.
591
592 \section{Type Checker}
593 \subsection{Duplicate Modules}
594 This check makes sure that all module names in any of the imported files are unique.
595
596 \subsection{Duplicate Parameters}
597 This check makes sure that no module has two parameters with the same name.
598
599 \subsection{Duplicate Index Variables}
600 This check makes sure that no two index variables in the same scope have the same name.
601
602 \subsection{Undefined Modules}
603 This check makes sure that all modules being instantiated actually exist.
604
605 \subsection{Undefined Parameters}
606 This check makes sure that all referenced parameters are in scope.
607
608 \subsection{Undefined Index Variables}
609 This check makes sure that all index variables referenced in templated identifiers are in scope. 
610
611 \subsection{Parameter Type Mismatch}
612 This check makes sure that parameters are used in a type safe way.
613
614 \subsection{Argument Count Mismatch}
615 This check makes sure that module instantiations give the correct number of arguments to the module template being instantiated.
616
617 \subsection{Argument Type Mismatch}
618 This check makes sure that the arguments passed to module templates have the correct type.
619
620 \section{Instantiator}
621 \subsection{Module Instantiation Loops}
622 This check makes sure that there are no loops in module instantiations which would result in an infinite nesting of decoding subnets.
623
624 \subsection{Duplicate Namespaces}
625 This check makes sure that all module instantiations in a module have a unique namespace.
626
627 \subsection{Duplicate Identifiers}
628 This check makes sure that all node identifiers are unique.
629 This includes output ports, declared nodes and nodes mapped to input ports of instantiated modules.
630
631 \subsection{Duplicate Ports}
632 This check makes sure, that there are no duplicate input or output ports.
633 Note that declaring an output port with the same identifier as an input port is allowed and results in all address resolutions going through the input port being passed through the module to the output port.
634
635 \subsection{Duplicate Port Mapping}
636 This check makes sure that no port is mapped twice in the same module instantiation.
637
638 \section{Net Builder}
639
640 \subsection{Mapping to Undefined Port}
641 This check makes sure that there are no port mappings to ports not declared by the instantiated module.
642
643 \subsection{References to Undefined Nodes}
644 This check makes sure that all nodes referenced in translation sets, overlays and port mappings exist.
645 It also checks that every input port has a corresponding node declaration.
646
647
648 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
649 \chapter{Prolog Mapping for Sockeye}
650 \label{chap:prolog}
651 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
652 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.
653 A decoding net is expressed by the predicate \Prolog{net/2}.
654 The first argument to the predicate is the node identifier and the second one the node specification.
655
656 Node identifiers are represented as a functor \Prolog{nodeId/2}.
657 The first argument is the node's name, represented as an atom, and the second one is the (possibly nested) namespace it is in.
658 The namespace is represented as a list of atoms where the head is the innermost namespace component.
659
660 Node specifications are represented by a Prolog functor \Prolog{node/3}.
661 The arguments to the functor are the node type, the list of accepted addresses and the list of translated addresses.
662 The overlay is translated to address mappings and added to the list of translated addresses during compilation.
663
664 The node type is one of three atoms: \Prolog{device}, \Prolog{memory} or \Prolog{other}.
665 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.
666 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 target node's identifier and the third one is the base address for the mapping in the target node.
667
668 There is a predicate clause for \Prolog{net/2} for every node specified. 
669 Listings~\ref{lst:prolog_example} shows the generated Prolog code for the Sockeye example in Listing~\ref{lst:sockeye_example}.
670
671 \lstinputlisting[caption={Generated Prolog code},label={lst:prolog_example},language=Prolog]{example.pl}
672
673
674 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
675 \chapter{Compiling Sockeye Files with Hake}
676 \label{chap:hake}
677 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
678 SoC descriptions are placed in the directory \pathname{SOURCE/socs} with the file extension \pathname{soc}.
679 Each top-level Sockeye file has to be added to the list of SoCs in the Hakefile in the same directory.
680 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}.
681 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.
682 This causes \texttt{make} to rebuild the file also when imported files are changed.
683 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.
684
685
686 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
687 \bibliographystyle{abbrv}
688 \bibliography{defs,barrelfish}
689
690 \end{document}