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
12module Main where
13
14import System.Exit
15import System.IO
16import Text.Printf
17import Data.List
18import qualified Data.Char
19
20data Entry = Entry {
21      entry_title :: String,
22      entry_aliases :: [ String ],
23      entry_description :: String
24} deriving (Show,Eq)
25
26
27glossary :: [ Entry ]
28glossary = [ Entry "dispatcher control block" [ "DCB" ]
29             "The kernel object representing the dispatcher.  DCBs are \
30             \referred to by specially typed capabilities.",
31
32             Entry "kernel control block" ["KCB"]
33             "The kernel object representing all per-core state. KCBs are \
34             \referred to by special capability types.",
35
36             Entry "Driver Domain" []
37             "A driver domain executes one or more drivers. It is special in the sense that \
38             \it communicates with Kaluga to act on requests to spawn or destroy new driver \
39             \instances.",
40
41             Entry "Driver Module" []
42             "A Barrelfish driver module is a piece of code (typically a library) that describes the logic \
43             \for interacting with a device. It follows a well defined structure that allows Kaluga to interface with an \
44             \instantiated driver (see Driver Instance) to control its life-cycle.",
45
46             Entry "Driver Instance" []
47             "A driver is the runtime object instantiated from a given driver module. In practice any number of instances\
48             \can be created from a driver module and executed within one or more driver domains.",
49
50             Entry "Boot driver" []
51
52             "A piece of code running on a ``home core'' to manage a ``target core''. \
53             \It encapsulates the hardware functionality to boot, suspend, resume, \
54             \and power-down the latter.",
55
56             Entry "CPU driver" []
57
58             "The code running on a core which executes in kernel or \
59             \privileged mode.  CPU drivers are the Barrelfish \
60             \equivalent of a kernel, except that there is one per \
61             \core, and they share no state or synchronization. CPU \
62             \drivers are typically non-preemptible, \
63             \single-threaded, and mostly stateless.",
64
65             Entry "Mackerel" []
66
67             "The Domain Specific Language used in Barrelfish to specify \
68             \device hardware registers and hardware-defined in-memory \
69             \data structures.  The Mackerel compiler takes such a \
70             \description and outputs a \
71             \C header file containing inline functions to read and \
72             \write named bitfields for a device or data structure, \
73             \together with string formatting code to aid in \
74             \debugging.  Mackerel input files are found in the \
75             \\\texttt{/devices} directory of the source tree, and end \
76             \in \\texttt{.dev}.  Generated header files are found in \
77             \the \\texttt{/include/dev} subdirectory of the build \
78             \tree.",
79
80             Entry "interconnect driver" [ "ICD" ]
81
82             "A partial abstraction of low-level message passing \
83             \mechanism, such as a shared-memory buffer or hardware \
84             \message passing primitive.  ICDs do not present a uniform \
85             \interface, and therefore require specific stubs to be \
86             \generated by Flounder.  Similarly, they do not present \
87             \any particular semantics with regard to flow control, \
88             \polled or upcall-based delivery, etc.  A special case of \
89             \an ICD is the local message passing (LMP) mechanism, \
90             \which is implemented for every type of core and provide \
91             \communication between dispatchers running on that core.",
92
93             Entry "notification driver" [ "ND" ]
94
95             "A partial abstraction of a low-level message passing \
96             \mechanism which performs notification (sending an \
97             \event), rather than transferring data per se.  In \
98             \Barrelfish these mechanisms are separated where \
99             \possible for flexibility and to further decouple \
100             \sender and receiver.  Notification drivers exist in \
101             \Barrelfish for sending inter-processor interrupts on \
102             \most architectures, for example.",
103
104             Entry "Flounder" []
105
106             "The Interface Definition Language used for \
107             \communication between domains in Barrelfish.  Flounder \
108             \supports message type signatures, various concrete type \
109             \constructors like structs and arrays, and also some \
110             \opaque types like capabilities and interface \
111             \references.  The Flounder compiler is written in \
112             \Haskell and generates code in C or THC.  Flounder \
113             \generates specialized code for each Interconnect Driver \
114             \in a system.",
115
116             Entry "Hake" [ "Hakefile" ]
117
118             "The build system for Barrelfish.  The Barrelfish source \
119             \tree consists of a Hakefile in each relevant source \
120             \directory, which contains a single Haskell expression \
121             \specifying a list of targets to be built.  Hake itself \
122             \aggregates all these Hakefiles, and uses them to generate \
123             \a single Makefile in a separate, build directory.  This \
124             \Makefile contains an explicit target for \\emph{every} \
125             \file that can be built for Barrelfish for every \
126             \appropriate architecture.  A separate, manually-edited \
127             \Makefile contains convenient symbolic targets for \
128             \creating boot images, etc.  Since the contents of \
129             \Hakefiles are Haskell expressions, quite powerful \
130             \constructs can be used to specify how to build files for \
131             \different targets.",
132
133             Entry "Elver" []
134
135             "An intermediate boot loader for booting 64-bit \
136             \ELF images on Intel-architecture machines where the main \
137             \boot loader (such as Grub) does not support entering a \
138             \kernel in long mode.  Elver is specified as the first \
139             \module of the multiboot image, and puts the boot \
140             \processor into long mode before jumping to the CPU \
141             \driver, which is assumed to be in the second multiboot \
142             \module.",
143
144             Entry "Filet-o-Fish" [ "FoF" ]
145
146             "An embedding of C into Haskell, used for writing C code \
147             \generators for Haskell-based domain specific languages.  \
148             \Instead of using C syntax combinators (as used in \
149             \Flounder and Mackerel) FoF-based DSLs (such as Fugu and \
150             \Hamlet) use backend which are actually semantic \
151             \specifications of behavior, from which FoF can generates \
152             \C code which is guaranteed to implement the given \
153             \semantics.",
154
155             Entry "Fugu" [ "errno.h" ]
156
157             "A small domain-specific language (implemented using \
158             \Filet-o-Fish) to express error conditions and messages \
159             \for Barrelfish.  Fugu offloads the problem of tracking \
160             \error messages and code, and also implements a short \
161             \error ``stack'' in machine word to provide more detailed \
162             \error information.  Fugu generates the \\texttt{errno.h} \
163             \file.",
164
165             Entry "THC" []
166
167             "A dialect of C with extensions to support the \
168             \asynchronous message passing flavor of most Barrelfish \
169             \services by providing an \\texttt{async} construct and \
170             \continuations.  THC also integrates with specially generated \
171             \Flounder stubs.",
172
173             Entry "System Knowledge Base" [ "SKB" ]
174
175             "A repository for hardware-derived system information in \
176             \a running Barrelfish system.  The SKB is currently a port \
177             \of the ECLiPse Constraint Logic Programming system, and is \
178             \used for (among other things) PCI bridge programming, \
179             \interrupt routing, and constructing routing trees for \
180             \intra-machine multicast. The SKB runs as a system service \
181             \accessed by message passing.",
182
183             Entry "Octopus" []
184
185             "A service built on (and colocated with) the SKB which \
186             \provides locking functionality inspired by Chubby and \
187             \Zookeeper, and publish/subscribe notification for \
188             \Barrelfish processes.",
189
190             Entry "Kaluga" []
191
192             "The Barrelfish device manager.  Kaluga is responsible \
193             \to starting and stopping device drivers in response to \
194             \hardware events, and based on configurable system \
195             \policies.",
196
197             Entry "capability space" [ "cspace" ]
198
199             "The set of capabilities held by a dispatcher on a core \
200             \is organized in a guarded page table structure \
201             \implemented as a tree of CNodes, where internal nodes are \
202             \CNodes and leaf nodes are non-CNode capabilities.  This \
203             \allows any capability held by a dispatcher to be referred \
204             \to using a 32-bit address; when invoking a capability, \
205             \the CPU driver walks the cspace structure resolving a \
206             \variable number of bits of this address at each level. \
207             \This means that capabilities used frequently should be \
208             \stored near the top of the tree, preferably in the root \
209             \CNode.  Some CPU drivers allow a fast path where the \
210             \32-bit address is implicitly assumed to simply an offset \
211             \in the root CNode.  The capability for the root CNode can \
212             \be efficiently found from the DCB; note that, unlike the \
213             \vspace, the cspace is purely local to a core and cannot \
214             \be shared between dispatchers on difference cores.",
215
216             Entry "vspace" []
217
218             "An object representing a virtual address space.  Unlike \
219             \a cspace, a vspace can under some circumstances be shared \
220             \between cores.  However, a vspace is tied to a particular \
221             \core architecture, and a particular physical address \
222             \space, though vspaces can be manipulated on other cores \
223             \and even cores of other architectures.  Mappings are \
224             \created in a vspace by specifying capabilities to regions \
225             \of memory that are mappable (such as frame \
226             \capabilities).",
227
228             Entry "Aquarium" []
229
230             "A visualization tool for Barrelfish trace data. Aquarium \
231             \is written in C\\# and can accept data as a stream over \
232             \the network from a running Barrelfish machine, or from a \
233             \trace file.  It displays a time line showing which \
234             \dispatchers are running on which cores, messages between \
235             \dispatchers, and other system events.",
236
237             Entry "Hamlet" []
238
239             "The language used to specify all Barrelfish capability \
240             \types, together with their in-memory formats and \
241             \transformation rules when transferring a capability from \
242             \one core to another.  Hamlet is implemented using \
243             \Filet-o-Fish and generates capability dispatch code for \
244             \CPU drivers, among other things. \
245             \Surprisingly, Hamlet is a type of fish.",
246
247             Entry "Local Message Passing" [ "LMP" ]
248
249             "Each Barrelfish CPU driver includes a special \
250             \Interconnect Driver for passing messages between \
251             \dispatchers on the same core, often based on the \
252             \concepts from LRPC and L4 IPC.  This is referred to as \
253             \LMP.",
254
255             Entry "dispatcher" []
256
257             "The data structure representing an application's \
258             \runnability on a core.  Dispatchers contain scheduling \
259             \state, message end points, and upcall entry points; they \
260             \are the nearest equivalent to processes in Unix. \
261             \Dispatchers are always tied to a core.  A Barrelfish \
262             \application can be viewed as a collection of dispatchers \
263             \spread across the set of cores on which the application \
264             \might run, together with associated other resources. \
265             \The term is from K42. Multiple dispatchers may share a vspace\
266             \or cspace.",
267
268             Entry "monitor" []
269
270             "A privileged process running on a core which handles \
271             \most core OS functionality not provided by the CPU \
272             \driver.  Since CPU drivers do not directly communicate \
273             \with each other, the task of state coordination in \
274             \Barrelfish is mostly handled by Monitors.  Monitors are \
275             \also responsible for setting up inter-core communication \
276             \channels (``binding''), and transferring capabilities \
277             \between cores.  When a capability is retyped or revoked, \
278             \the monitors are responsible for ensuring that this \
279             \occurs consistently system-wide.  The monitor for a core \
280             \holds a special capability (the kernel capability) which \
281             \allows it to manipulate certain data structures in the \
282             \CPU driver, such as the capability database.",
283
284             Entry "User-level Message Passing" [ "UMP", "CC-UMP" ]
285
286             "A series of Interconnect Drivers which use \
287             \cache-coherent shared memory to send cache-line \
288             \sized frames between cores.  UMP is based on ideas \
289             \from URPC, and avoids kernel transitions on message \
290             \send and receive.  It is the preferred channel for \
291             \communication between cores on an Intel-architecture \
292             \PC, for example.  However, because it operates \
293             \entirely in user space, it cannot send capabilities \
294             \between cores.  Instead, the Flounder stubs for UMP \
295             \send capabilities via another channel through LMP to \
296             \the local monitor, which forwards them correctly to \
297             \the destination.",
298
299             Entry "capability" [ "cap" ]
300
301             "Barrelfish uses ``partitioned capabilities'' to refer to \
302             \most OS resources (most of which are actually typed areas \
303             \of memory).  Operations on such resources are typically \
304             \carried out ``invoking'' an operation on the capability \
305             \via a system call to the local CPU driver.  Capabilities \
306             \are fixed-size data structures which are held in areas of \
307             \memory called CNodes, and which cannot be directly read \
308             \from or written to by user mode programs.  Instead, users \
309             \move capabilities between CNodes by invoking operations \
310             \on the capability that refers to the CNode.  Capabilities \
311             \can be ``retyped'' and progressively refined from pure \
312             \memory capabilities to ones which can be mapped into an \
313             \address space, for example, or used as CNodes.  The set \
314             \of capability types understood by Barrelfish is defined \
315             \using the Hamlet language.",
316
317             Entry "physical address capability" []
318
319             "A capability referring to a raw region of physical \
320             \address space.  This is the most basic type of \
321             \capability; all other capability types which refer to \
322             \memory are ultimately subtypes of this.",
323
324             Entry "RAM capability" []
325
326             "A capability type which refers to a region of Random \
327             \Access Memory.  A direct subtype of a Physical Address \
328             \capability.",
329
330             Entry "device frame capability" []
331
332             "A capability type which refers to a region of physical \
333             \address space containing memory-mapped I/O registers. A \
334             \direct subtype of a Physical Address capability.",
335
336
337             Entry "CNode capability" []
338
339             "A capability type referring to a CNode.",
340
341             Entry "foreign capability" []
342
343             "A capability referring to a resource which only makes \
344             \sense on a different core to the one it exists on.  For \
345             \example, since the cspace is purely local to core, \
346             \transferring a CNode capability to another core \
347             \transforms it into a Foreign CNode capability, whose only \
348             \operations are to remotely manipulate (principally copy \
349             \capabilities from) the original CNode.",
350
351             Entry "dispatcher capability" []
352
353             "A capability referring to the memory region occupied by \
354             \a Dispatcher Control Block.",
355
356             Entry "endpoint capability" []
357
358             "A capability referring to a (core-local) communication \
359             \endpoint.  Posession of such a capability enables the \
360             \holder to send a message to endpoint.",
361
362             Entry "frame capability" []
363
364             "A capability refering to a \
365             \set of page frames which can be mapped into a \
366             \virtual address space.  Frame capabilities are a \
367             \subtype of RAM capabilities; the latter cannot be \
368             \mapped.",
369
370             Entry "kernel capability" []
371
372             "A capability enabling the holder to manipulate CPU \
373             \driver data structures (in particular, the capability \
374             \database).  The kernel capability for a core is only held \
375             \by the core's monitor.",
376
377             Entry "vnode capability" []
378
379             "One of a set of capability types, one for each format of \
380             \page table page for each architecture supported by \
381             \Barrelfish.  For example, there are four Vnode capability \
382             \types for the x86-64 architecture, corresponding to the \
383             \PML4, PDPT, PDIR, and PTABLE pages in a page table.",
384
385             Entry "IO capability" []
386
387             "A capability enabling the holder to perform IO space \
388             \operations on Intel architecture machines.  Each IO \
389             \capability grants access to a range of IO space addresses \
390             \on a specific core.",
391
392             Entry "capability node" [ "cnode" ]
393
394             "A region of RAM containing capabilities.  A CNode cannot \
395             \be mapped into a virtual address space, and so can only \
396             \be accessed by operations on the CNode capability which \
397             \refers to it -- this is how strict partitioning of \
398             \capability memory from normal memory is achieved.  The \
399             \set of CNodes which can be referenced by a single \
400             \dispatcher is called the cspace.",
401
402             Entry "scheduler manifest" []
403
404             "A description of the scheduling requirements of \
405             \multiprocessor application, used to inform the various \
406             \system schedulers about how best to dispatch the \
407             \application's threads.",
408
409             Entry "dite" []
410
411             "A tool used to build a boot image in the proprietary Intel \
412             \``32.obj'' format, for booting on the Single-chip Cloud \
413             \Computer.",
414
415             Entry "Pleco" []
416
417             "The Domain Specific Language used in Barrelfish to specify \
418             \constants for the tracing infrastructure.  The Pleco \
419             \compiler takes such description and outputs a \
420             \C header file containing the definitions, a C source \
421             \file with the constants, and a JSON file to be used by \
422             \host visualization tools.",
423
424             Entry "Beehive" []
425
426             "Beehive was an experimental soft-core processor \
427             \designed by Chuck Thacker at Microsoft Research Silicon \
428             \Valley.  Beehive was implemented in a simulator and on \
429             \FPGAs, in particular the BEE3 processor emulation board \
430             \(which could run up to 15 Beehive cores at a time). \
431             \The architecture had a number of unusual features, in \
432             \particular, a ring interconnect for message passing, a \
433             \software-visible FIFO on each core for incoming messages, \
434             \and a memory system implemented using message passing \
435             \(loads and stores became RPCs to the memory system). \
436             \Barrelfish was ported to the Beehive processor but \
437             \support for the architecture was eventually dropped \
438             \after the Beehive project completed.",
439
440
441             Entry "BSP Core" []
442
443             "Refers to the bootstrap processor, meaning the first \
444             \processor that is usually booted by the boot-loader or firmware on a hardware \
445             \architecture.",
446
447             Entry "APP Core" []
448             "Application processor, processors booted either by the BSP \
449             \or other APP cores and not the initial boot-loader or firmware.",
450
451             Entry "Domain" []
452
453             "The word domain is used to refer to the user-level \
454             \code sharing a protection domain and (usually) an address space. \
455             \A domain consists of one or more dispatchers.",
456
457             Entry "Channel" []
458
459             "A uni-directional kernel-mediated communication path \
460             \between dispatchers. All messages travel over channels. Holding a \
461             \capability for a channel guarantees the right to send a message to it \
462             \(although the message may not be sent for reasons other than \
463             \protection).",
464
465             Entry "Mapping Database" []
466
467             "The mapping database is used to facilitate retype and revoke operations. \
468             \A capability that is not of type dispatcher, can only be retyped once. \
469             \The mapping database facilitates this check. \
470             \When a capability is revoked, all its descendants and copies are deleted. \
471             \The mapping database keeps track of descendants and copies of a capability \
472             \allowing for proper execution of a revoke operation. \
473             \Each core has a single private mapping database. \
474             \All capabilities on the core must be included in the database.",
475
476             Entry "Descendant" []
477             "A capability X is a descendant of a capability A if: \
478             \X was retyped from A, \
479             \or X is a descendant of A1 and A1 is a copy of A, \
480             \or X is a descendant of B and B is a descendant of A, \
481             \or X is a copy of X1 and X1 is a descendant of A.",
482
483             Entry "Ancestor" []
484             "A capability A is an ancestor of a capability X if X is a descendant of A.",
485
486             Entry "ZZZ terms yet to be added" []
487
488             "asmoffsets, retype, iref"
489
490           ]
491
492
493compare_entry :: Entry -> Entry -> Ordering
494compare_entry (Entry k1 _ _) (Entry k2 _ _) =
495    compare (map Data.Char.toLower k1) (map Data.Char.toLower k2)
496
497format_glossary :: [Entry] -> String
498format_glossary gl =
499    let full_gl = gl ++ (expand_aliases gl)
500        sort_gl = sortBy compare_entry full_gl
501    in unlines [ format_entry e | e <- sort_gl ]
502
503format_entry :: Entry -> String
504format_entry (Entry title aliases description) =
505    printf "\\item[%s:] %s\n" (format_aliases title aliases) description
506
507format_aliases :: String -> [String] -> String
508format_aliases t [] = t
509format_aliases t al =
510    printf "%s \\textrm{\\textit{(%s)}}" t (concat $ intersperse ", " al)
511
512expand_aliases :: [Entry] -> [Entry]
513expand_aliases el =
514    let expand_alias (Entry name alist _) =
515            [ Entry a [] ("See \\textit{" ++ name ++ "}.") | a <- alist ]
516    in nub $ concat [ expand_alias e | e <- el ]
517
518main :: IO ()
519main = do
520  hPutStrLn stdout $ format_glossary glossary
521  exitWith ExitSuccess
522