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