Sockeye TN: Update usage info
[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 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 inbetween 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}. Octal literals start with \texttt{0o}.
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 octal & \rightarrow (\textsf{0o})(\textsf{0 \ldots 7})^{\textrm{1}}\\
172 \end{align*}
173
174 \item[Reserved words:] The following are reserved words in Sockeye:
175 \begin{verbatim}
176 is, are, accept, map, over, to, at
177 \end{verbatim}
178
179 \end{description}
180
181
182 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
183 \chapter{Decoding Net Declaration}
184 \label{chap:declaration}
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
186
187 In this chapter we define the layout of a Sockeye file. Each Sockeye file contains the declaration of a single decoding net.
188 An SoC can be split into multiple decoding nets e.g. one for the address spaces and another one for the interrupt routes.
189 However a node in a decoding net can not reference a node in a different decoding net (see also Section~\ref{sec:modularity} for further information).
190
191 \section{Syntax}
192
193 \subsection{Syntax Specification}
194 We use EBNF to specify the Sockeye syntax. Terminals are \textbf{bold}.
195 The non-terminals \textit{iden}, \textit{integer} and \textit{decimal} correspond to identifiers, integer literals and decimal literals from Chapter~\ref{chap:lexer}.
196
197 \subsection{Net specification}
198 A net consists of one or more 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 \begin{align*}
203 \textit{net}_s & \mathop{=}
204         \Big\{
205                 \textit{iden}\ \textbf{is}\ \textit{node}_s\
206         \Big|\
207                 \bigl\{ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
208         \Big\} \\
209 \end{align*}
210
211 \paragraph{Example}
212 \begin{syntax}
213         node1 \textbf{is} \ldots
214
215         node2
216         node3 \textbf{are} \ldots
217 \end{syntax}
218
219 \subsection{Node specifications}
220 A node specification consists of a type, a set of accepted addresses, a set of translated addresses and an overlay.
221 All of these are optional.
222
223 \begin{align*}
224 \textit{node}_s & \mathop{=}
225         \Big[
226                 \textit{type}
227         \Big]\  
228         \Big[
229                 \textbf{accept [}\ \big\{\textit{block}_s\big\}\ \textbf{]}\ 
230         \Big]\ 
231         \Big[
232                 \textbf{map [}\ \big\{\textit{map}_s\big\}\ \textbf{]}\ 
233         \Big]\ 
234         \Big[
235                 \textbf{over}\ \textit{iden}
236         \Big] \\
237 \end{align*}
238
239 \paragraph{Example}
240 \begin{syntax}
241         node1 \textbf{is} \textit{<type>} \textbf{accept} [\ldots]
242         node2 \textbf{is} \textbf{map} [\ldots] \textbf{over} node1
243 \end{syntax}
244
245 \subsection{Node type}
246 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.
247 The \verb|device|-type specifies that the accepted addresses are device registers while the \Sockeye{memory}-type is for memory nodes like RAM or ROM.
248
249 \begin{align*}
250 \textit{type} & \mathop{=}
251         \textbf{device}\
252         |\
253         \textbf{memory} \\
254 \end{align*}
255
256 \paragraph{Example}
257 \begin{syntax}
258         node1 \textbf{is} memory \textbf{accept} [\ldots]
259         node2 \textbf{is} device \textbf{accept} [\ldots]
260 \end{syntax}
261
262 \subsection{Addresses}
263 Addresses can be given as hexadecimal, octal or decimal integers.
264 \begin{align*}
265 \textit{addr} & \mathop{=} \textit{integer} \\
266 \end{align*}
267
268 \clearpage
269 \subsection{Block specification}{}
270 A block is specified by its start and end address.
271 If the start and end address are the same, the end address can be omitted.
272 Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
273 A block from \texttt{0x0} to \texttt{0xFFF} with a size of 4kB can be specified as \Sockeye|0x0/12|.
274
275 \begin{align*}
276 \textit{block}_s & \mathop{=} \textit{addr}\
277         \Big[
278                 \textbf{-}\ \textit{addr}\ 
279         \Big|\
280                 \textbf{/}decimal
281         \Big] \\
282 \end{align*}
283
284 \paragraph{Example}
285 \begin{syntax}
286         node1 is \textbf{accept} [0x42-0x51]
287         node2 is \textbf{accept} [0x42]      // \textit{same as \textup{0x42-0x42}}
288         node3 is \textbf{accept} [0x0/12]    // \textit{same as \textup{0x00-0xFFF}}
289 \end{syntax}
290
291 \subsection{Map specification}
292 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.
293 If no target base address is given, the block is translated to the same addresses within the target node.
294 Multiple translation targets can be specified by giving a comma-separated list of targets.
295
296 \begin{align*}
297 \textit{map}_s & \mathop{=}
298 \textit{block}_s\ \textbf{to}\ \textit{iden}\ 
299         \Big[
300                 \textbf{at}\ \textit{addr}
301         \Big]\
302         \Big\{
303                 \textbf{,}\ \textit{iden}\ 
304                 \Big[
305                         \textbf{at}\ \textit{addr}
306                 \Big]
307         \Big\} \\
308 \end{align*}
309
310 \paragraph{Example}
311 \begin{syntax}
312         /* \textit{Translate \textup{0x0-0xFF} to \textup{node2} at \textup{0x300-0x3FF}:} */
313         node1 is \textbf{map} [0x0/8 \textbf{to} node2 \textbf{at} 0x300] 
314
315         /* \textit{This is the same as \textup{0x300/8 \textbf{to} node1 \textbf{at} 0x300}:} */
316         node2 is \textbf{map} [0x300/8 \textbf{to} node1]
317
318         /* \textit{Multiple translation targets, \textup{0x0-0xFF} is translated to
319            - \textup{node1} at \textup{0x0-0xFF}
320            - \textup{node2} at \textup{0x300-0x3FF}:} */
321         node3 is \textbf{map} [0x0/8 \textbf{to} node1, node2 \textbf{at} 0x300]
322 \end{syntax}
323
324 \section{Example Specification}
325 Listing~\ref{lst:sockeye_example} shows an example Sockeye specification.
326
327 \lstinputlisting[caption={Example Sockeye specification}, label={lst:sockeye_example}, language=Sockeye]{example.soc}
328
329 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/omap4460.soc}.
330
331
332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
333 \chapter{Checks on the AST}
334 \label{chap:checks}
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
336 The Sockeye compiler performs some sanity checks on the parsed AST.
337
338 \section{No Duplicate Identifiers}
339 This check makes sure that there aren't two node declarations with the same identifier.
340
341 \section{No References to Undefined Nodes}
342 This check makes sure that all nodes referenced in translation sets and overlays are declared in the same file.
343
344
345 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
346 \chapter{Prolog Mapping for Sockeye}
347 \label{chap:prolog}
348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
349 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.
350 A decoding net is expressed by the predicate \Prolog{net/2}. The first argument to the predicate is the node identifier represented as a Prolog atom.
351 The second argument is the node specification, a Prolog functor with the name \Prolog{node} and an arity of four. The arguments of the functor are the node type, the list of accepted addresses, the list of translated addresses and the overlay.
352
353 The node type is one of three atoms: \Prolog{device}, \Prolog{memory} or \Prolog{other}.
354 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.
355 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.
356 The overlay is represented as an atom which is either the node identifier of the overlay node or \Prolog{'@none'} for nodes with no overlay.
357
358 There is a predicate clause for \Prolog{net/2} for every node specified. 
359 Listings~\ref{lst:prolog_example} shows the generated Prolog code for the Sockeye example in Listing~\ref{lst:sockeye_example}.
360
361 \lstinputlisting[caption={Generated Prolog code},label={lst:prolog_example},language=Prolog]{example.pl}
362
363
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
365 \chapter{Compiling Sockeye files with Hake}
366 \label{chap:hake}
367 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
368 SoC descriptions are placed in the directory \pathname{SOURCE/socs} with the file extension \pathname{soc}.
369 Each top-level Sockeye file has to be added to the list of SoCs in the Hakefile in the same directory.
370 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.
371 The rule will also generate a \pathname{.depend} file so that make recompiles the file also when imported files are changed.
372 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.
373
374
375 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
376 \bibliographystyle{abbrv}
377 \bibliography{defs,barrelfish}
378
379 \end{document}