Technote: Clean up
[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{\ccode}{\lstinline[language=C]}
67
68 \lstset{
69   language=C,
70   basicstyle=\ttfamily \small,
71   keywordstyle=\bfseries,
72   flexiblecolumns=false,
73   basewidth={0.5em,0.45em},
74   boxpos=t,
75   captionpos=b
76 }
77
78
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
80 \chapter{Introduction and usage}
81 \label{chap:introduction}
82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
83
84 \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. 
85 Source: \href{https://en.wikipedia.org/wiki/Sockeye_salmon}{Wikipedia}}
86 is a domain specific language to describe SoCs (Systems on a Chip).
87 It is an implementation of the language introduced in \cite{achermann:mars17} but adds some features to address issues encountered in practise.
88
89 The Sockeye compiler is written in Haskell using the Parsec parsing library. It
90 generates Prolog files from the Sockeye files. These Prolog files contain facts that represent a decoding net as defined in \cite{achermann:mars17}.
91 The Prolog files can then be loaded into Barrelfish's System Knowledgebase (SKB).
92
93 The source code for Sockeye can be found in \texttt{SOURCE/tools/sockeye}.
94
95
96 \section{Command line options}
97 \label{sec:cmdline}
98
99 \begin{verbatim}
100 $ sockeye [options] file
101 \end{verbatim}
102
103
104 The available options are:
105 \begin{description}
106         \item[-P] Generate a Prolog file that can be loaded into the SKB.
107         \item[-C] Just perform checks, do not compile.
108   \item[-o] \textit{filename} The path to the output file (including the file extension)
109   \item[-h] show usage information
110 \end{description}
111
112 The backend (capital letter options) specified last takes precedence.
113
114 The Sockeye file to compile is give via the \textit{file} parameter. The typical file extension for Sockeye files is \verb|.soc|.
115
116
117 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
118 \chapter{Lexical Conventions}
119 \label{chap:lexer}
120 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
121
122 The Sockeye parser follows a similar convention as opted by modern day 
123 programming languages like C and Java. Hence, Sockeye uses a Java-style-like
124 parser based on the Haskell Parsec Library. The following conventions are used:
125
126 \begin{description}
127 \item[Encoding] The file should be encoded using plain text.
128 \item[Whitespace:]  As in C and Java, Sockeye considers sequences of
129   space, newline, tab, and carriage return characters to be
130   whitespace.  Whitespace is generally not significant. 
131
132 \item[Comments:] Sockeye supports C-style comments.  Single line comments
133   start with \texttt{//} and continue until the end of the line.
134   Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
135   anything inbetween is ignored and treated as white space.
136
137 \item[Identifiers:] Valid Sockeye identifiers are sequences of numbers
138   (0-9), letters (a-z, A-Z), the underscore character ``\texttt{\_}'' and hyphens ``\texttt{-}''. They
139   must start with a letter.
140   \begin{align*}
141   identifier & \rightarrow letter (letter \mid digit \mid \_ \mid -)^{\textrm{*}} \\
142   letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
143   digit & \rightarrow (\textsf{0 \ldots 9})
144         \end{align*}
145   
146 \item[Integer Literals:] A Sockeye integer literal is a sequence of
147   digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
148   literals have no specifier and hexadecimal literals start with
149   \texttt{0x}. Octal literals start with \texttt{0o}.
150
151 \begin{align*}
152 decimal & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
153 hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
154 octal & \rightarrow (\textsf{0o})(\textsf{0 \ldots 7})^{\textrm{1}}\\
155 \end{align*}
156
157 \item[Reserved words:] The following are reserved words in Sockeye:
158 \begin{verbatim}
159 is, are, accept, map, over, to, at
160 \end{verbatim}
161
162 \end{description}
163
164
165 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
166 \chapter{Decoding Net Declaration}
167 \label{chap:declaration}
168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
169
170 In this chapter we define the layout of a Sockeye file. Each Sockeye file contains the declaration of a single decoding net.
171 An SoC can be split into multiple decoding nets e.g. one for the address spaces and another one for the interrupt routes.
172 However a node in a decoding net can not reference a node in a different decoding net.
173
174 \section{Syntax}
175
176 \subsection{Syntax Specification}
177 We use EBNF to specify the Sockeye syntax. Terminals are \textbf{bold}.
178 The non-terminals \textit{iden}, \textit{integer} and \textit{decimal} correspond to the identifiers, integer literals and decimal literals from Chapter~\ref{chap:lexer}.
179
180 \subsection{Net specification}
181 A net consists of one or more node declarations.
182 A node declaration contains one or more identifiers and the node specification.
183 The order in which the nodes are declared does not matter.
184
185 \begin{align*}
186 \textit{net}_s & \mathop{=}
187         \Big\{
188                 \textit{iden}\ \textbf{is}\ \textit{node}_s\
189         \Big|\
190                 \bigl\{ \textit{iden}\bigr\}\ \textbf{are}\ \textit{node}_s
191         \Big\} \\
192 \end{align*}
193
194 \subsection{Node specifications}
195 A node specification consists of a type, a set of accepted addresses, a set of translated addresses and an overlay.
196 All of these are optional.
197
198 \begin{align*}
199 \textit{node}_s & \mathop{=}
200         \Big[
201                 \textit{type}
202         \Big]\  
203         \Big[
204                 \textbf{accept [}\ \big\{\textit{block}_s\big\}\ \textbf{]}\ 
205         \Big]\ 
206         \Big[
207                 \textbf{map [}\ \big\{\textit{map}_s\big\}\ \textbf{]}\ 
208         \Big]\ 
209         \Big[
210                 \textbf{over}\ \textit{iden}
211         \Big] \\
212 \end{align*}
213
214 \subsection{Node type}
215 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.
216 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.
217
218 \begin{align*}
219 \textit{type} & \mathop{=}
220         \textbf{device}\
221         |\
222         \textbf{memory} \\
223 \end{align*}
224
225 \subsection{Addresses}
226 Addresses can be given as hexadecimal, octal or decimal integers.
227 \begin{align*}
228 \textit{addr} & \mathop{=} \textit{integer} \\
229 \end{align*}
230
231 \subsection{Block specification}
232 A block is specified by its start and end address.
233 If the start and end address are the same, the end address can be omitted.
234 Sockeye also supports specifying a block as its base address and the number of address bits the block spans:
235 A block from \texttt{0x0} to \texttt{0xFFF} with a size of 4kB can be specified ass \verb|0x0/12|.
236
237 \begin{align*}
238 \textit{block}_s & \mathop{=} \textit{addr}\
239         \Big[
240                 \textbf{-}\ \textit{addr}\ 
241         \Big|\
242                 \textbf{/}decimal
243         \Big] \\
244 \end{align*}
245
246 \subsection{Map specification}
247 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.
248 Multiple translation targets can be specified by giving a comma-separated list of targets.
249
250 \begin{align*}
251 \textit{map}_s & \mathop{=}
252 \textit{block}_s\ \textbf{to}\ \textit{iden}\ 
253         \Big[
254                 \textbf{at}\ \textit{addr}
255         \Big]\
256         \Big\{
257                 \textbf{,}\ \textit{iden}\ 
258                 \Big[
259                         \textbf{at}\ \textit{addr}
260                 \Big]
261         \Big\} \\
262 \end{align*}
263
264 \section{Conventions}
265 \todo{Specify conventions}
266
267
268 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
269 \chapter{Checks on the AST}
270 \label{chap:checks}
271 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
272 The Sockeye compiler performs some sanity checks on the parsed AST.
273
274 \section{No Duplicate Identifiers}
275 This check makes sure that there aren't two node declarations with the same identifier.
276
277 \section{No References to Undefined Nodes}
278 This check makes sure that all nodes referenced in translation sets and overlays are declared in the same file.
279
280
281 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
282 \chapter{Prolog Mapping for Sockeye}
283 \label{chap:prolog}
284 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
285 \todo{Describe Prolog fact layout}
286
287
288 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
289 \chapter{Integration into the Hake Build System}
290 \label{chap:hake}
291 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
292 \todo{Describe integration into Hake}
293
294
295 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
296 \bibliographystyle{abbrv}
297 \bibliography{barrelfish}
298
299 \end{document}