doc: tn13: update capability type section
[barrelfish] / doc / 013-capability-mgmt / type_system.tex
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 \chapter{Type system}\label{chap:type_system}
3
4 In this chapter, we cover the type model of capabilities and the
5 supported types in Barrelfish.
6
7 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8 \section{Type Model}
9 \note{We do not implement capability rights yet.}
10     
11 \begin{description}
12 \item[Name] Each type has a unique name.
13
14 \item[Origin] A capability type is either \emph{primitive}, which
15   means that capabilities of the type may be created only through a
16   special process (eg. at boot time), or \emph{derived}, which means
17   that capabilities of the type may be created by retyping an existing
18   capability. For primitive types, we specify how the capabilities of
19   that type are created; for derived types, we specify which
20   capability types may be retyped to yield a capability of the given
21   type.
22
23 \item[Retypability] Some types of capability may be \emph{retyped} to
24   create one or more new capabilities of the same or different
25   type. If this is the case, we specify for each type from what other types of
26   capability it may be retyped.
27
28 \item[Mint parameters] It is possible to specify type-specific
29   parameters when \emph{minting} capabilities. We specify for each
30   type the interpretation of the type-specific parameters. When not
31   specified, they are ignored.
32
33 \item[Interpretation of rights] The interpretation of the primitive
34   capability rights is type-specific. A capability type defines the
35   interpretation of these rights, usually in the specification of the
36   legal invocations.
37
38 \item[Transferability to another core] Depending on its type, it may
39   or may not be possible to transfer a capability to another core.
40
41 \item[Last copy deleted] The type specific operations to perform when
42   the last copy of a capability is deleted. For capability types
43     that refer to actual memory, if the last reference to a piece of
44     memory is deleted, then the memory must be garbage collected.
45
46 \item[Concrete representations] Each capability type has one or more
47   representations: in the memory of each core on which it may appear,
48   and in a canonical serialised representation used for transferring
49   it in a message between cores. These are specified as
50   Hamlet\cite{dagand:fof:plos09} data types.
51
52 \item[Invocations] Most capability types support one or more
53   type-specific operations through the use of the invoke system call.
54   (documented in \ref{sec:sys_invoke}).
55 \end{description}
56
57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
58 \section{Types}
59   
60 \subsection{CNode}\label{sec:cnode}
61
62 A CNode refers to an array of capabilities of some power-of-two size.
63 CNodes are used to hierarchically construct the CSpace of a domain, as
64 described in \ref{sec:cspace}.  All capability management is
65 performed through invocations on CNodes.
66
67 CNodes are organized as a two-level table with distinct capability types for
68 the root or L1 CNode (which can be dynamically enlarged), and L2 or leaf
69 CNodes which have a fixed size of 256 capability slots.
70 The two-level CNode table forms a 32-bit capability address space for each
71 dispatcher.
72 User space refers to entries in that address space with a 32-bit
73 \emph{capability address}.
74 The high 24 bits of the capability address are used as an index into the L1
75 CNode.
76 The L1 CNode index can be too large for a given L1 CNode that has not been
77 enlarged to it's maximum size of $2^24$ slots.
78 A user space operation referring to an L1 slot that is not allocated will fail
79 with \verb|SYS_ERR_L1_CNODE_INDEX|.
80 The CPU driver then uses the L1 index to perform a lookup for the L2 CNode.
81 If an L2 CNode exists for the given L1 index, the low 8 bits of the supplied
82 capability address are used as an index into the L2 CNode.
83 The CPU driver then uses the L2 index to perform a lookup for the requested
84 capability.
85
86 Many CNode invocations require that the caller provide both a CSpace
87 address and the number of \emph{levels} to resolve. This allows the
88 invocations to refer to a L2 CNode capability that is located in a L1 slot,
89 and thus would usually be recursed through by the address resolution
90 algorithm.
91
92 \begin{description}
93 \item[Origin] Retyping from RAM type capabilities
94
95 \item[Retypability] No
96
97 \item[Mint parameters] No
98
99 \item[Interpretation of rights] \note{Explain rights and rights mask.
100   Capability rights and rights masks are currently not implemented.
101   This means that every user domain holding a capability has full
102   rights to it.}
103
104 \item[Transferability to another core] Yes.  When transfered to
105   another core, capability is implicitly retyped to a Foreign CNode
106   type.
107     \note{We currently allow CNode type caps to be transferred without doing
108     the type conversion, which is extremely risky, but does not break the
109     system if the receiver only ever tries to copy capabilities out of the
110     received CNode.}
111
112 \item[Last copy deleted] When the last copy is deleted, all
113   capabilities stored within it are also deleted.
114
115 \item[Concrete representations] The in-memory representation is as follows:
116     
117   \begin{lstlisting}[language=Mackerel]
118     datatype L1CNode "L1 CNode capability" {
119       cnode 64 "Physical base address of CNode";
120       size  64 "Allocated size of CNode in bytes";
121       rightsmask 8 "Capability rights mask";
122     };
123     \end{lstlisting}
124
125     \begin{lstlisting}[language=Mackerel]
126       datatype L2CNode "L2 CNode capability" {
127         cnode 64 "Physical base address of CNode";
128         rightsmask 8 "Capability rights mask";
129       };
130     \end{lstlisting}
131
132     Note that L2 CNodes have a fixed size of 16384 bytes, which is
133     \textbf{not} stored in their in-memory representation.
134 \end{description}
135
136 \begin{invocation}{Mint}\label{sec:mint}
137  \arg Capability of the source cspace root CNode to invoke
138  \arg Destination cspace cap address relative to source cspace
139  \arg Destination CNode address relative to destination cspace
140  \arg Slot in destination CNode cap to place copy into
141  \arg Address of cap to copy.
142  \arg Level/depth of 'to'.
143  \arg Level/depth of 'from'.
144  \arg 1st cap-dependent parameter.
145  \arg 2nd cap-dependent parameter.
146 \end{invocation}
147 The Mint invocation creates a new capability in an existing CNode
148 slot, given an existing capability.  The new capability will be a copy
149 of the existing capability, except for changes to the
150 \emph{type-specific parameters}.
151
152 The use of the two type-specific parameters is described along with
153 the description of the relevant type.
154
155 \begin{invocation}{Copy}
156  \arg Capability of the source cspace root CNode to invoke
157  \arg Capability address of destination root cnode relative to our cspace
158  \arg CNode address to place copy into relative to destination cspace.
159  \arg Slot in CNode cap to place copy into.
160  \arg Capability address of source root cnode relative to our cspace
161  \arg Address of cap to copy.
162  \arg Level/depth of 'to'.
163  \arg Level/depth of 'from'.
164 \end{invocation}
165 This invocation is similar to Mint, but does not change any
166 type-specific data. In fact, the CPU driver currently uses the same code path
167 for copy and mint, and a mint with both cap-dependent parameters set to zero
168 will behave exactly like a Copy invocation.
169
170 \begin{invocation}{Retype}
171  \arg Capability of the source cspace root CNode to invoke
172  \arg Source cspace cap address in our cspace.
173  \arg Address of cap to retype in source cspace.
174  \arg Offset into cap to retype
175  \arg Kernel object type to retype to.
176  \arg Size of created objects, for variable-sized types
177  \arg Number of objects to create
178  \arg Destination cspace cap address in our cspace
179  \arg Address of CNode cap in destination cspcae to place retyped caps into.
180  \arg Level/depth of CNode cap in destination cspace
181  \arg Slot in CNode cap to start placement.
182 \end{invocation}
183
184 This invocation creates one or more new descendant capabilities of the
185 specified type in the specified slots, given a source capability and a
186 destination type.
187 It will fail if the source or destination are invalid, or if the capability
188 already has descendants which overlap the requested region (some capability
189 types, currently only the dispatcher type can be retyped even if it already
190 has descendants).
191 The destination slots must all occupy the same CNode.  The permissible
192 source/destination pairs are shown in \ref{fig:cap_types} and
193 \ref{tab:retype_types}.
194 The number of new capabilities created is given as an argument.
195 The invocation can fail if the retype region, which is defined as a pair of
196 base address and size does not fit into the source capability.
197 The retype region's base address is given as an offset into the source
198 capability, and it's size is given as the number of capabilities to create
199 multiplied by the requested size for the new capabilities.
200
201 \note{check tables and figure for validity in 2017}
202
203 \ctable[
204   caption=Permissible types for the Retype invocation,
205   label=tab:retype_types,
206 ]{lll}{}{
207   \FL Source & Destination & Variable size?\ML
208   Physical address range & Physical address range & Yes\NN
209   Physical address range & RAM & Yes\NN
210   Physical address range & Device frame & Yes\NN
211   RAM & RAM & Yes\NN
212   RAM & CNode & Yes\NN
213   RAM & VNode & No\NN
214   RAM & Dispatcher & No\NN
215   RAM & Frame & Yes\NN
216   Dispatcher & IDC endpoint & No\NN
217 }
218
219 \begin{figure}
220   \centering
221   \includegraphics[width=.7\columnwidth]{cap_types}
222   \caption{Valid capability retyping paths}\label{fig:cap_types}
223 \end{figure}
224   
225 \begin{invocation}{Delete}
226  \arg Capability of the CNode to invoke
227  \arg Address of cap to delete.
228  \arg Level/depth of 'cap'.
229 \end{invocation}
230 This invocation deletes the capability at the given address, freeing
231 the associated CNode slot.
232
233 \begin{invocation}{Revoke}
234  \arg Capability of the CNode to invoke
235  \arg Address of cap to delete.
236  \arg Level/depth of 'cap'.
237 \end{invocation}
238 This invocation revokes the capability at the given address.
239
240 The capability itself is left untouched while all its descendants and
241 copies are deleted.
242
243 \subsection{Foreign CNode}
244 \note{This has not been implemented yet}
245
246 The foreign CNode capability gives a domain on a core the ability to
247 specify a capability that actually resides on another core.  This
248 capability allows for the holder to create local copies of the
249 capabilities stored in the actual CNode modulo rights as can be
250 implemented.  The capability tracks on which core the actual CNode
251 resides.  \note{Full implementation and discussion pending}
252
253 \begin{description}
254 \item[Origin] When a CNode capability are copied to another core.
255
256 \item[Retyability] No
257
258 \item[Mint parameters] None
259   
260 \item[Interpretation of rights] \note{Explain rights}
261   
262 \item[Transferability to another core] Yes
263
264 \item[Last copy deleted] \note{NYI}
265   
266 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
267   
268   \begin{lstlisting}[language=Mackerel]
269     datatype fcnode_cap "Foreign CNode capability" {
270       cnode      64  "Physical base address of CNode";
271       bits        8  "Number of bits this CNode resolves";
272       rightsmask  8  "Capability rights mask";
273       core_id     8  "Core id of the core the actual CNode capability
274                       resides in";
275       guard_size  8  "Number of bits in guard word";
276       guard      32  "Bitmask already resolved when reaching this CNode";
277     };
278   \end{lstlisting}
279     \note{This should not be used as-is, as we have changed the CNodes
280     themselves significantly in 2016.}
281 \end{description}
282
283 \note{Discussion pending on invocations}
284
285 \subsection{Physical address range}
286
287 Most domains will generally not handle capabilities of this type.
288 They are introduced because the kernel relies on the user-space
289 software to decide the location of RAM.
290
291 By retyping physical address range capabilities to RAM, the caller
292 guarantees that the underlying region does contain RAM that can safely
293 be used for storage of kernel objects.  Any domain with access to
294 physical address range capabilities is therefore a critical part of
295 the trusted computing base.
296
297 \begin{description}
298 \item[Origin] Created at boot time in the bsp core based on the
299   multiboot info.
300
301 \item[Mint parameters] None
302   
303 \item[Retyability] To Physical address range, RAM or DevFrame type.
304   
305 \item[Interpretation of rights] \note{Explain rights}
306   
307 \item[Transferability to another core] Yes
308
309 \item[Last copy deleted] \note{NYI, maybe inform some special
310   dispatcher like memory server}
311   
312 \item[Concrete representations] The in-memory representation is as follows:
313   
314   \begin{lstlisting}[language=Mackerel]
315     datatype physaddr_cap "Physical address range capability" {
316       base       64  "Physical base address of region";
317       bytes      64  "Size of region";
318     };
319   \end{lstlisting}
320 \end{description}
321
322 \subsection{RAM}
323
324 A RAM capability refers to a naturally-aligned power-of-two-sized
325 region of kernel-accessible memory.
326
327 \begin{description}
328 \item[Origin] Retyping from physical address range capabilities.
329   
330 \item[Retyability] To RAM, Frame, CNode, VNode, or Dispatcher types.
331   
332 \item[Mint parameters] None
333   
334 \item[Interpretation of rights] \note{Explain rights}
335   
336 \item[Transferability to another core] Yes
337
338 \item[Last copy deleted] \note{NYI, maybe inform some special
339   dispatcher like memory server}
340   
341 \item[Concrete representations] The in-memory representation is as follows:
342   
343   \begin{lstlisting}[language=Mackerel]
344     datatype ram_cap "RAM capability" {
345       base       64  "Physical base address of region";
346       bytes      64  "Size of region";
347     };
348   \end{lstlisting}
349 \end{description}
350
351 \subsection{Dispatcher}
352 This capability type refers to the kernel object associated with a
353 user-level dispatcher.
354
355 \begin{description}
356 \item[Origin] Retyping from RAM capabilities.
357   
358 \item[Retyability] To IDC Endpoint type
359   
360 \item[Mint parameters] None
361   
362 \item[Interpretation of rights] \note{Explain rights}
363   
364 \item[Transferability to another core] No
365
366 \item[Last copy deleted] \note{NYI, maybe inform some special
367   dispatcher like spawn daemon}
368   
369 \item[Concrete representations] The in-memory representation on x86-64
370   is as follows:
371   
372   \begin{lstlisting}[language=Mackerel]
373     datatype dcb_cap "Dispatcher capability" {
374       dcb        64  "Pointer to the in kernel representation of
375                       the dispatcher control block";
376     };
377   \end{lstlisting}
378 \end{description}
379
380 \begin{invocation}{Setup}
381  \arg Address of dispatcher capability relative to dispatchers caller's cspace
382  \arg Address of existing dispatcher for domain ID relative to caller's cspace
383  \arg Root of CSpace for new dispatcher relative to caller's cspace
384  \arg Root of VSpace for new dispatcher relative to cspace for new dispatcher.
385  \arg Frame capability for dispatcher structure relative to cspace for new dispatcher.
386  \arg Make runnable if true
387 \end{invocation}
388 This invocation sets any of the above parameters on a dispatcher
389 object.  If any of the CSpace addresses are null, they are ignored.
390 Additionally, once all of the parameters are set (either in a single
391 invocation, or after multiple invocations), and if the runnable flag
392 is set, the dispatcher is made runnable.  \note{There are additional
393   invocations in the code that we have not discussed yet.}
394
395 \subsection{IDC Endpoint}
396     
397 Every IDC endpoint refers both to a dispatcher and an \emph{endpoint
398   buffer} within that dispatcher. The endpoint buffer is specified as
399 an offset from the start of the dispatcher frame, and is the location
400 where the kernel delivers IDC messages. It is also delivered to the
401 user with an LRPC message.  The initial endpoint offset of an IDC
402 endpoint capability when it is retyped from a dispatcher capability is
403 zero; the capability cannot be used to send IDC until the the offset
404 is specified changed by minting an endpoint to another endpoint.
405
406 \begin{description}
407 \item[Origin] Retyping Dispatcher type capabilities.
408
409 \item[Mint parameters] The mint parameters can be used to change the
410   badge on the capability
411   \begin{itemize}
412   \item Parameter 1: The endpoint offset to set on the capability.
413   \item Parameter 2: The endpoint buffer size to set on the capability.
414   \end{itemize}
415   
416 \item[Retyability] No
417   
418 \item[Interpretation of rights] \note{Explain rights}
419   
420 \item[Transferability to another core] No
421
422 \item[Last copy deleted] \note{NYI, inform some entity to initiate
423   connection teardown}
424   
425 \item[Concrete representations] The in-memory representation on x86-64
426   is as follows:
427   
428   \begin{lstlisting}[language=Mackerel]
429     datatype idc_cap "IDC endpoint capability" {
430       listener     64  "Pointer to the in kernel representation of the
431                         receiver's dispatcher control block";
432       epoffset     64  "Offset of endpoint buffer within dispatcher
433                         structure";
434       buflen       32  "Length of endpoint buffer in words";
435     };
436   \end{lstlisting}
437   
438 \item[Invocation] Any invocation of an endpoint capability causes the
439   entire message to be delivered to the dispatcher to which the
440   endpoint refers.
441   \end{description}
442
443 \subsection{VNode}
444 A VNode capability refers to a hardware page table and is used to
445 manage a domain's virtual address space.  Frame and device frame
446 capabilities can be copied or minted into them or deleted from them by
447 invoking a CNode.  The architecture may impose limitations on the
448 capabilities that may be copied into a VNode, or may allow extra
449 attributes to be set when minting.
450
451 We define one VNode capability type per hardware page table type per
452 architecture.
453
454 \begin{description}
455 \item[Origin] Retyping from RAM type capabilities.
456
457 \item[Retyability] No
458
459 \item[Mint parameters] None
460   
461 \item[Interpretation of rights] \note{Explain rights}
462   
463 \item[Transferability to another core] \note{Discussion pending}
464
465 \item[Last copy deleted] \note{NYI, initiate mechanisms to unmap from
466   associated page tables and remove mapped in page tables and frames}
467   
468 \item[Concrete representations] The in-memory representation on x86-64
469   is as follows:
470   
471   \begin{lstlisting}[language=Mackerel]
472     datatype vnode_cap "VNode capability" {
473       base     64  "Base address of the page table";
474     };
475   \end{lstlisting}
476 \end{description}  
477
478 \subsection{Frame}
479 A frame capability refers to a page-aligned\footnote{We coloquially refer to
480 4kB pages as pages} region of physical memory with a size that is a multiple
481 of 4096 bytes.
482 A frame capability may be mapped into a domain's virtual address space (by
483 copying it to a VNode).
484 When a frame capability is created (ie.~retyped from RAM), the kernel
485 zero-fills the frame.
486 \note{Is this a good idea? Shouldn't we be able to pre-zero frames?
487   -AB}
488
489 \begin{description}
490 \item[Origin] Retyping from RAM type capabilities.
491   
492 \item[Retyability] To Frame type
493   
494 \item[Mint parameters] None
495   
496 \item[Interpretation of rights] \note{Explain rights}
497   
498 \item[Transferability to another core] Yes
499
500 \item[Any copy deleted] Look up associated \emph{Mapping} capability and use
501   information stored in that mapping to remove any page table entries that
502   exist for this copy of the frame capability.
503
504 \item[Last copy deleted] Check whether there are any other capabilities that
505   refer to the region, or a superset of the region, referred to by this
506     capability. If not, return create a new RAM capability and return it to a
507     specially identified ``memory server'' dispatcher.
508   
509 \item[Concrete representations] The in-memory representation is as follows:
510   
511   \begin{lstlisting}[language=Mackerel]
512     datatype frame_cap "Frame capability" {
513       base       64  "Physical base address of mappable region";
514       bytes      64  "Size of the region";
515     };
516   \end{lstlisting}
517 \end{description}  
518
519 \noarginvocation{Identify}
520 This invocation returns the physical address and size (in bytes) of the frame.
521
522 \subsection{Device frame}
523 A device frame capability refers to a page-aligned region of physical address
524 space, with a size that is a multiple of 4096, that may be mapped into a
525 domain's virtual address space (by copying it to a VNode).
526 Unlike frame capabilities, the kernel does not zero-fill device frame
527 capabilities upon mapping.
528 As the name implies, device frames are typically used for access to
529 memory-mapped devices.
530
531 \begin{description}
532 \item[Origin] Retyping Physical address range type capabilities.
533   
534 \item[Retyability] To Device frame type
535   
536 \item[Mint parameters] None
537   
538 \item[Interpretation of rights] \note{Explain rights}
539   
540 \item[Transferability to another core] Yes
541
542 \item[Any copy deleted] Look up associated \emph{Mapping} capability and use
543   information stored in that mapping to remove any page table entries that
544   exist for this copy of the frame capability.
545
546 \item[Last copy deleted] Check whether there are any other capabilities that
547   refer to the region, or a superset of the region, referred to by this
548     capability. If not, return create a new RAM capability and return it to a
549     specially identified ``memory server'' dispatcher.
550   
551 \item[Concrete representations] The in-memory representation is as follows:
552   
553   \begin{lstlisting}[language=Mackerel]
554     datatype device_cap "Device Frame capability" {
555       base       64  "Physical base address of region";
556       bytes      64  "Size of the region";
557     };
558   \end{lstlisting}
559 \end{description}  
560
561 \noarginvocation{Identify} This invocation returns the physical
562 address and size (in bytes) of the frame.
563
564 \subsection{IO}
565 An IO capability gives the holder the ability to read and write to IO ports.
566 IO capabilities are currently only supported on x86-64.
567
568 \begin{description}
569 \item[Origin] A single IO capability covering the whole IO region created at
570   boot time in the BSP core.
571   
572 \item[Retyability] No
573   
574 \item[Mint parameters] Used to specify the region of io space the capability can access.
575   \begin{itemize}
576   \item Parameter 1: Start of the region
577   \item Parameter 2: End of the region
578   \end{itemize}
579   
580 \item[Interpretation of rights] \note{Explain rights}
581   
582 \item[Transferability to another core] Yes
583
584 \item[Last copy deleted] \note{NYI}
585   
586 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
587   
588   \begin{lstlisting}[language=Mackerel]
589     datatype io_cap "IO capability" {
590       start      16  "Start of the granted IO range";
591       end        16  "End of the granted IO range";
592     };
593   \end{lstlisting}
594 \end{description}
595
596 \begin{invocation}{Outb}
597   \arg IO port number
598   \arg Output data
599 \end{invocation}
600 This invocation writes a byte to the the specified IO port
601
602 \begin{invocation}{Outw}
603   \arg IO port number
604   \arg Output data
605 \end{invocation}
606 This invocation writes a two byte word to the the specified IO port
607
608 \begin{invocation}{Outd}
609   \arg IO port number
610   \arg Output data
611 \end{invocation}
612 This invocation writes a four byte to the the specified IO port
613
614 \begin{invocation}{Inb}
615   \arg IO port number
616 \end{invocation}
617 This invocation returns a byte read from the specified IO port.
618
619 \begin{invocation}{Inw}
620   \arg IO port number
621 \end{invocation}
622 This invocation returns a 16-bit word read from the specified IO port.
623
624 \begin{invocation}{Ind}
625   \arg IO port number
626 \end{invocation}
627 This invocation returns a 32-bit doubleword read from the specified IO port.
628
629 \subsection{IRQ table capability}
630 The IRQ table capability allows the holder to configure the user-level
631 handler dispatcher that will be invoked when the kernel receives
632 device interrupts.
633
634 \note{Discuss new IRQSrc and IRQDest capabilities}
635
636 \begin{description}
637 \item[Origin] Given to the first domain spawned on a core.
638   
639 \item[Retyability] No
640   
641 \item[Mint parameters] None
642   
643 \item[Interpretation of rights] \note{Explain rights}
644   
645 \item[Transferability to another core] No
646
647 \item[Last copy deleted] \note{NYI}
648   
649 \item[Concrete representations] This capability type has no
650   representation associated with it as it is used to simply give
651   permissions to the holders and does not refer to any kernel data
652   structure.
653   \end{description}
654
655 \begin{invocation}{Set}
656   \arg IRQ number
657   \arg CSpace address of asynchronous endpoint capability
658 \end{invocation}
659 This invocation sets the user-level handler endpoint that will receive
660 a message when the given interrupt occurs.  While a handler is set,
661 interrupts will be delivered as IDC messages.
662
663
664 \begin{invocation}{Delete}
665   \arg IRQ number
666 \end{invocation}
667 This invocation clears the handler for the given IRQ.
668
669 \subsection{Kernel Capability}
670 This capability is used to confer authority to the user-space part of the
671 Barrelfish kernel, the ``monitor''.
672 Some other privileged domains also receive a copy of the kernel capability,
673 but we should factor those operations out and create different capability
674 types that give those dispatchers only the right to invoke the operations they
675 actually need.
676 One example of such a dispatcher is the dispatcher that brings up new cores.
677
678 \begin{description}
679 \item[Origin] Given to the first domain spawned on a core.
680   
681 \item[Retyability] No
682   
683 \item[Mint parameters] None
684   
685 \item[Interpretation of rights] \note{Explain rights}
686   
687 \item[Transferability to another core] No
688
689 \item[Last copy deleted] \note{NYI}
690   
691 \item[Concrete representations] The in-memory representation is as follows:
692   
693   \begin{lstlisting}[language=Mackerel]
694     datatype kernel_cap "Kernel capability" {
695     };
696   \end{lstlisting}
697
698     The kernel capability does not convey any information, it is simply a
699     token of authority.
700 \end{description}
701
702 \begin{invocation}{Spawn core}
703   \arg Apic ID of the core to try booting
704   \arg CSpace address of the RAM capability to use to relocate the new kernel
705   \arg CSpace address of the Dispatcher capability of the first domain to run
706   \arg Number of valid bits for the root CNode to associate with the Dispatcher capability
707   \arg CSpace address of the root CNode to associate with the Dispatcher capability
708   \arg CSpace address of the VNode to associate with the Dispatcher capability
709   \arg CSpace address of the dispatcher frame to associate with the Dispatcher capability
710 \end{invocation}
711 The invocation requests the kernel to try booting another core.  The
712 kernel is to be relocated into the given memory region and to run the
713 the given domain.
714
715 \begin{invocation}{Get core ID}
716   \arg None
717 \end{invocation}
718 The invocation returns the APIC ID of the core.
719
720 \begin{invocation}{Identify capability}
721   \arg CSpace address of the capability to identify
722   \arg Level of the capability to identify
723   \arg Location of buffer to hold capability representation
724 \end{invocation}
725 The invocation stores the kernel's in-memory representation of the
726 capability into the given buffer.
727 j
728 \begin{invocation}{Identify another dispatcher's capability}
729   \arg CSpace address of the dispatcher's L1 cnode capability
730   \arg Level in our CSpace of the L1 cnode capability
731   \arg CSpace address relative to the dispatcher's CSpace of the capability to
732   identify
733   \arg Level in the dispatcher's CSpace of the capability to identify
734   \arg Location of buffer to hold capability representation
735 \end{invocation}
736 The invocation stores the kernel's in-memory representation of another
737 dispatcher's capability into the given buffer.
738
739 \begin{invocation}{Create capability}
740   \arg In memory representation of a capability
741   \arg CSpace address of the CNode the place the created capability in
742   \arg Level of the CNode in the CSpace
743   \arg Slot number to place the capability in
744   \arg Owning core of the new capability
745 \end{invocation}
746 Creates the given capability in the given slot in the given CNode with the
747 given Owner.
748
749 \note{TODO: KernelCmd_Copy_existing}
750
751 \begin{invocation}{Set capability's remote relations}
752   \arg CSpace address of CSpace (L1 CNode) in which to look for capability
753   \arg Level of root capability.
754   \arg CSpace address of capability
755   \arg Level of capability
756   \arg Remote relations to set.
757   \arg Mask: bitmask to show which remote relations to set.
758 \end{invocation}
759 If mask is not zero, set remote relations according to the bits set in the
760 expression \verb|remote_relations & mask|.
761 Always returns the remote relations bitmask after potentially setting new
762 remote relations.
763
764 \begin{invocation}{Read capability's remote relations}
765   \arg CSpace address of capability
766   \arg Level of capability
767 \end{invocation}
768 Returns bitmask of currently set remote relations on capability.
769
770 \begin{itemize}
771   \item \verb|KernelCmd_Get_arch_id|: Returns arch id of caller's core
772   \item \verb|KernelCmd_Nullify_cap|: Set the capability to NULL allowed it to be reused
773   \item \verb|KernelCmd_Setup_trace|: Set up trace buffer
774   \item \verb|KernelCmd_Register|: Register monitor notify endpoint
775   \item \verb|KernelCmd_Domain_Id|: Set domain ID of dispatcher
776   \item \verb|KernelCmd_Get_cap_owner|:
777   \item \verb|KernelCmd_Set_cap_owner|:
778   \item \verb|KernelCmd_Lock_cap|:
779   \item \verb|KernelCmd_Unlock_cap|:
780   \item \verb|KernelCmd_Delete_last|:
781   \item \verb|KernelCmd_Delete_foreigns|:
782   \item \verb|KernelCmd_Revoke_mark_target|:
783   \item \verb|KernelCmd_Revoke_mark_relations|:
784   \item \verb|KernelCmd_Delete_step|:
785   \item \verb|KernelCmd_Clear_step|:
786   \item \verb|KernelCmd_Retype|:
787   \item \verb|KernelCmd_Has_descendants|:
788   \item \verb|KernelCmd_Is_retypeable|:
789   \item \verb|KernelCmd_Sync_timer|:
790   \item \verb|KernelCmd_IPI_Register|:
791   \item \verb|KernelCmd_IPI_Delete|:
792   \item \verb|KernelCmd_GetGlobalPhys|:
793   \item \verb|KernelCmd_Add_kcb|: add extra kcb to be scheduled
794   \item \verb|KernelCmd_Remove_kcb|: remove kcb from scheduling ring
795   \item \verb|KernelCmd_Suspend_kcb_sched|: suspend/resume kcb scheduler
796   \item \verb|KernelCmd_Get_platform|: Get architecture platform
797
798 \note{The other invocations are outdated and will probably change
799   when the monitors are discussed}