f5e26d44fa83d8370022d89cdc4c1c290c30ca0b
[barrelfish] / doc / 001-glossary / Main.hs
1 {- 
2    Glossary: a simple glossary generator for Barrelfish
3    
4   Copyright (c) 2010, ETH Zurich.
5   All rights reserved.
6   
7   This file is distributed under the terms in the attached LICENSE file.
8   If you do not find this file, copies can be found by writing to:
9   ETH Zurich D-INFK, Universitaetstr. 6, CH-8092 Zurich. Attn: Systems Group.
10 -}
11   
12 module Main where 
13
14 import System.Exit
15 import System.IO
16 import Text.Printf
17 import Data.List
18 import qualified Data.Char
19
20 data Entry = Entry {
21       entry_title :: String,
22       entry_aliases :: [ String ],
23       entry_description :: String
24 } deriving (Show,Eq)
25
26
27 glossary :: [ Entry ] 
28 glossary = [ Entry "dispatcher control block" [ "DCB" ] 
29              
30              "Data structure representing the dispatcher.  DCBs are \
31              \referred to by specially typed capabilities.",
32
33              Entry "CPU driver" [] 
34
35              "The code running on a core which executes in kernel or \
36              \privileged mode.  CPU drivers are the Barrelfish \
37              \equivalent of a kernel, except that there is one per \
38              \core, and they share no state or synchronization. CPU \
39              \drivers are typically non-preemptible, \
40              \single-threaded, and mostly stateless.",
41
42              Entry "Mackerel" [] 
43              
44              "The Domain Specific Language used in Barrelfish to specify \
45              \device hardware registers and hardware-defined in-memory \
46              \data structures.  The Mackerel compiler takes such a \
47              \description and outputs a \
48              \C header file containing inline functions to read and \
49              \write named bitfields for a device or data structure, \
50              \together with string formatting code to aid in \
51              \debugging.  Mackerel input files are found in the \
52              \\\texttt{/devices} directory of the source tree, and end \
53              \in \\texttt{.dev}.  Generated header files are found in \
54              \the \\texttt{/include/dev} subdirectory of the build \
55              \tree.",
56
57              Entry "interconnect driver" [ "ICD" ]
58
59              "A partial abstraction of low-level message passing \
60              \mechanism, such as a shared-memory buffer or hardware \
61              \message passing primitive.  ICDs do not present a uniform \
62              \interface, and therefore require specific stubs to be \
63              \generated by Flounder.  Similarly, they do not present \
64              \any particular semantics with regard to flow control, \
65              \polled or upcall-based delivery, etc.  A special case of \
66              \an ICD is the local message passing (LMP) mechanism, \
67              \which is implemented for every type of core and provide \
68              \communication between dispatchers running on that core.",
69
70              Entry "Flounder" []
71
72              "The Interface Definition Language used for \
73              \communication between domains in Barrelfish.  Flounder \
74              \supports message type signatures, various concrete type \
75              \constructors like structs and arrays, and also some \
76              \opaque types like capabilities and interface \
77              \references.  The Flounder compiler is written in \
78              \Haskell and generates code in C or THC.  Flounder \
79              \generates specialized code for each Interconnect Driver \
80              \in a system.",
81              
82              Entry "Hake" [ "Hakefile" ]
83
84              "The build system for Barrelfish.  The Barrelfish source \
85              \tree consists of a Hakefile in each relevant source \
86              \directory, which contains a single Haskell expression \
87              \specifying a list of targets to be built.  Hake itself \
88              \aggregates all these Hakefiles, and uses them to generate \
89              \a single Makefile in a separate, build directory.  This \
90              \Makefile contains an explicit target for \\emph{every} \
91              \file that can be built for Barrelfish for every \
92              \appropriate architecture.  A separate, manually-edited \
93              \Makefile contains convenient symbolic targets for \
94              \creating boot images, etc.  Since the contents of \
95              \Hakefiles are Haskell expressions, quite powerful \
96              \constructs can be used to specify how to build files for \
97              \different targets.",
98
99              Entry "Elver" [] 
100
101              "An intermediate boot loader for booting 64-bit \
102              \ELF images on Intel-architecture machines where the main \
103              \boot loader (such as Grub) does not support entering a \
104              \kernel in long mode.  Elver is specified as the first \
105              \module of the multiboot image, and puts the boot \
106              \processor into long mode before jumping to the CPU \ 
107              \driver, which is assumed to be in the second multiboot \
108              \module.",
109
110              Entry "Filet-o-Fish" [ "FoF" ]
111
112              "An embedding of C into Haskell, used for writing C code \
113              \generators for Haskell-based domain specific languages.  \
114              \Instead of using C syntax combinators (as used in \
115              \Flounder and Mackerel) FoF-based DSLs (such as Fugu and \
116              \Hamlet) use backend which are actually semantic \
117              \specifications of behavior, from which FoF can generates \
118              \C code which is guaranteed to implement the given \
119              \semantics.",
120
121              Entry "Fugu" [ "errno.h" ]
122
123              "A small domain-specific language (implemented using \
124              \Filet-o-Fish) to express error conditions and messages \
125              \for Barrelfish.  Fugu offloads the problem of tracking \
126              \error messages and code, and also implements a short \
127              \error ``stack'' in machine word to provide more detailed \ 
128              \error information.  Fugu generates the \\texttt{errno.h} \
129              \file.",
130
131              Entry "THC" []
132
133              "A dialect of C with extensions to support the \
134              \asynchronous message passing flavor of most Barrelfish \
135              \services by providing an \\texttt{async} construct and \
136              \continuations.  THC also integrates with specially generated \
137              \Flounder stubs.",
138
139              Entry "System Knowledge Base" [ "SKB" ]
140
141              "A repository for hardware-derived system information in \
142              \a running Barrelfish system.  The SKB is currently a port \
143              \of the ECLiPse Constraint Logic Programming system, and is \
144              \used for (among other things) PCI bridge programming, \
145              \interrupt routing, and constructing routing trees for \
146              \intra-machine multicast. The SKB runs as a system service \
147              \accessed by message passing.",
148
149              Entry "capability space" [ "cspace" ]
150
151              "The set of capabilities held by a dispatcher on a core \
152              \is organized in a guarded page table structure \
153              \implemented as a tree of CNodes, where internal nodes are \
154              \CNodes and leaf nodes are non-CNode capabilities.  This \
155              \allows any capability held by a dispatcher to be referred \
156              \to using a 32-bit address; when invoking a capability, \
157              \the CPU driver walks the cspace structure resolving a \
158              \variable number of bits of this address at each level. \
159              \This means that capabilities used frequently should be \
160              \stored near the top of the tree, preferably in the root \
161              \CNode.  Some CPU drivers allow a fast path where the \ 
162              \32-bit address is implicitly assumed to simply an offset \
163              \in the root CNode.  The capability for the root CNode can \
164              \be efficiently found from the DCB; note that, unlike the \
165              \vspace, the cspace is purely local to a core and cannot \
166              \be shared between dispatchers on difference cores.",
167              
168              Entry "vspace" []
169
170              "An object representing a virtual address space.  Unlike \
171              \a cspace, a vspace can under some circumstances be shared \
172              \between cores.  However, a vspace is tied to a particular \
173              \core architecture, and a particular physical address \
174              \space, though vspaces can be manipulated on other cores \
175              \and even cores of other architectures.  Mappings are \
176              \created in a vspace by specifying capabilities to regions \
177              \of memory that are mappable (such as frame \
178              \capabilities).",
179              
180              Entry "Aquarium" []
181
182              "A visualization tool for Barrelfish trace data. Aquarium \
183              \is written in C\\# and can accept data as a stream over \
184              \the network from a running Barrelfish machine, or from a \
185              \trace file.  It displays a time line showing which \
186              \dispatchers are running on which cores, messages between \
187              \dispatchers, and other system events.",
188
189              Entry "Hamlet" []
190
191              "The language used to specify all Barrelfish capability \
192              \types, together with their in-memory formats and \
193              \transformation rules when transferring a capability from \
194              \one core to another.  Hamlet is implemented using \
195              \Filet-o-Fish and generates capability dispatch code for \
196              \CPU drivers, among other things. \
197              \Surprisingly, Hamlet is a type of fish.",
198
199              Entry "Local Message Passing" [ "LMP" ] 
200
201              "Each Barrelfish CPU driver includes a special \
202              \Interconnect Driver for passing messages between \
203              \dispatchers on the same core, often based on the \
204              \concepts from LRPC and L4 IPC.  This is referred to as \
205              \LMP.",
206
207              Entry "dispatcher" []
208
209              "The data structure representing an application's \
210              \runnability on a core.  Dispatchers contain scheduling \
211              \state, message end points, and upcall entry points; they \
212              \are the nearest equivalent to processes in Unix. \
213              \Dispatchers are always tied to a core.  A Barrelfish \
214              \application can be viewed as a collection of dispatchers \
215              \spread across the set of cores on which the application \
216              \might run, together with associated other resources. \
217              \The term is from K42.",
218
219              Entry "monitor" []
220                    
221              "A privileged process running on a core which handles \
222              \most core OS functionality not provided by the CPU \
223              \driver.  Since CPU drivers do not directly communicate \
224              \with each other, the task of state coordination in \
225              \Barrelfish is mostly handled by Monitors.  Monitors are \
226              \also responsible for setting up inter-core communication \
227              \channels (``binding''), and transferring capabilities \
228              \between cores.  When a capability is retyped or revoked, \
229              \the monitors are responsible for ensuring that this \
230              \occurs consistently system-wide.  The monitor for a core \
231              \holds a special capability (the kernel capability) which \
232              \allows it to manipulate certain data structures in the \
233              \CPU driver, such as the capability database.",
234
235              Entry "User-level Message Passing" [ "UMP", "CC-UMP" ]
236
237              "A series of Interconnect Drivers which use \
238              \cache-coherent shared memory to send cache-line \
239              \sized frames between cores.  UMP is based on ideas \
240              \from URPC, and avoids kernel transitions on message \
241              \send and receive.  It is the preferred channel for \
242              \communication between cores on an Intel-architecture \
243              \PC, for example.  However, because it operates \
244              \entirely in user space, it cannot send capabilities \
245              \between cores.  Instead, the Flounder stubs for UMP \
246              \send capabilities via another channel through LMP to \
247              \the local monitor, which forwards them correctly to \
248              \the destination.",
249
250              Entry "capability" [ "cap" ]
251
252              "Barrelfish uses ``partitioned capabilities'' to refer to \
253              \most OS resources (most of which are actually typed areas \
254              \of memory).  Operations on such resources are typically \
255              \carried out ``invoking'' an operation on the capability \
256              \via a system call to the local CPU driver.  Capabilities \
257              \are fixed-size data structures which are held in areas of \
258              \memory called CNodes, and which cannot be directly read \
259              \from or written to by user mode programs.  Instead, users \
260              \move capabilities between CNodes by invoking operations \
261              \on the capability that refers to the CNode.  Capabilities \
262              \can be ``retyped'' and progressively refined from pure \
263              \memory capabilities to ones which can be mapped into an \
264              \address space, for example, or used as CNodes.  The set \
265              \of capability types understood by Barrelfish is defined \
266              \using the Hamlet language.",
267
268              Entry "physical address capability" [] 
269
270              "A capability referring to a raw region of physical \
271              \address space.  This is the most basic type of \
272              \capability; all other capability types which refer to \
273              \memory are ultimately subtypes of this.",
274
275              Entry "RAM capability" [] 
276
277              "A capability type which refers to a region of Random \
278              \Access Memory.  A direct subtype of a Physical Address \
279              \capability.",
280
281              Entry "device frame capability" []
282
283              "A capability type which refers to a region of physical \
284              \address space containing memory-mapped I/O registers. A \
285              \direct subtype of a Physical Address capability.",
286
287                                 
288              Entry "CNode capability" []
289
290              "A capability type referring to a CNode.",
291
292              Entry "foreign capability" []
293
294              "A capability referring to a resource which only makes \
295              \sense on a different core to the one it exists on.  For \
296              \example, since the cspace is purely local to core, \
297              \transferring a CNode capability to another core \
298              \transforms it into a Foreign CNode capability, whose only \
299              \operations are to remotely manipulate (principally copy \
300              \capabilities from) the original CNode.",
301
302              Entry "dispatcher capability" []
303
304              "A capability referring to the memory region occupied by \
305              \a Dispatcher Control Block.",
306
307              Entry "endpoint capability" []
308
309              "A capability referring to a (core-local) communication \
310              \endpoint.  Posession of such a capability enables the \
311              \holder to send a message to endpoint.",
312
313              Entry "frame capability" [] 
314
315              "A capability refering to a \
316              \set of page frames which can be mapped into a \
317              \virtual address space.  Frame capabilities are a \
318              \subtype of RAM capabilities; the latter cannot be \
319              \mapped.",
320
321              Entry "kernel capability" [] 
322
323              "A capability enabling the holder to manipulate CPU \
324              \driver data structures (in particular, the capability \
325              \database).  The kernel capability for a core is only held \
326              \by the core's monitor.",
327
328              Entry "vnode capability" []
329
330              "One of a set of capability types, one for each format of \
331              \page table page for each architecture supported by \
332              \Barrelfish.  For example, there are four Vnode capability \
333              \types for the x86-64 architecture, corresponding to the \
334              \PML4, PDPT, PDIR, and PTABLE pages in a page table.",
335
336              Entry "IO capability" []
337
338              "A capability enabling the holder to perform IO space \
339              \operations on Intel architecture machines.  Each IO \
340              \capability grants access to a range of IO space addresses \
341              \on a specific core.",
342              
343              Entry "capability node" [ "cnode" ]
344
345              "A region of RAM containing capabilities.  A CNode cannot \
346              \be mapped into a virtual address space, and so can only \
347              \be accessed by operations on the CNode capability which \
348              \refers to it -- this is how strict partitioning of \
349              \capability memory from normal memory is achieved.  The \
350              \set of CNodes which can be referenced by a single \
351              \dispatcher is called the cspace.",
352
353              Entry "scheduler manifest" []
354
355              "A description of the scheduling requirements of \
356              \multiprocessor application, used to inform the various \
357              \system schedulers about how best to dispatch the \
358              \application's threads.",
359
360              Entry "dite" []
361
362              "A tool used to build a boot image in the proprietary Intel \
363              \``32.obj'' format, for booting on the Single-chip Cloud \
364              \Computer.",
365  
366              Entry "Pleco" []
367
368              "The Domain Specific Language used in Barrelfish to specify \
369              \constants for the tracing infrastructure.  The Pleco \
370              \compiler takes such description and outputs a \
371              \C header file containing the definitions, a C source \
372              \file with the constants, and a JSON file to be used by \
373              \host visualization tools.",
374
375              Entry "ZZZ terms yet to be added" []
376
377              "cc-ump, init, Beehive, asmoffsets, retype, iref"
378
379            ]
380
381
382 compare_entry :: Entry -> Entry -> Ordering
383 compare_entry (Entry k1 _ _) (Entry k2 _ _) = 
384     compare (map Data.Char.toLower k1) (map Data.Char.toLower k2)
385
386 format_glossary :: [Entry] -> String
387 format_glossary gl = 
388     let full_gl = gl ++ (expand_aliases gl)
389         sort_gl = sortBy compare_entry full_gl
390     in unlines [ format_entry e | e <- sort_gl ]
391
392 format_entry :: Entry -> String
393 format_entry (Entry title aliases description) = 
394     printf "\\item[%s:] %s\n" (format_aliases title aliases) description
395
396 format_aliases :: String -> [String] -> String
397 format_aliases t [] = t
398 format_aliases t al = 
399     printf "%s \\textrm{\\textit{(%s)}}" t (concat $ intersperse ", " al)
400
401 expand_aliases :: [Entry] -> [Entry]
402 expand_aliases el = 
403     let expand_alias (Entry name alist _) = 
404             [ Entry a [] ("See \\textit{" ++ name ++ "}.") | a <- alist ]
405     in nub $ concat [ expand_alias e | e <- el ]
406
407 main :: IO ()
408 main = do
409   hPutStrLn stdout $ format_glossary glossary
410   exitWith ExitSuccess