Sockeye TN: Add description of template indentifiers
[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{amsmath}
14 \usepackage{bftn}
15 \usepackage{calc}
16 \usepackage{verbatim}
17 \usepackage{xspace}
18 \usepackage{pifont}
19 \usepackage{pxfonts}
20 \usepackage{textcomp}
21
22 \usepackage{multirow}
23 \usepackage{listings}
24 \usepackage{todonotes}
25 \usepackage{hyperref}
26
27 \title{Sockeye in Barrelfish}
28 \author{Barrelfish project}
29 % \date{\today}   % Uncomment (if needed) - date is automatic
30 \tnnumber{025}
31 \tnkey{Sockeye}
32
33
34 \lstdefinelanguage{Sockeye}{
35     morekeywords={is,are,accept,map,over,to,at},
36     sensitive=true,
37     morecomment=[l]{//},
38     morecomment=[s]{/*}{*/},
39     morestring=[b]",
40 }
41
42 \presetkeys{todonotes}{inline}{}
43
44 \begin{document}
45 \maketitle      % Uncomment for final draft
46
47 \begin{versionhistory}
48 \vhEntry{0.1}{15.06.2017}{DS}{Initial Version}
49 \end{versionhistory}
50
51 % \intro{Abstract}    % Insert abstract here
52 % \intro{Acknowledgements}  % Uncomment (if needed) for acknowledgements
53 \tableofcontents    % Uncomment (if needed) for final draft
54 % \listoffigures    % Uncomment (if needed) for final draft
55 % \listoftables     % Uncomment (if needed) for final draft
56 \cleardoublepage
57 \setcounter{secnumdepth}{2}
58
59 \newcommand{\fnname}[1]{\textit{\texttt{#1}}}%
60 \newcommand{\datatype}[1]{\textit{\texttt{#1}}}%
61 \newcommand{\varname}[1]{\texttt{#1}}%
62 \newcommand{\keywname}[1]{\textbf{\texttt{#1}}}%
63 \newcommand{\pathname}[1]{\texttt{#1}}%
64 \newcommand{\tabindent}{\hspace*{3ex}}%
65 \newcommand{\Sockeye}{\lstinline[language=Sockeye]}
66 \newcommand{\Prolog}{\lstinline[language=Prolog]}
67 \newcommand{\ccode}{\lstinline[language=C]}
68
69 \lstset{
70   basicstyle=\ttfamily \small,
71   keywordstyle=\bfseries,
72   flexiblecolumns=false,
73   basewidth={0.5em,0.45em},
74   boxpos=t,
75   captionpos=b,
76   frame=single,
77   breaklines=true,
78   postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space}
79 }
80
81
82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
83 \chapter{Introduction and usage}
84 \label{chap:introduction}
85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
86
87 \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. 
88 Source: \href{https://en.wikipedia.org/wiki/Sockeye_salmon}{Wikipedia}}
89 is a domain specific language to describe SoCs (Systems on a Chip).
90
91 Achermann~et~al.~\cite{achermann:mars17} propose a formal model to describe address spaces and interrupt routes in a system as a directed graph.
92 They call such a graph a ``decoding net''.
93 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).
94 Starting at a specific node addresses can be resolved by following the appropriate edges in the decoding net.
95 When a node translates an address, resolution is continued on that node.
96 When a node accepts an address, resolution terminates
97
98 Achermann~et~al.~\cite{achermann:mars17} also propose a concrete syntax for specifying decoding nets.
99 Sockeye is an implementation of the language introduced in but adds some features to address issues encountered in practice.
100
101 The Sockeye compiler is written in Haskell using the Parsec parsing library. It
102 generates Prolog files from the Sockeye files. These Prolog files contain facts that represent a decoding net (see Chapter~\ref{chap:prolog}).
103 The Prolog files can then be loaded into Barrelfish's System Knowledgebase (SKB).
104
105 The source code for Sockeye can be found in \pathname{SOURCE/tools/sockeye}.
106
107
108 \section{Command line options}
109
110 \begin{verbatim}
111 $ sockeye [options] file
112 \end{verbatim}
113
114
115 The available options are:
116 \begin{description}
117 \item[-P] Generate a Prolog file that can be loaded into the SKB.
118 \item[-i] Add a directory to the search path where Sockeye looks for imports.
119 \item[-o] \varname{filename} The path to the output file
120 \item[-h] show usage information
121 \end{description}
122
123 The backend (capital letter options) specified last takes precedence.
124
125 Multiple directories can be added by giving the \texttt{-i} options multiple times.
126 Sockeye will first look for files in the current directory and then check the given directories in the order they were given.
127
128 The Sockeye file to compile is given via the \texttt{file} parameter.
129
130
131 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
132 \chapter{Lexical Conventions}
133 \label{chap:lexer}
134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
135
136 The Sockeye parser follows a similar convention as opted by modern day 
137 programming languages like C and Java. Hence, Sockeye uses a Java-style-like
138 parser based on the Haskell Parsec Library. The following conventions are used:
139
140 \begin{description}
141 \item[Encoding] The file should be encoded using plain text.
142 \item[Whitespace:]  As in C and Java, Sockeye considers sequences of
143   space, newline, tab, and carriage return characters to be
144   whitespace.  Whitespace is generally not significant. 
145
146 \item[Comments:] Sockeye supports C-style comments.  Single line comments
147   start with \texttt{//} and continue until the end of the line.
148   Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
149   anything in between is ignored and treated as white space.
150   Nested comments are not supported.
151
152 \item[Identifiers:] Valid Sockeye identifiers are sequences of numbers
153   (0-9), letters (a-z, A-Z), the underscore character ``\texttt{\_}'' and the dash character ``\textendash''. They
154   must start with a letter.
155   \begin{align*}
156   identifier & \rightarrow letter (letter \mid digit \mid \text{\_} \mid \text{\textendash})^{\textrm{*}} \\
157   letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
158   digit & \rightarrow (\textsf{0 \ldots 9})
159     \end{align*}
160
161 \item[Case sensitivity:] Sockeye is case sensitive hence identifiers \Sockeye{node1} and \Sockeye{Node2} are not the same.
162   
163 \item[Integer Literals:] A Sockeye integer literal is a sequence of
164   digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
165   literals have no specifier and hexadecimal literals start with
166   \texttt{0x}.
167
168 \begin{align*}
169 decimal & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
170 hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
171 \end{align*}
172
173 \item[Reserved words:] The following are reserved words in Sockeye:
174 \begin{verbatim}
175 accept, are, as, at, import, in, input, is, map,
176 module, output, over, reserved, to, with
177 \end{verbatim}
178
179 \end{description}
180
181
182 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
183 \chapter{Decoding Net }
184 \label{chap:declaration}
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
186
187 In this chapter we define the layout of a Sockeye file.
188 The node declarations in a Sockeye file describe a single decoding net.
189 Parts of a decoding net can be packaged into reusable modules (see Section~\ref{sec:modules}).
190 With imports (see Section~\ref{sec:imports}) modules can also be put into separate files.
191 Also an SoC can be split into multiple decoding nets e.g. one for the address spaces and another one for the interrupt routes.
192
193 In the following sections we use EBNF to specify the Sockeye syntax. Terminals are \textbf{bold} while non-terminals are \textit{italic}.
194 The non-terminals \textit{iden}, \textit{letter}, \textit{decimal} and \textit{hexadecimal} correspond to the ones defined in Chapter~\ref{chap:lexer}.
195
196 \section{Basic Syntax}
197
198 \subsection{Node declarations}
199 A node declaration contains one or more identifiers and the node specification.
200 The order in which the nodes are declared does not matter.
201
202 \paragraph{Syntax}
203 \begin{align*}
204 \textit{net}_s & \mathop{=}
205     \Big\{
206         \textit{iden}\ \textbf{is}\ \textit{node}_s\
207     \Big|\
208         \bigl\{ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
209     \Big\} \\
210 \end{align*}
211
212 \paragraph{Example}
213 \begin{syntax}
214     node1 \textbf{is} \ldots
215
216     node2
217     node3 \textbf{are} \ldots
218 \end{syntax}
219
220 \subsection{Node specifications}
221 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.
222 All of these are optional.
223 The reserved address blocks are only relevant in conjunction with overlays and are used to exclude some addresses from the overlay.
224 The overlay is specified as a node identifier and a number of address bits.
225 The overlay will take effect from \texttt{0x0} to \(\texttt{0x2}^\texttt{bits} - \texttt{1}\).
226
227 \paragraph{Syntax}
228 \begin{align*}
229 \textit{node}_s & \mathop{=}
230     \Big[\ 
231        \textit{type}\ 
232     \Big]\  
233     \Big[
234        \textit{accept}\ 
235     \Big]\ 
236     \Big[\ 
237        \textit{map}\ 
238     \Big]\ 
239     \Big[\ 
240         \textit{reserved}\ 
241     \Big]\ 
242     \Big[\ 
243         \textit{overlay}\ 
244     \Big]\\
245 \textit{accept} & \mathop{=}
246     \textbf{accept [}\ \big[\ \textit{block}_s\big\{\textbf{,}\ \textit{block}_s\big\}\ \big]\ \textbf{]}\\
247 \textit{map} & \mathop{=}
248     \textbf{map [}\ \big[\ \textit{map}_s\big\{\textbf{,}\ \textit{map}_s\big\}\ \big]\ \textbf{]}\\
249 \textit{reserved} & \mathop{=}
250     \textbf{reserved [}\ \big[\textit{block}_s\big\{\textbf{,}\ \textit{block}_s\big\}\ \big]\ \textbf{]}\\
251 \textit{overlay} & \mathop{=}
252     \textbf{over}\ \textit{iden}\textbf{/}\textit{decimal}\\
253 \end{align*}
254
255 \paragraph{Example}
256 \begin{syntax}
257     node1 \textbf{is} \textit{<type>} \textbf{accept} [\ldots]
258     node2 \textbf{is} \textbf{map} [\ldots]
259     node3 \textbf{is} \textbf{reserved} [\ldots] \textbf{over} node2/32
260 \end{syntax}
261
262 \subsection{Node type}
263 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.
264 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.
265
266 \paragraph{Syntax}
267 \begin{align*}
268 \textit{type} & \mathop{=}
269     \textbf{device}\
270     |\
271     \textbf{memory} \\
272 \end{align*}
273
274 \paragraph{Example}
275 \begin{syntax}
276     node1 \textbf{is} memory \textbf{accept} [\ldots]
277     node2 \textbf{is} device \textbf{accept} [\ldots]
278 \end{syntax}
279
280 \clearpage
281 \subsection{Addresses}
282 Addresses are specified as hexadecimal literals.
283
284 \paragraph{Syntax}
285 \begin{align*}
286 \textit{addr} & \mathop{=} \textit{hexadecimal} \\
287 \end{align*}
288
289 \subsection{Block specification}{}
290 A block is specified by its start and end address.
291 If the start and end address are the same, the end address can be omitted.
292 Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
293 A block from \Sockeye{0x0} to \Sockeye{0xFFF} with a size of 4kB can be specified as \Sockeye{0x0/12}.
294
295 \paragraph{Syntax}
296 \begin{align*}
297 \textit{block}_s & \mathop{=} \textit{addr}\
298     \Big[
299         \textbf{-}\ \textit{addr}\ 
300     \Big|\
301         \textbf{/}decimal
302     \Big] \\
303 \end{align*}
304
305 \paragraph{Example}
306 \begin{syntax}
307     node1 is \textbf{accept} [0x42-0x51]
308     node2 is \textbf{accept} [0x42]      // \textit{same as \textup{0x42-0x42}}
309     node3 is \textbf{accept} [0x0/12]    // \textit{same as \textup{0x00-0xFFF}}
310 \end{syntax}
311
312 \subsection{Map specification}
313 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.
314 If no target base address is given, the block is translated to the target node starting at \Sockeye{0x0}.
315 Note that this is different from the concrete syntax described in \cite{achermann:mars17} where unspecified base address means use the base address of the source block.
316 This was changed due to the mapping to \Sockeye{0x0} being used more often in practice.
317 Multiple translation targets can be specified by giving a comma-separated list of targets.
318
319 \paragraph{Syntax}
320 \begin{align*}
321 \textit{map}_s & \mathop{=}
322 \textit{block}_s\ \textbf{to}\ \textit{iden}\ 
323     \Big[
324         \textbf{at}\ \textit{addr}
325     \Big]\
326     \Big\{
327         \textbf{,}\ \textit{iden}\ 
328         \Big[
329             \textbf{at}\ \textit{addr}
330         \Big]
331     \Big\}\\
332 \end{align*}
333
334 \paragraph{Example}
335 \begin{syntax}
336     /* \textit{Translate \textup{0x0-0xFF} to \textup{node2} at \textup{0x300-0x3FF}:} */
337     node1 is \textbf{map} [0x0/8 \textbf{to} node2 \textbf{at} 0x300] 
338
339     /* \textit{This is the same as \textup{0x300/8 \textbf{to} node1 \textbf{at} 0x0}:} */
340     node2 is \textbf{map} [0x300/8 \textbf{to} node1]
341
342     /* \textit{Multiple translation targets, \textup{0x0-0xFF} is translated to
343        - \textup{node1} at \textup{0x0-0xFF}
344        - \textup{node2} at \textup{0x300-0x3FF}:} */
345     node3 is \textbf{map} [0x0/8 \textbf{to} node1, node2 \textbf{at} 0x300]
346 \end{syntax}
347
348 \section{Modules}
349 \label{sec:modules}
350
351 \section{Templated Identifiers}
352 Templated identifiers allow to declare multiple nodes and ports at once and instantiate a module multiple times at once.
353 There are two forms of templated identifiers:
354 \begin{description}
355     \item[Interval template]
356         The template contains one or several intervals.
357         The identifier will be instantiated for all possible combinations of values in the intervals.
358         Index variables can optionally be named so they can be referenced later.
359     \item[Simple template]
360         Simple templates work very similar to interval templates.
361         The only difference is, that a simple template can only reference index variables declared in the same context.
362         It can not contain intervals which declare new index variables.
363 \end{description}
364
365 Interval templates can be used in identifiers of node declarations (to declare multiple nodes at once), port declarations (to declare multiple ports at once) and namespaces of module instantiations (to instantiate a module multiple times).
366 The scope of index variables is the corresponding syntactic construct the interval template was used in.
367 Simple templates can be used in any place a node identifier is expected.
368
369 An important thing to note is that the limits of an interval can reference module parameters of type \Sockeye{nat}.
370 This allows module parameters to control the number of certain nodes in a module declaration.
371
372 \paragraph{Syntax}
373 \begin{align*}
374     \textit{limit} & \mathop{=}
375         \textit{decimal}\ |\ \textit{iden} \\
376     \textit{interval}_s & \mathop{=}
377         \textbf{[}\textit{limit}\textbf{..}\textit{limit}\textbf{]}\\
378     \textit{for\_iden}_s & \mathop{=}
379         \textit{iden}\textbf{\{}\textit{var}\ \textbf{in}\ \textit{interval}_s\textbf{\}}
380         \Big[
381             \textit{iden}\ |\ \textit{templ\_iden}_s\ |\ \textit{for\_iden}_s
382         \Big]\\
383     \textit{var} & \mathop{=}
384         \textit{iden}\\
385     \textit{templ\_iden}_s & \mathop{=}
386         \textit{iden}\textbf{\{}\textit{var}\textbf{\}}\Big[\textit{iden}\ |\ \textit{templ\_iden}_s\Big]\\
387 \end{align*}
388
389 \paragraph{Example}
390 \begin{syntax}
391     /* Declare similar nodes
392        (Note that interval templates always require the usage of 'are' */
393     Device_\verb+{+[1..5]\verb+}+ \textbf{are} device \textbf{accept} [0x0/8]
394
395     /* Use the index in the node definition */
396     Map_\verb+{+m in [1..5]\verb+}+ \textbf{is} \textbf{map} [0x100/8 to Device_\verb+{+m\verb+}+]
397
398     /* Declare similar module ports
399        (possibly depending on module parameters) */
400     \textbf{module} SomeModule(nat num) \verb+{+
401         output Out_\verb+{+[1..num]\verb+}+
402         \ldots
403     \verb+}+
404
405     /* Instantiate module multiple times
406        and use index variable in port mappings*/
407     SomeModule(3) \textbf{as} sub_module_\verb+{+m in [1..2]\verb+}+ \textbf{with}
408         Node_\verb+{+m\verb+}+_\verb+{+o in [1..3]\verb+}+ > Out_\verb+{+o\verb+}+
409 \end{syntax}
410
411 \section{Imports}
412 \label{sec:imports}
413 Imports allow a specification to be divided over several files.
414 They also allow the reuse of declared modules.
415 Imports have to be specified at the very top of a Sockeye file.
416 An import will cause the compiler to load all modules from \pathname{<import\_path>.soc}
417 Nodes declared outside of modules will not be loaded.
418 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.
419
420 \paragraph{Syntax}
421 \begin{align*}
422 \textit{import}_s & \mathop{=}
423     \textbf{import}\ \big\{\ \textit{letter}\ |\ \textbf{/}\ \big\}
424 \end{align*}
425
426 \paragraph{Example}
427 \begin{syntax}
428     /* Invoked with 'sockeye -i imports -i modules' this will cause
429        the compiler to look for the files
430        - ./subdir/core.soc
431        - imports/subdir/core.soc
432        - modules/subdir/core.soc
433        and import all modules from the first one that exists. */
434     \textbf{import} subdir/core
435 \end{syntax}
436
437 \clearpage
438 \section{Example Specification}
439 Listing~\ref{lst:sockeye_example} shows an example Sockeye specification.
440
441 \lstinputlisting[caption={Example Sockeye specification}, label={lst:sockeye_example}, language=Sockeye]{example.soc}
442
443 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}.
444
445
446 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
447 \chapter{Checks on the AST}
448 \label{chap:checks}
449 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
450 The Sockeye compiler performs some sanity checks on the parsed AST.
451
452 \section{No Duplicate Identifiers}
453 This check makes sure that there aren't two node declarations with the same identifier.
454
455 \section{No References to Undefined Nodes}
456 This check makes sure that all nodes referenced in translation sets and overlays are declared.
457
458
459 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
460 \chapter{Prolog Mapping for Sockeye}
461 \label{chap:prolog}
462 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
463 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.
464 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.
465 The second argument is the node specification, a Prolog functor with the name \Prolog{node} and an arity of three.
466 The arguments of the functor are the node type, the list of accepted addresses and the list of translated addresses.
467 The overlay is translated to address mappings and added to the list of translated addresses during compilation.
468
469 The node type is one of three atoms: \Prolog{device}, \Prolog{memory} or \Prolog{other}.
470 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.
471 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.
472
473 There is a predicate clause for \Prolog{net/2} for every node specified. 
474 Listings~\ref{lst:prolog_example} shows the generated Prolog code for the Sockeye example in Listing~\ref{lst:sockeye_example}.
475
476 \lstinputlisting[caption={Generated Prolog code},label={lst:prolog_example},language=Prolog]{example.pl}
477
478
479 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
480 \chapter{Compiling Sockeye files with Hake}
481 \label{chap:hake}
482 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
483 SoC descriptions are placed in the directory \pathname{SOURCE/socs} with the file extension \pathname{soc}.
484 Each top-level Sockeye file has to be added to the list of SoCs in the Hakefile in the same directory.
485 The Hake rule for Sockeye files compiles all the listed files to \pathname{BUILD/sockeyefacts/<filename>.pl} if they are specified as a dependency in some Hakefile.
486 The rule will also generate a \pathname{.depend} file (with the \texttt{-d} option of the Sockeye compiler) so that \texttt{make} recompiles the file also when imported files are changed.
487 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.
488
489
490 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
491 \bibliographystyle{abbrv}
492 \bibliography{defs,barrelfish}
493
494 \end{document}