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