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