TN-020: adding motivational usescases fo Skate
[barrelfish] / doc / 020-skate / Skate.tex
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 % Copyright (c) 2015, 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{Skate in Barrelfish}
28 \author{Barrelfish project}
29 % \date{\today}   % Uncomment (if needed) - date is automatic
30 \tnnumber{020}
31 \tnkey{Skate}
32
33
34 \lstdefinelanguage{skate}{
35     morekeywords={schema,typedef,fact,enum},
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}{16.11.2015}{MH}{Initial Version}
49 \vhEntry{0.2}{20.04.2017}{RA}{Renaming ot Skate and expanding.}
50 \end{versionhistory}
51
52 % \intro{Abstract}    % Insert abstract here
53 % \intro{Acknowledgements}  % Uncomment (if needed) for acknowledgements
54 \tableofcontents    % Uncomment (if needed) for final draft
55 % \listoffigures    % Uncomment (if needed) for final draft
56 % \listoftables     % Uncomment (if needed) for final draft
57 \cleardoublepage
58 \setcounter{secnumdepth}{2}
59
60 \newcommand{\fnname}[1]{\textit{\texttt{#1}}}%
61 \newcommand{\datatype}[1]{\textit{\texttt{#1}}}%
62 \newcommand{\varname}[1]{\texttt{#1}}%
63 \newcommand{\keywname}[1]{\textbf{\texttt{#1}}}%
64 \newcommand{\pathname}[1]{\texttt{#1}}%
65 \newcommand{\tabindent}{\hspace*{3ex}}%
66 \newcommand{\Skate}{\lstinline[language=skate]}
67 \newcommand{\ccode}{\lstinline[language=C]}
68
69 \lstset{
70   language=C,
71   basicstyle=\ttfamily \small,
72   keywordstyle=\bfseries,
73   flexiblecolumns=false,
74   basewidth={0.5em,0.45em},
75   boxpos=t,
76   captionpos=b
77 }
78
79
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 \chapter{Introduction and usage}
82 \label{chap:introduction}
83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
84
85 \emph{Skate}\footnote{Skates are cartilaginous fish belonging to the family 
86 Rajidae in the superorder Batoidea of rays. More than 200 species have been 
87 described, in 32 genera. The two subfamilies are Rajinae (hardnose skates) and 
88 Arhynchobatinae (softnose skates). 
89 Source: \href{https://en.wikipedia.org/wiki/Skate_(fish)}{Wikipedia}}
90 is a domain specific language to describe the schema of 
91 Barrelfish's System Knowledge Base (SKB)~\cite{skb}. The SKB stores all 
92 statically or dynamically discovered facts about the system. Static facts are 
93 known and exist already at compile time of the SKB ramdisk or are added through
94 an initialization script or program. 
95
96 Examples for static facts include the device database, that associates known 
97 drivers with devices or the devices of a wellknown SoC. Dynamic facts, on the 
98 otherhand, are added to the SKB during and based on hardware discovery. 
99 Examples for dynamic facts include the number of processors or PCI Express 
100 devices. 
101
102 Inside the SKB, a prolog based constraint solver takes the added facts and 
103 computes a solution for hardware configuration such as PCI bridge programming,
104 NUMA information for memory allocation or device driver lookup. Programs can 
105 query the SKB using Prolog statements and obtain device configuration and PCI 
106 bridge programming, interrupt routing and constructing routing trees for IPC. 
107 Applications can use information to determine hardware characteristics such as 
108 cores, nodes, caches and memory as well as their affinity.
109
110
111 The Skate language is used to define format of those facts. The DSL is then 
112 compiled into a set of fact definitions and functions that are wrappers arround
113 the SKB client functions, in particular \texttt{skb\_add\_fact()}, to ensure
114 the correct format of the added facts.  
115
116 The intention when designing Skate is that the contents of system descriptor
117 tables such as ACPI, hardware information obtained by CPUID or PCI discovery
118 can be extracted from the respective manuals and easily specified in a Skate 
119 file. 
120
121 Skate complements the SKB by defining a \emph{schema} of the data stored in
122 the SKB. A schema defines facts and their structure, which is similar to Prolog
123 facts and their arity. A code-generation tool generates a C-API to populate the
124 SKB according to a specific schema instance.
125
126 The Skate compiler is written in Haskell using the Parsec parsing library. It
127 generates C header files from the Skate files. In addition it supports the 
128 generation of Schema documentation.
129
130 The source code for Skate can be found in \texttt{SOURCE/tools/skate}.
131
132
133 \section{Use cases}
134
135 We envision the following non exhausting list of possible use cases for Skate:
136
137 \begin{itemize}
138     \item A programmer is writing PCI discovery code or a device driver. The
139     program inserts various facts about the discovered devices and the state
140     of them into the SKB. To make the inserted facts usable to other programs
141     running on the system, the format of the facts have to be known. For this 
142     purpose we need a common to specify the format of those facts and their 
143     meaning.
144     
145     \item Each program needs to ultimately deal with the issue of actually 
146     inserting the facts into the SKB or query them. For this purpose, the fact 
147     strings need to be formatted accordingly, and this may be done differently 
148     for various languages and is error prone to typos. Skate is intended to 
149     remove the burden from the programmer by providing a language native (e.g. 
150     C or Rust) to ensure a safe way of inserting facts into the SKB. 
151     
152     \item Just knowing the format and the existence of certain facts is 
153     useless. A programmer needs to understand the meaning of them and their 
154     fields. It's not enough just to list the facts with the fields. Skate 
155     provides a way to generate a documentation about the specified facts. This 
156     enables programmers to reason about which facts should be used in 
157     particular selecting the right level of abstraction. This is important 
158     given that facts entered into the SKB from hardware discovery are 
159     intentionally as un-abstracted as possible.
160     
161     \item Documenting the available inference rules that the SKB implements
162     to abstract facts into useful concepts for the OS. 
163 \end{itemize}
164
165
166
167
168 \section{Command line options}
169 \label{sec:cmdline}
170
171 \begin{verbatim}
172 $ skate <options> INFILE.skt
173 \end{verbatim}
174
175
176 Where options is one of
177 \begin{description}
178   \item[-o] \textit{filename} The output file name
179   \item[-L] generate latex documentation
180   \item[-H] generate headerfile
181   \item[-W] generate Wiki syntax documentation
182 \end{description}
183
184
185
186 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
187 \chapter{Lexical Conventions}
188 \label{chap:lexer}
189 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
190
191 The Skate parser follows a similar convention as opted by modern day 
192 programming languages like C and Java. Hence, Skate uses a java-style-like
193 parser based on the Haskell Parsec Library. The following conventions are used:
194
195 \begin{description}
196 \item[Encoding] The file should be encoded using plain text.
197 \item[Whitespace:]  As in C and Java, Skate considers sequences of
198   space, newline, tab, and carriage return characters to be
199   whitespace.  Whitespace is generally not significant. 
200
201 \item[Comments:] Skate supports C-style comments.  Single line comments
202   start with \texttt{//} and continue until the end of the line.
203   Multiline comments are enclosed between \texttt{/*} and \texttt{*/};
204   anything inbetween is ignored and treated as white space.
205
206 \item[Identifiers:] Valid Skate identifiers are sequences of numbers
207   (0-9), letters (a-z, A-Z) and the underscore character ``\texttt{\_}''.  They
208   must start with a letter or ``\texttt{\_}''.  
209   \begin{align*}
210     identifier & \rightarrow ( letter \mid \_ ) (letter \mid digit \mid \_)^{\textrm{*}} \\
211     letter & \rightarrow (\textsf{A \ldots Z} \mid  \textsf{a \ldots z})\\
212     digit & \rightarrow (\textsf{0 \ldots 9})
213 \end{align*}
214
215   Note that a single underscore ``\texttt{\_}'' by itself is a special,
216   ``don't care'' or anonymous identifier which is treated differently
217   inside the language. 
218   
219 \item[Integer Literals:] A Skate integer literal is a sequence of
220   digits, optionally preceded by a radix specifier.  As in C, decimal (base 10)
221   literals have no specifier and hexadecimal literals start with
222   \texttt{0x}.  Binary literals start with \texttt{0b}. 
223
224   In addition, as a special case the string \texttt{1s} can be used to
225   indicate an integer which is composed entirely of binary 1's. 
226
227 \begin{align*}
228 digit & \rightarrow (\textsf{0 \ldots 9})^{\textrm{1}}\\
229 hexadecimal & \rightarrow (\textsf{0x})(\textsf{0 \ldots 9} \mid \textsf{A \ldots F} \mid \textsf{a \ldots f})^{\textrm{1}}\\
230 binary & \rightarrow (\textsf{0b})(\textsf{0, 1})^{\textrm{1}}\\
231 \end{align*}
232
233 \item[String Literals] String literals are enclosed in double quotes and should 
234   not span multiple lines.
235
236
237 \item[Reserved words:] The following are reserved words in Skate:
238 \begin{verbatim}
239 schema, fact, flags, constants, enumeration, text, section
240 \end{verbatim}
241
242
243 \item[Special characters:] The following characters are used as operators,
244   separators, terminators or other special purposes in Skate:
245 \begin{alltt}
246
247   \{ \} [ ] ( ) + - * / ; , . = 
248
249 \end{alltt}
250
251 \end{description}
252
253
254
255 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
256 \chapter{Schema Declaration}
257 \label{chap:declaration}
258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
259
260 In this chapter we define the layout of a Skate schema file, which declarations 
261 it must contain and what other declarations it can have. Each Skate schema file
262 defines exactly one schema, which may refer to other schemas.
263
264 \section{Syntax Highlights}
265 In the following sections we use the syntax highlighting as follows:
266 \begin{syntax}
267 \synbf{bold}:      Keywords  
268 \synit{italic}:      Identifiers / strings chosen by the user
269 \verb+verbatim+   constructs, symbols etc
270 \end{syntax}
271
272
273
274 \section{Conventions}
275 There are a some conventions that should be followed when writing a schema 
276 declaration. Following the conventions ensures consistency among different
277 schemas and allows generating a readable and well structured documentation.
278
279 \begin{description}
280     \item[Identifiers] Either camelcase or underscore can be used to separate 
281     words. Identifiers must be unique i.e. their fully qualified identifier must
282     be unique. A fully qualified identifier can be constructed as 
283     $schema.(namespace.)*name.$
284     \item[Descriptions] The description fields of the declarations should be 
285     used as a more human readable representation of the identifier. No use of
286     abbreviations or  
287     \item[Hierarchy/Grouping] Declarations of the same concept should be grouped
288     in a schema file (e.g. a single ACPI table). The declarations may be 
289     grouped further using namespaces (e.g. IO or local interrupt controllers)
290     \item[Sections/Text] Additional information can be provided using text 
291     blocks and sections. Each declaration can be wrapped in a section. 
292 \end{description}
293
294 \todo{which conventions do we actually want}
295
296 \section{The Skate File}
297 A Skate file must consist of zero or more \emph{import} declarations (see
298 Section~\ref{sec:decl:schema}) followed by a single \emph{schema} declaration 
299 (see Section~\ref{sec:decl:schema}) which contains the actual definitions. The 
300 Skate file typically has the extension \emph{*.sks}, referring to a Skate (or 
301 SKB) schema.
302
303 \begin{syntax}
304 /* Header comments */
305 (\synbf{import} schema)*
306
307 /* the actual schema declaration */
308 \synbf{schema} theschema "" \verb+{+...\verb+}+
309 \end{syntax}
310
311 Note that all imports must be stated at the beginning of the file. Comments can
312 be inserted at any place.
313
314 %\begin{align*}
315 %    skatefile & \rightarrow ( Import )^{\textrm{*}} (Schema)
316 %\end{align*}
317
318 \section{Imports}\label{sec:decl:import}
319 An import statement makes the definitions in a different schema file
320 available in the current schema definition, as described below.  The
321 syntax of an import declaration is as follows:
322
323 \paragraph{Syntax}
324
325 \begin{syntax}
326 \synbf{import} \synit{schema};
327 \end{syntax}
328
329 \paragraph{Fields}
330
331 \begin{description}
332 \item[schema] is the name of the schema to import definitions from.  
333 \end{description}
334
335 The order of the imports does not matter to skate. At compile time, the Skate 
336 compiler will try to resolve the imports by searching the include paths and the 
337 path of the current schema file for an appropriate schema file. Imported files 
338 are parsed at the same time as the main schema file. The Skate compiler will 
339 attempt to parse all the imports of the imported files transitively. Cyclic 
340 dependencies between device files will not cause errors, but at present are 
341 unlikely to result in C header files which will successfully compile. 
342
343 \section{Types}\label{sec:decl:types}
344
345 The Skate type system consists of a set of built in types and a set of implicit 
346 type definitions based on the declarations of the schema. Skate performs some
347 checks on the use of types.
348
349 \subsection{BuiltIn Types}
350
351 Skate supports the common C-like types such as integers, floats, chars as well 
352 as boolean values and Strings (character arrays). In addition, Skate treats
353 the Barrelfish capability reference (\texttt{struct capref}) as a built in 
354 type.
355
356 \begin{syntax}
357     UInt8, UInt16, UInt32, UInt64, UIntPtr
358     Int8, Int16, Int32, Int64, IntPtr
359     Float, Double
360     Char, String
361     Bool
362     Capref
363 \end{syntax}
364
365
366 \subsection{Declaring Types}
367 All declarations stated in Section~\ref{sec:decl:decls} are implicitly types 
368 and can be used within the fact declarations. This can restrict the values
369 that are valid in a field. The syntax of the declarations enforces certain
370 restrictions on which types can be used in the given context. 
371
372 In particular, fact declarations allow fields to be of type fact which allows 
373 a notion of inheritance and common abstractions. For example, PCI devices and
374 USB devices may implement a specialization of the device abstraction. Note, 
375 cicular dependencies must be avoided.
376
377 Defining type aliases using a a C-Like typedef is currently not supported.
378
379 \section{Schema}\label{sec:decl:schema}
380
381 A schema groups all the facts of a particular topic together. For example, 
382 a schema could be the PCI Express devices, memory regions or an ACPI table. 
383 Each schema must have a unique name, which must match the name of the file, and
384 it must have at least one declaration to be considered a valid file. All checks
385 that are being executed by Skate are stated in Chapter~\ref{chap:astops}.
386 There can only be one schema declaration in a single Schema file.
387
388 \paragraph{Syntax}
389
390 \begin{syntax}
391 \synbf{schema} \synit{name} "\synit{description}" \verb+{+
392   \synit{declaration};
393   \ldots
394 \verb+}+;
395 \end{syntax}
396
397 \paragraph{Fields}
398
399 \begin{description}
400 \item[name] is an identifier for the Schema type, and will be used to
401   generate identifiers in the target language (typically C).  
402   The name of the schema \emph{must} correspond to the
403   filename of the file, including case sensitivity: for example, 
404   the file \texttt{cpuid.sks} will define a schema type
405   of name \texttt{cpuid}. 
406
407 \item [description] is a string literal in double quotes, which
408   describes the schema type being specified, for example \texttt{"CPUID 
409   Information Schema"}. 
410
411 \item [declaration] must contain at least one of the following declarations:
412     \begin{itemize}
413         \item namespace -- Section \ref{sec:decl:namespace}
414         \item flags -- Section \ref{sec:decl:flags}
415         \item constants -- Section \ref{sec:decl:constants}
416         \item enumeration -- Section \ref{sec:decl:enums}
417         \item facts -- Section \ref{sec:decl:facts}
418         \item section -- Section \ref{sec:doc:section}
419         \item text -- Section \ref{sec:doc:text}
420     \end{itemize}
421
422 \end{description}
423
424
425
426 \section{Namespaces}
427 \label{sec:decl:namespace}
428
429 The idea of a namespaces is to provide more hierarchical structure similar to 
430 Java packages or URIs (schema.namespace.namespace) For example, a PCI devices 
431 may have virtual and physical functions or a processor has multiple cores. 
432 Namespaces can be nested within a schema to build a deeper hierarchy. 
433 Namespaces will have an effect on the code generation.
434
435 \todo{does everything has to live in a namespace?, or is there an implicit
436 default namespace?}
437
438 \paragraph{Syntax}
439
440 \begin{syntax}
441 \synbf{namespace} \synit{name} "\synit{description}" \verb+{+
442     \synit{declaration};
443     \ldots
444 \verb+}+;
445 \end{syntax}
446
447 \paragraph{Fields}
448
449 \begin{description}
450     \item[name] the identifier of this namespace.
451     
452     \item[description] human readable description of this namespace
453     
454     \item[declarations] One or more declarations that are valid a schema 
455     definition.
456 \end{description}
457
458
459
460 \section{Declarations}\label{sec:decl:decls}
461
462 In this section we define the syntax for the possible fact, constant, flags
463 and enumeration declarations in Skate. Each of the following declarations will
464 define a type and can be used.
465
466 \subsection{Flags}
467 \label{sec:decl:flags}
468
469 Flags are bit fields of a fixed size (8, 16, 32, 64 bits) where each bit 
470 position has a specific meaning e.g. the CPU is enabled or an interrupt
471 is edge-triggered. 
472
473 In contrast to constants and enumerations, the bit positions of the flags have 
474 a particular meaning and two flags can be combined effectively enabling both
475 options whereas the combination of enumeration values or constants may not be 
476 defined. Bit positions that are not defined in the flag group are treated as 
477 zero.
478
479 As an example of where to use the flags use case we take the GICC CPU Interface 
480 flags as defined in the MADT Table of the ACPI specification.
481
482
483 \begin{tabular}{lll}
484     \textbf{Flag}      & \textbf{Bit} & \textbf{Description} \\
485     \hline
486     Enabled   & 0   & If zero, this processor is unusable.\\
487     Performance Interrupt Mode & 1 &  0 - Level-triggered,\\
488     VGIC Maintenance Interrupt Mode & 2 & 0 - Level-triggered, 1 - 
489     Edge-Triggered \\
490     Reserved & 3..31 & Reserved \\
491     \hline
492 \end{tabular}
493
494
495
496 \subsubsection{Syntax}
497
498 \begin{syntax}
499 \synbf{flags} \synit{name} \synit{width} "\synit{description}" \verb+{+
500     \synit{position1} \synit{name1} "\synit{description1}" ;
501     \ldots
502 \verb+}+;
503 \end{syntax}
504
505 \subsubsection{Fields}
506
507 \begin{description}
508     \item[name] the identifier of this flag group. Must be unique for all 
509                 declarations.
510     
511     \item [width] The width in bits of this flag group. Defines the maximum 
512                   number of flags supported. This is one of 8, 16, 32, 64.
513     
514     \item [description] description in double quotes is a short explanation of
515                         what the flag group represents.
516     
517     \item [name1] identifier of the flag. Must be unique within the flag 
518                   group. 
519     
520     \item [position1] integer defining which bit position the flag sets
521     
522     \item [description1] description of this particular flag.
523 \end{description}
524
525 \subsubsection{Type}
526 Flags with identifier $name$ define the following type:
527 \begin{syntax}
528 \synbf{flag} \synit{name};
529 \end{syntax}
530
531 \subsubsection{Example}
532
533 The example from the ACPI table can be expressed in Skate as follows:
534
535 \begin{syntax}
536 \synbf{flags} CPUInterfaceFlags \synit{32} "\synit{GICC CPU Interface Flags}"\
537 \verb+{+
538     0 Enabled         "\synit{The CPU is enabled and can be used}" ;
539     1 Performance     "\synit{Performance Interrupt Mode Edge-Triggered }" ;
540     1 VGICMaintenance "\synit{VGIC Maintenance Interrupt Mode Edge-Triggered}" ;
541 \verb+}+;
542 \end{syntax}
543
544
545 \subsection{Constants}
546 \label{sec:decl:constants}
547
548 Constants provide a way to specify a set of predefined values of a particular 
549 type. They are defined in a constant group and every constant of this group
550 needs to be of the same type.
551
552 Compared to flags, the combination of two constants has no meaning (e.g.
553 adding two version numbers). In addition, constants only define a set of known 
554 values, but do not rule out the possibility of observing other values. As an 
555 example for this may be the vendor ID of a PCI Expess device, where the 
556 constant group contains the known vendor IDs.
557
558 As an example where constants ca be used we take the GIC version field of the
559 GICD entry of the ACPI MADT Table.
560
561 \begin{tabular}{ll}
562     \textbf{Value} & \textbf{Meaning} \\
563     \hline
564     \texttt{0x00} & No GIC version is specified, fall back to hardware 
565     discovery for GIC version \\
566     \texttt{0x01} & Controller is a GICv1 \\
567     \texttt{0x02} & Controller is a GICv2 \\
568     \texttt{0x03} & Controller is a GICv3 \\
569     \texttt{0x04} & Controller is a GICv4 \\
570     \texttt{0x05-0xFF} & Reserved for future use. \\
571     \hline
572 \end{tabular}
573
574 \subsubsection{Syntax}
575
576 \begin{syntax}
577 \synbf{constants} \synit{name} \synit{builtintype} "\synit{description}" \verb+{+
578     \synit{name1} = \synit{value1} "\synit{description1}" ;
579     \ldots
580 \verb+}+;
581 \end{syntax}
582
583 \subsubsection{Fields}
584
585 \begin{description}
586     \item[name] the identifier of this constants group. Must be unique for all 
587                 declarations.
588     
589     \item [builtintype] the type of the constant group. Must be one of the 
590                         builtin types as defined in~\ref{sec:decl:types}
591     
592     \item [description] description in double quotes is a short explanation of
593                         what the constant group represents.
594     
595     \item [name1] identifier of the constant. Must be unique within the 
596                   constant group. 
597     
598     \item [value1] the value of the constant. Must match the declared type.
599     
600     \item [description1] description of this particular constant
601     
602 \end{description}
603
604 \subsubsection{Type}
605 Constants with identifier $name$ define the following type:
606 \begin{syntax}
607 \synbf{constant} \synit{name};
608 \end{syntax}
609
610
611 \subsubsection{Example}
612 The GIC version of our example can be expressed in the syntax as follows: 
613
614 \begin{syntax}
615 \synbf{constants} GICVersion \synit{uint8} "\synit{The GIC Version}" \verb+{+
616     unspecified = 0x00 "\synit{No GIC version is specified}" ;    
617     GICv1       = 0x01 "\synit{Controller is a GICv1}" ;
618     GICv2       = 0x02 "\synit{Controller is a GICv2}" ;
619     GICv3       = 0x03 "\synit{Controller is a GICv3}" ;
620     GICv4       = 0x04 "\synit{Controller is a GICv4}" ;
621 \verb+}+;
622 \end{syntax}
623
624 \subsection{Enumerations}
625 \label{sec:decl:enums}
626
627 Enumerations model a finite set of states effectively constants that only allow
628 the specified values. However, in contrast to constants they are not assigned
629 an specific value. Two enumeration values cannot be combined. As an example, 
630 the enumeration construct can be used to express the state of a device in the
631 system which can be in one of the following states: \emph{uninitialized, 
632 operational, suspended, halted.} It's obvious, that the combination of the 
633 states operational
634 and suspended is meaning less.
635
636
637 \subsubsection{Syntax}
638
639 \begin{syntax}
640 \synbf{enumeration} \synit{name} "\synit{description}" \verb+{+
641     \synit{name1} "\synit{description1}";
642     \ldots
643 \verb+}+;
644 \end{syntax}
645
646 \subsubsection{Fields}
647
648 \begin{description}
649     \item[name] the identifier of this enumeration group. Must be unique for 
650                 all declarations.
651     
652     \item [description] description in double quotes is a short explanation of
653                         what the enumeration group represents.
654     
655     \item [name1] identifier of the element. Must be unique within the 
656                   enumeration group.   
657     
658     \item [description1] description of this particular element
659     
660 \end{description}
661
662 \subsubsection{Type}
663 Enumerations with identifier $name$ define the following type:
664 \begin{syntax}
665 \synbf{enum} \synit{name};
666 \end{syntax}
667
668 \subsubsection{Example}
669 \begin{syntax}
670 \synbf{enumeration} DeviceState "\synit{Possible device states}" \verb+{+
671     uninitialized "\synit{The device is uninitialized}";
672     operational   "\synit{The device is operaetional}";
673     suspended     "\synit{The device is suspended}";
674     halted        "\synit{The device is halted}";
675 \verb+}+;
676 \end{syntax}
677
678 \subsection{Facts}
679 \label{sec:decl:facts}
680
681 The fact is the central element of Skate. It defines the actual facts about the
682 system that are put into the SKB. Each fact has a name and one or more fields
683 of a given type. Facts should be defined such that they do not require any 
684 transformation. For example, take the entries of an ACPI table and define a
685 fact for each of the entry types. 
686
687 \subsubsection{Syntax}
688
689 \begin{syntax}
690 \synbf{fact} \synit{name}  "\synit{description}" \verb+{+
691     \synit{type1} \synit{name1} "\synit{description1}" ;
692     \ldots
693 \verb+}+;
694 \end{syntax}
695
696 \subsubsection{Fields}
697
698 \begin{description}
699     \item[name] the identifier of this fact. Must be unique for all 
700                 declarations.
701     
702     \item[description] description in double quotes is a short English          
703                        explanation of what the fact defines. (e.g. Local APIC)
704     
705     \item[type1] the type of the fact field. Must be one of the BuiltIn types
706                  or one of the constants, flags or other facts. When using 
707                  facts as field types, there must be no recursive nesting.
708
709     \item [name1] identifier of a fact field. Must be unique within the 
710                   Fact group.   
711     
712     \item [description1] description of this particular field
713 \end{description}
714
715 \subsubsection{Type}
716 Facts with identifier $name$ define the following type.
717
718 \begin{syntax}
719 \synbf{fact} \synit{name};
720 \end{syntax}
721
722
723 \section{Documentation}
724
725 The schema declaration may contain \emph{section} and \emph{text} blocks that
726 allow providing an introduction or additional information for the schema 
727 declared in the Skate file. The two constructs are for documentation purpose 
728 only and do not affect code generation. The section and text blocks can appear
729 at any place in the Schema declaration. There is no type being defined for 
730 documentation blocks.
731
732 \subsection{Schema}
733 The generated documentation will contain all the schemas declared in the source 
734 tree. The different schema files correspond to chapters in the resulting 
735 documentation or form a page of a Wiki for instance.
736
737 \subsection{Text}
738 \label{sec:doc:text}
739
740 By adding \texttt{text} blocks, additional content can be added to the generated
741 documentation. This includes examples and additional information of the
742 declarations of the schema. The text blocks are omitted when generating code. 
743 Note, each of the text lines must be wrapped in double quotes. Generally, a 
744 block of text will translate to a paragraph.
745
746 \subsubsection{Syntax}
747
748 \begin{syntax}
749 \synbf{text} \verb+{+
750     "\synit{text}"
751     ...
752 \verb+};+
753 \end{syntax}
754
755 \subsubsection{Fields}
756
757 \begin{description}
758     \item[text] A line of text in double quotes.
759 \end{description}
760
761 \subsection{Sections}
762 \label{sec:doc:section}
763 The \texttt{section} construct allows to insert section headings into the 
764 documentation. A section logically groups the declarations and text blocks 
765 together to allow expressing a logical hierarchy. 
766
767 \subsubsection{Syntax}
768
769 \begin{syntax}
770 \synbf{section} "\synit{name}"  \verb+{+
771     \synit{declaration};
772     \ldots
773 \verb+};+
774 \end{syntax}
775
776 \subsubsection{Fields}
777
778 \begin{description}
779     \item[name] the name will be used as the section heading
780     \item[declaration] declarations belonging to this section. 
781 \end{description}
782
783 Note, nested sections will result into (sub)subheadings or heading 2, 3, ...
784 Namespaces will appear as sections in the documentation.
785
786
787 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
788 \chapter{Operations and checks on the AST}
789 \label{chap:astops}
790 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
791
792 \section{Filename Check}
793
794 \section{Type Checks}
795
796 \section{Sorting of Declarations}
797
798
799 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
800 \chapter{C mapping for Schema Definitions}
801 \label{chap:cmapping}
802 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
803
804 For each schema specification, Skate generates ....
805
806 \paragraph{Abbrevations}
807 In all the sections of this chapter, we use the follwing abbrevations, where 
808 the actual value may be upper or lower case depending on the conventions:
809
810 \begin{description}
811   \item[SN] The schema name as used in the schema declaration.
812   \item[DN] The declaration name as used in the flags / constants / 
813             enumeration / facts declaration
814   \item[FN] The field name as used in field declaration of flags / constants / 
815             enumeration / facts
816 \end{description}
817
818 In general all defined functions, types and macros are prefixed with the schema
819 name SN.
820
821 \paragraph{Conventions}
822 We use the follwing conventions for the generated code:
823 \begin{itemize}
824   \item macro definitions and enumerations are uppercase.
825   \item type definitions, function names are lowercase.
826   \item use of the underscore \texttt{'\_'} to separate words
827 \end{itemize}
828
829 \todo{just a header file (cf mackerel), or also C functions (cf. flounder)?}
830
831 \section{Using Schemas}
832
833 Developers can use the schemas by including the generated header file of a 
834 schema. All header files are placed in the schema subdirectory of the main 
835 include folder of the build tree. For example, the 
836 schema \texttt{SN} would generate the file \texttt{SN\_schema.h} and can 
837 be included by a C program with:
838 \begin{quote}
839 \texttt{\#include <schema/SN\_schema.h}
840 \end{quote}
841
842 \section{Preamble}
843
844 The generated headerfile is protected by a include guard that depends on the
845 schema name. For example, the schema \texttt{SN} will be guarded by the
846 macro definition \texttt{\_\_SCHEMADEF\_\_SN\_H\_}. The header file will 
847 include the folling header files:
848 \begin{enumerate}
849   \item a common header \texttt{skate.h} providing the missing macro and 
850         function definitions for correct C generation.
851   \item an include for each of the imported schema devices.
852 \end{enumerate}
853
854 \section{Constants}
855
856 For any declared constant group, Skate will generate the following:
857
858 \paragraph{Type and macro definitions}
859 \begin{enumerate}
860   \item A type definition for the declared type of the constant group. The 
861         type  typename will be \texttt{SN\_DN\_t}.
862   \item A set of CPP macro definitions, one for each of the declared constants.
863         Each macro will have the name as in \texttt{SN\_DN\_FN} and expands to the field value cast to the type of the field.
864 \end{enumerate}
865
866 \paragraph{Function definitions}
867 \begin{enumerate}
868   \item A function to describe the value 
869         \begin{quote}
870           \texttt{SN\_DN\_describe(SN\_DN\_t);}
871         \end{quote}
872
873   \item An snprintf-like function to pretty-print values of type SN\_DN\_t, 
874         with prototype:
875         \begin{quote}
876           \texttt{int SN\_DN\_print(char *s, size\_t sz);}
877         \end{quote}
878
879 \end{enumerate}
880 \todo{Do we need more ?}
881
882 \section{Flags}
883
884 \paragraph{Type and macro definitions}
885 \begin{enumerate}
886   \item A type definition for the declared type of the flag group. The 
887         type typename will be \texttt{SN\_DN\_t}.
888 \end{enumerate}
889
890 \paragraph{Function definitions}
891 \begin{enumerate}
892   \item A function to describe the value 
893         \begin{quote}
894           \texttt{SN\_DN\_describe(SN\_DN\_t);}
895         \end{quote}
896 \end{enumerate}
897 \todo{Do we need more ?}
898
899 \section{Enumerations}
900 Enumerations translate one-to-one to the C enumeration type in a straight 
901 forward manner:
902
903 \begin{quote}
904   \texttt{typdef enum \{ SN\_DN\_FN1, ... \} SN\_DN\_t; }
905 \end{quote}
906
907 \paragraph{Function definitions}
908 \begin{enumerate}
909   \item A function to describe the value 
910         \begin{quote}
911           \texttt{SN\_DN\_describe(SN\_DN\_t);}
912         \end{quote}
913   \item A function to pretty-print the value
914         \begin{quote}
915           \texttt{SN\_DN\_print(char *b, size\_t sz, SN\_DN\_t val);}
916         \end{quote}
917 \end{enumerate}
918
919 \section{Facts}
920
921
922 \paragraph{Type and macro definitions}
923 \begin{enumerate}
924   \item A type definition for the declared type of the flag group. The 
925         type typename will be \texttt{SN\_DN\_t}.
926 \end{enumerate}
927
928 \paragraph{Function definitions}
929 \begin{enumerate}
930   \item A function to describe the value 
931         \begin{quote}
932           \texttt{SN\_DN\_describe(SN\_DN\_t);}
933         \end{quote}
934   \item A function to add a fact to the SKB
935   \item A function to retrieve all the facts of this type from the SKB
936   \item A function to delete the fact from the SKB
937 \end{enumerate}
938
939 \todo{Provide some way of wildcard values. e.g. list all facts with this 
940 filter or delete all facts that match the filter.}
941
942 \section{Namespaces}
943
944 \paragraph{Function definitions}
945 \begin{enumerate}
946     \item A function to retrieve all the facts belonging to a name space
947 \end{enumerate}
948
949
950 \section{Sections and text blocks}
951 For the \texttt{section} and \texttt{text} blocks in the schema file, there
952 won't be any visible C constructs generated, but rather turned into comment
953 blocks in the generated C files.
954
955
956
957
958 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
959 \chapter{Prolog mapping for Schema Definitions}
960 \label{chap:prologmapping}
961 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
962
963 Each fact added to the SKB using Skate is represented by a single Prolog
964 functor.  The functor name in Prolog consist of the schema and fact name.  The
965 fact defined in Listing \ref{lst:sample_schema} is represented by the functor
966 \lstinline!cpuid_vendor!~and has an arity of three.
967
968
969 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
970 \chapter{Generated Documentation}
971 \label{chap:documentation}
972 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
973
974
975 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
976 \chapter{Access Control}
977 \label{chap:accesscontrol}
978 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
979
980 on the level of schema or namespaces.
981
982
983 \chapter{Integration into the Hake build system}
984
985 Skate is a tool that is integrated with Hake. Add the attribute
986 \lstinline!SkateSchema!~to a Hakefile to invoke Skate as shown in Listing
987 \ref{lst:Skate_hake}.
988
989 \begin{lstlisting}[caption={Including Skate schemata in Hake},
990 label={lst:Skate_hake}, language=Haskell]
991 [ build application {
992     SkateSchema = [ "cpu" ]
993     ... 
994 } ]
995 \end{lstlisting}
996
997 Adding an entry for \varname{SkateSchema} to a Hakefile will generate both
998 header and implementation and adds it to the list of compiled resources. A
999 Skate schema is referred to by its name and Skate will look for a file
1000 ending with \varname{.Skate} containing the schema definition.
1001
1002 The header file is placed in \pathname{include/schema} in the build tree, the C
1003 implementation is stored in the Hakefile application or library directory.
1004
1005
1006
1007 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1008 \bibliographystyle{abbrv}
1009 \bibliography{barrelfish}
1010
1011 \end{document}