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