bdb3acaa24ce0f4a92105783584cb648d6b56cda
[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 It is an implementation of the language introduced in \cite{achermann:mars17} but adds some features to address issues encountered in practise.
91
92 \todo{Add short introduction on decoding nets.}
93
94 The Sockeye compiler is written in Haskell using the Parsec parsing library. It
95 generates Prolog files from the Sockeye files. These Prolog files contain facts that represent a decoding net as defined in \cite{achermann:mars17}.
96 The Prolog files can then be loaded into Barrelfish's System Knowledgebase (SKB).
97
98 The source code for Sockeye can be found in \pathname{SOURCE/tools/sockeye}.
99
100
101 \section{Command line options}
102
103 \begin{verbatim}
104 $ sockeye [options] file
105 \end{verbatim}
106
107
108 The available options are:
109 \begin{description}
110 \item[-P] Generate a Prolog file that can be loaded into the SKB.
111 \item[-C] Just perform checks, do not compile.
112 \item[-o] \varname{filename} The path to the output file (including the file extension)
113 \item[-h] show usage information
114 \end{description}
115
116 The backend (capital letter options) specified last takes precedence.
117
118 The Sockeye file to compile is given via the \textit{file} parameter.
119
120
121 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
122 \chapter{Lexical Conventions}
123 \label{chap:lexer}
124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
125
126 The Sockeye parser follows a similar convention as opted by modern day 
127 programming languages like C and Java. Hence, Sockeye uses a Java-style-like
128 parser based on the Haskell Parsec Library. The following conventions are used:
129
130 \begin{description}
131 \item[Encoding] The file should be encoded using plain text.
132 \item[Whitespace:]  As in C and Java, Sockeye considers sequences of
133   space, newline, tab, and carriage return characters to be
134   whitespace.  Whitespace is generally not significant. 
135
136 \item[Comments:] Sockeye supports C-style comments.  Single line comments
137   start with \texttt{//} and continue until the end of the line.
138   Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
139   anything inbetween is ignored and treated as white space.
140   Nested comments are not supported.
141
142 \item[Identifiers:] Valid Sockeye identifiers are sequences of numbers
143   (0-9), letters (a-z, A-Z), the underscore character ``\texttt{\_}'' and the dash character ``\textendash''. They
144   must start with a letter.
145   \begin{align*}
146   identifier & \rightarrow letter (letter \mid digit \mid \text{\_} \mid \text{\textendash})^{\textrm{*}} \\
147   letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
148   digit & \rightarrow (\textsf{0 \ldots 9})
149         \end{align*}
150
151 \item[Case sensitivity:] Sockeye is case sensitive hence identifiers \Sockeye{node1} and \Sockeye{Node2} are not the same.
152   
153 \item[Integer Literals:] A Sockeye integer literal is a sequence of
154   digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
155   literals have no specifier and hexadecimal literals start with
156   \texttt{0x}. Octal literals start with \texttt{0o}.
157
158 \begin{align*}
159 decimal & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
160 hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
161 octal & \rightarrow (\textsf{0o})(\textsf{0 \ldots 7})^{\textrm{1}}\\
162 \end{align*}
163
164 \item[Reserved words:] The following are reserved words in Sockeye:
165 \begin{verbatim}
166 is, are, accept, map, over, to, at
167 \end{verbatim}
168
169 \end{description}
170
171
172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
173 \chapter{Decoding Net Declaration}
174 \label{chap:declaration}
175 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
176
177 In this chapter we define the layout of a Sockeye file. Each Sockeye file contains the declaration of a single decoding net.
178 An SoC can be split into multiple decoding nets e.g. one for the address spaces and another one for the interrupt routes.
179 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).
180
181 \section{Syntax}
182
183 \subsection{Syntax Specification}
184 We use EBNF to specify the Sockeye syntax. Terminals are \textbf{bold}.
185 The non-terminals \textit{iden}, \textit{integer} and \textit{decimal} correspond to identifiers, integer literals and decimal literals from Chapter~\ref{chap:lexer}.
186
187 \subsection{Net specification}
188 A net consists of one or more node declarations.
189 A node declaration contains one or more identifiers and the node specification.
190 The order in which the nodes are declared does not matter.
191
192 \begin{align*}
193 \textit{net}_s & \mathop{=}
194         \Big\{
195                 \textit{iden}\ \textbf{is}\ \textit{node}_s\
196         \Big|\
197                 \bigl\{ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
198         \Big\} \\
199 \end{align*}
200
201 \paragraph{Example}
202 \begin{syntax}
203         node1 \textbf{is} \ldots
204
205         node2
206         node3 \textbf{are} \ldots
207 \end{syntax}
208
209 \subsection{Node specifications}
210 A node specification consists of a type, a set of accepted addresses, a set of translated addresses and an overlay.
211 All of these are optional.
212
213 \begin{align*}
214 \textit{node}_s & \mathop{=}
215         \Big[
216                 \textit{type}
217         \Big]\  
218         \Big[
219                 \textbf{accept [}\ \big\{\textit{block}_s\big\}\ \textbf{]}\ 
220         \Big]\ 
221         \Big[
222                 \textbf{map [}\ \big\{\textit{map}_s\big\}\ \textbf{]}\ 
223         \Big]\ 
224         \Big[
225                 \textbf{over}\ \textit{iden}
226         \Big] \\
227 \end{align*}
228
229 \paragraph{Example}
230 \begin{syntax}
231         node1 \textbf{is} \textit{<type>} \textbf{accept} [\ldots]
232         node2 \textbf{is} \textbf{map} [\ldots] \textbf{over} node1
233 \end{syntax}
234
235 \subsection{Node type}
236 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.
237 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.
238
239 \begin{align*}
240 \textit{type} & \mathop{=}
241         \textbf{device}\
242         |\
243         \textbf{memory} \\
244 \end{align*}
245
246 \paragraph{Example}
247 \begin{syntax}
248         node1 \textbf{is} memory \textbf{accept} [\ldots]
249         node2 \textbf{is} device \textbf{accept} [\ldots]
250 \end{syntax}
251
252 \subsection{Addresses}
253 Addresses can be given as hexadecimal, octal or decimal integers.
254 \begin{align*}
255 \textit{addr} & \mathop{=} \textit{integer} \\
256 \end{align*}
257
258 \clearpage
259 \subsection{Block specification}{}
260 A block is specified by its start and end address.
261 If the start and end address are the same, the end address can be omitted.
262 Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
263 A block from \texttt{0x0} to \texttt{0xFFF} with a size of 4kB can be specified as \Sockeye|0x0/12|.
264
265 \begin{align*}
266 \textit{block}_s & \mathop{=} \textit{addr}\
267         \Big[
268                 \textbf{-}\ \textit{addr}\ 
269         \Big|\
270                 \textbf{/}decimal
271         \Big] \\
272 \end{align*}
273
274 \paragraph{Example}
275 \begin{syntax}
276         node1 is \textbf{accept} [0x42-0x51]
277         node2 is \textbf{accept} [0x42]      // \textit{same as \textup{0x42-0x42}}
278         node3 is \textbf{accept} [0x0/12]    // \textit{same as \textup{0x00-0xFFF}}
279 \end{syntax}
280
281 \subsection{Map specification}
282 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.
283 If no target base address is given, the block is translated to the same addresses within the target node.
284 Multiple translation targets can be specified by giving a comma-separated list of targets.
285
286 \begin{align*}
287 \textit{map}_s & \mathop{=}
288 \textit{block}_s\ \textbf{to}\ \textit{iden}\ 
289         \Big[
290                 \textbf{at}\ \textit{addr}
291         \Big]\
292         \Big\{
293                 \textbf{,}\ \textit{iden}\ 
294                 \Big[
295                         \textbf{at}\ \textit{addr}
296                 \Big]
297         \Big\} \\
298 \end{align*}
299
300 \paragraph{Example}
301 \begin{syntax}
302         /* \textit{Translate \textup{0x0-0xFF} to \textup{node2} at \textup{0x300-0x3FF}:} */
303         node1 is \textbf{map} [0x0/8 \textbf{to} node2 \textbf{at} 0x300] 
304
305         /* \textit{This is the same as \textup{0x300/8 \textbf{to} node1 \textbf{at} 0x300}:} */
306         node2 is \textbf{map} [0x300/8 \textbf{to} node1]
307
308         /* \textit{Multiple translation targets, \textup{0x0-0xFF} is translated to
309            - \textup{node1} at \textup{0x0-0xFF}
310            - \textup{node2} at \textup{0x300-0x3FF}:} */
311         node3 is \textbf{map} [0x0/8 \textbf{to} node1, node2 \textbf{at} 0x300]
312 \end{syntax}
313
314 \section{Example Specification}
315 Listing~\ref{lst:sockeye_example} shows an example Sockeye specification.
316
317 \lstinputlisting[caption={Example Sockeye specification}, label={lst:sockeye_example}, language=Sockeye]{example.soc}
318
319 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}.
320
321
322 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
323 \chapter{Checks on the AST}
324 \label{chap:checks}
325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
326 The Sockeye compiler performs some sanity checks on the parsed AST.
327
328 \section{No Duplicate Identifiers}
329 This check makes sure that there aren't two node declarations with the same identifier.
330
331 \section{No References to Undefined Nodes}
332 This check makes sure that all nodes referenced in translation sets and overlays are declared in the same file.
333
334
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
336 \chapter{Prolog Mapping for Sockeye}
337 \label{chap:prolog}
338 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
339 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.
340 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.
341 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.
342
343 The node type is one of three atoms: \Prolog{device}, \Prolog{memory} or \Prolog{other}.
344 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.
345 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.
346 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.
347
348 There is a predicate clause for \Prolog{net/2} for every node specified. 
349 Listings~\ref{lst:prolog_example} shows the generated Prolog code for the Sockeye example in Listing~\ref{lst:sockeye_example}.
350
351 \lstinputlisting[caption={Generated Prolog code},label={lst:prolog_example},language=Prolog]{example.pl}
352
353
354 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
355 \chapter{Compiling Sockeye files with Hake}
356 \label{chap:hake}
357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
358 SoC descriptions are placed in the directory \pathname{SOURCE/socs} with the file extension \pathname{soc}.
359 Each top-level Sockeye file has to be added to the list of SoCs in the Hakefile in the same directory.
360 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.
361 The rule will also generate a \pathname{.depend} file so that make recompiles the file also when imported files are changed.
362 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.
363
364
365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
366 \bibliographystyle{abbrv}
367 \bibliography{defs,barrelfish}
368
369 \end{document}