147a0a5f59b089ed22551ce5473de85164c586b8
[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 A CNode capability stores a \emph{guard} and \emph{guard size}, which
68 is expressed as a number of bits. As in guarded page
69 tables\cite{Liedtke_GPT}, the guard allows the depth of the CSpace
70 tree to be reduced by skipping levels that would only contain a single
71 mapping. When resolving a CSpace address that has led to a CNode
72 capability, the guard is compared with the corresponding number of
73 bits from the remaining part of the address, and if it does not match,
74 the lookup fails.
75
76 Many CNode invocations require that the caller provide both a CSpace
77 address and the number of \emph{valid bits} in the address. This
78 allows the invocations to refer to another CNode capability that is
79 located at an intermediate level in the tree, and thus would usually
80 be recursed through by the address resolution algorithm. If the number
81 of valid bits associated with a CSpace is less than the size of a full
82 CSpace address, only the least significant bits that are valid, but
83 starting with the most significant bit thereof, are used, and the
84 address lookup terminates early.
85
86 \begin{description}
87 \item[Origin] Retyping from RAM type capabilities
88
89 \item[Retypability] No
90
91 \item[Mint parameters] The mint parameters can be used to set a guard
92   on a CNode.
93   \begin{itemize}
94   \item Parameter 1: The guard to set.
95   \item Parameter 2: The size of the guard in bits.
96   \end{itemize}
97
98 \item[Interpretation of rights] \note{Explain rights and rights mask.
99   Capability rights and rights masks are currently not implemented.
100   This means that every user domain holding a capability has full
101   rights to it.}
102
103 \item[Transferability to another core] Yes.  When transfered to
104   another core, capability is implicitly retyped to a Foreign CNode
105   type. \note{We do not allow CNode type caps to be transferred yet.}
106
107 \item[Last copy deleted] When the last copy is deleted, all
108   capabilities stored within it are also deleted.
109
110 \item[Concrete representations] The in-memory representation of on
111   x86-64 is as follows:
112     
113   \begin{lstlisting}[language=Mackerel]
114     datatype cnode_cap "CNode capability" {
115       cnode 64 "Physical base address of CNode";
116       bits 8 "Number of bits this CNode resolves";
117       rightsmask 8 "Capability rights mask";
118       guard_size 8 "Number of bits in guard word";
119       guard 32 "Bitmask already resolved when reaching this CNode";
120     };
121     \end{lstlisting}
122 \end{description}
123
124 \begin{invocation}{Mint}\label{sec:mint}
125   \arg CSpace address of destination CNode
126   \arg Slot number in destination CNode
127   \arg CSpace address of source capability
128   \arg Number of valid bits in destination CNode address
129   \arg Number of valid bits in source capability address
130   \arg Type-specific parameter 1
131   \arg Type-specific parameter 2
132 \end{invocation}
133 The Mint invocation creates a new capability in an existing CNode
134 slot, given an existing capability.  The new capability will be a copy
135 of the existing capability, except for changes to the
136 \emph{type-specific parameters}.
137
138 The use of the two type-specific parameters is described along with
139 the description of the relevant type.
140
141 If the destination capability is of type VNode, then instead of a
142 mint, a page table entry is made into the page table pointed to by the
143 VNode.  In this case, the source capabilities must be of type VNode,
144 Frame, or Device Frame.  The first parameter specifies architecture
145 specific page (table) attributes and the second parameter specifies an
146 offset from the source frame/device frame to map.
147   
148 \begin{invocation}{Copy}
149   \arg CSpace address of destination CNode
150   \arg Slot number in destination CNode
151   \arg CSpace address of source capability
152   \arg Number of valid bits in destination CNode address
153   \arg Number of valid bits in source capability address
154 \end{invocation}
155 This invocation is similar to Mint, but does not change any
156 type-specific data.
157
158 If the destination capability is of type VNode, then instead of a
159 copy, a page table entry is made into the page table pointed to by the
160 VNode.  In this case, the source capabilities must be of type VNode,
161 Frame, or Device Frame.
162
163 \begin{invocation}{Retype}
164   \arg CSpace address of source capability to retype
165   \arg Type of new objects to create
166   \arg Size in bits of each object, for variable-sized objects
167   \arg CSpace address of destination CNode
168   \arg Slot number in desination CNode of the first created capability
169   \arg Number of valid bits in destination CNode address
170 \end{invocation}
171
172 This invocation creates one or more new descendant capabilities of the
173 specified type in the specified slots, given a source capability and a
174 destination type.  It will fail if the source or destination are
175 invalid, or if the capability already has descendants. (some
176 capability types, currently only the dispatcher type can be retyped
177 even if it already has descendants).  The destination slots must all
178 occupy the same CNode.  The permissible source/destination pairs are
179 shown in \ref{fig:cap_types} and \ref{tab:retype_types}.  The number
180 of new capabilities created is determined by the size of the source
181 capability divided by the size of the newly-created objects.
182
183 \ctable[
184   caption=Permissible types for the Retype invocation,
185   label=tab:retype_types,
186 ]{lll}{}{
187   \FL Source & Destination & Variable size?\ML
188   Physical address range & Physical address range & Yes\NN
189   Physical address range & RAM & Yes\NN
190   Physical address range & Device frame & Yes\NN
191   RAM & RAM & Yes\NN
192   RAM & CNode & Yes\NN
193   RAM & VNode & No\NN
194   RAM & Dispatcher & No\NN
195   RAM & Frame & Yes\NN
196   Dispatcher & IDC endpoint & No\NN
197 }
198
199 \begin{figure}
200   \centering
201   \includegraphics[width=.7\columnwidth]{cap_types}
202   \caption{Valid capability retyping paths}\label{fig:cap_types}
203 \end{figure}
204   
205 \begin{invocation}{Delete}
206   \arg CSpace address of capability to delete
207   \arg Number of valid bits in capability address
208 \end{invocation}
209 This invocation deletes the capability at the given address, freeing
210 the associated CNode slot.
211
212 \begin{invocation}{Revoke}
213   \arg CSpace address of capability to Revoke
214   \arg Number of valid bits in capability address
215 \end{invocation}
216 This invocation revokes the capability at the given address.
217
218 The capability itself is left untouched while all its descendants and
219 copies are deleted.
220
221 \subsection{Foreign CNode}
222 \note{This has not been implemented yet}
223
224 The foreign CNode capability gives a domain on a core the ability to
225 specify a capability that actually resides on another core.  This
226 capability allows for the holder to create local copies of the
227 capabilities stored in the actual CNode modulo rights as can be
228 implemented.  The capability tracks on which core the actual CNode
229 resides.  \note{Full implementation and discussion pending}
230
231 \begin{description}
232 \item[Origin] When a CNode capability are copied to another core.
233
234 \item[Retyability] No
235
236 \item[Mint parameters] None
237   
238 \item[Interpretation of rights] \note{Explain rights}
239   
240 \item[Transferability to another core] Yes
241
242 \item[Last copy deleted] \note{NYI}
243   
244 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
245   
246   \begin{lstlisting}[language=Mackerel]
247     datatype fcnode_cap "Foreign CNode capability" {
248       cnode      64  "Physical base address of CNode";
249       bits        8  "Number of bits this CNode resolves";
250       rightsmask  8  "Capability rights mask";
251       core_id     8  "Core id of the core the actual CNode capability
252                       resides in";
253       guard_size  8  "Number of bits in guard word";
254       guard      32  "Bitmask already resolved when reaching this CNode";
255     };
256   \end{lstlisting}
257 \end{description}
258
259 \note{Discussion pending on invocations}
260
261 \subsection{Physical address range}
262
263 Most domains will generally not handle capabilities of this type.
264 They are introduced because the kernel relies on the user-space
265 software to decide the location of RAM.
266
267 By retyping physical address range capabilities to RAM, the caller
268 guarantees that the underlying region does contain RAM that can safely
269 be used for storage of kernel objects.  Any domain with access to
270 physical address range capabilities is therefore a critical part of
271 the trusted computing base.
272
273 \begin{description}
274 \item[Origin] Created at boot time in the bsp core based on the
275   multiboot info.
276
277 \item[Mint parameters] None
278   
279 \item[Retyability] To Physical address range, RAM or DevFrame type.
280   
281 \item[Interpretation of rights] \note{Explain rights}
282   
283 \item[Transferability to another core] Yes
284
285 \item[Last copy deleted] \note{NYI, maybe inform some special
286   dispatcher like memory server}
287   
288 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
289   
290   \begin{lstlisting}[language=Mackerel]
291     datatype physaddr_cap "Physical address range capability" {
292       base       64  "Physical base address of region";
293       bits        8  "Size of region";
294     };
295   \end{lstlisting}
296 \end{description}
297
298 \subsection{RAM}
299
300 A RAM capability refers to a naturally-aligned power-of-two-sized
301 region of kernel-accessible memory.
302
303 \begin{description}
304 \item[Origin] Retyping from physical address range capabilities.
305   
306 \item[Retyability] To RAM, Frame, CNode, VNode, or Dispatcher types.
307   
308 \item[Mint parameters] None
309   
310 \item[Interpretation of rights] \note{Explain rights}
311   
312 \item[Transferability to another core] Yes
313
314 \item[Last copy deleted] \note{NYI, maybe inform some special
315   dispatcher like memory server}
316   
317 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
318   
319   \begin{lstlisting}[language=Mackerel]
320     datatype ram_cap "RAM capability" {
321       base       64  "Physical base address of region";
322       bits        8  "Size fo region";
323     };
324   \end{lstlisting}
325 \end{description}
326
327 \subsection{Dispatcher}
328 This capability type refers to the kernel object associated with a
329 user-level dispatcher.
330
331 \begin{description}
332 \item[Origin] Retyping from RAM capabilities.
333   
334 \item[Retyability] To IDC Endpoint type
335   
336 \item[Mint parameters] None
337   
338 \item[Interpretation of rights] \note{Explain rights}
339   
340 \item[Transferability to another core] No
341
342 \item[Last copy deleted] \note{NYI, maybe inform some special
343   dispatcher like spawn daemon}
344   
345 \item[Concrete representations] The in-memory representation on x86-64
346   is as follows:
347   
348   \begin{lstlisting}[language=Mackerel]
349     datatype dcb_cap "Dispatcher capability" {
350       dcb        64  "Pointer to the in kernel representation of
351                       the dispatcher control block";
352     };
353   \end{lstlisting}
354 \end{description}
355
356 \begin{invocation}{Setup}
357   \arg CSpace address of domain's root CNode (root of CSpace)
358   \arg Number of valid bits in root CNode address
359   \arg CSpace address of domain's root VNode (root page table)
360   \arg Number of valid bits in root VNode address
361   \arg CSpace address of dispatcher frame (user-level dispatcher
362   data) capability
363   \arg Whether to make dispatcher runnable
364 \end{invocation}
365 This invocation sets any of the above parameters on a dispatcher
366 object.  If any of the CSpace addresses are null, they are ignored.
367 Additionally, once all of the parameters are set (either in a single
368 invocation, or after multiple invocations), and if the runnable flag
369 is set, the dispatcher is made runnable.  \note{There are additional
370   invocations in the code that we have not discussed yet.}
371
372 \subsection{IDC Endpoint}
373     
374 Every IDC endpoint refers both to a dispatcher and an \emph{endpoint
375   buffer} within that dispatcher. The endpoint buffer is specified as
376 an offset from the start of the dispatcher frame, and is the location
377 where the kernel delivers IDC messages. It is also delivered to the
378 user with an LRPC message.  The initial endpoint offset of an IDC
379 endpoint capability when it is retyped from a dispatcher capability is
380 zero; the capability cannot be used to send IDC until the the offset
381 is specified changed by minting an endpoint to another endpoint.
382
383 \begin{description}
384 \item[Origin] Retyping Dispatcher type capabilities.
385
386 \item[Mint parameters] The mint parameters can be used to change the
387   badge on the capability
388   \begin{itemize}
389   \item Parameter 1: The endpoint offset to set on the capability.
390   \end{itemize}
391   
392 \item[Retyability] No
393   
394 \item[Interpretation of rights] \note{Explain rights}
395   
396 \item[Transferability to another core] No
397
398 \item[Last copy deleted] \note{NYI, inform some entity to initiate
399   connection teardown}
400   
401 \item[Concrete representations] The in-memory representation on x86-64
402   is as follows:
403   
404   \begin{lstlisting}[language=Mackerel]
405     datatype idc_cap "IDC endpoint capability" {
406       listener     64  "Pointer to the in kernel representation of the
407                         receiver's dispatcher control block";
408       epoffset     64  "Offset of endpoint buffer within dispatcher
409                         structure";
410     };
411   \end{lstlisting}
412   
413 \item[Invocation] Any invocation of an endpoint capability causes the
414   entire message to be delivered to the dispatcher to which the
415   endpoint refers.
416   \end{description}
417
418 \subsection{VNode}
419 A VNode capability refers to a hardware page table and is used to
420 manage a domain's virtual address space.  Frame and device frame
421 capabilities can be copied or minted into them or deleted from them by
422 invoking a CNode.  The architecture may impose limitations on the
423 capabilities that may be copied into a VNode, or may allow extra
424 attributes to be set when minting.
425
426 \begin{description}
427 \item[Origin] Retyping from RAM type capabilities.
428
429 \item[Retyability] No
430
431 \item[Mint parameters] None
432   
433 \item[Interpretation of rights] \note{Explain rights}
434   
435 \item[Transferability to another core] \note{Discussion pending}
436
437 \item[Last copy deleted] \note{NYI, initiate mechanisms to unmap from
438   associated page tables and remove mapped in page tables and frames}
439   
440 \item[Concrete representations] The in-memory representation on x86-64
441   is as follows:
442   
443   \begin{lstlisting}[language=Mackerel]
444     datatype vnode_cap "VNode capability" {
445       base     64  "Base address of the page table";
446     };
447   \end{lstlisting}
448 \end{description}  
449
450 \subsection{Frame}
451 A frame capability refers to a naturally-aligned power-of-two-sized
452 region of physical memory that may be mapped into a domain's virtual
453 address space (by copying it to a VNode).  When a frame capability is
454 created (ie.~retyped from RAM), the kernel zero-fills the frame.
455 \note{Is this a good idea? Shouldn't we be able to pre-zero frames?
456   -AB}
457
458 \begin{description}
459 \item[Origin] Retyping from RAM type capabilities.
460   
461 \item[Retyability] To Frame type
462   
463 \item[Mint parameters] None
464   
465 \item[Interpretation of rights] \note{Explain rights}
466   
467 \item[Transferability to another core] Yes
468
469 \item[Last copy deleted] \note{NYI, initiate unmapping from page
470   tables.  We may choose for this to happen when the last copy of a
471   frame within a dispatcher is deleted rather than the last copy in
472   the entire system.}
473   
474 \item[Concrete representations] The in-memory representation on x86-64
475   is as follows:
476   
477   \begin{lstlisting}[language=Mackerel]
478     datatype frame_cap "Frame capability" {
479       base       64  "Physical base address of untyped region";
480       bits        8  "Size of the region";
481     };
482   \end{lstlisting}
483 \end{description}  
484
485 \noarginvocation{Identify}
486 This invocation returns the physical address and size (in bits) of the frame.
487
488 \subsection{Device frame}
489 A device frame capability refers to a naturally-aligned
490 power-of-two-sized region of physical address space that may be mapped
491 into a domain's virtual address space (by copying it to a VNode).
492 Unlike frame capabilties, the kernel does not zero-fill device frame
493 capabilities upon mapping.  As the name implies, device frames are
494 typically used for access to memory-mapped devices.
495
496 \begin{description}
497 \item[Origin] Retyping Physical address range type capabilities.
498   
499 \item[Retyability] To Device frame type
500   
501 \item[Mint parameters] None
502   
503 \item[Interpretation of rights] \note{Explain rights}
504   
505 \item[Transferability to another core] Yes
506
507 \item[Last copy deleted] \note{NYI, initiate unmapping from page
508   tables.  We may choose for this to happen when the last copy of a
509   frame within a dispatcher is deleted rather than the last copy in
510   the entire system.}
511   
512 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
513   
514   \begin{lstlisting}[language=Mackerel]
515     datatype device_cap "Device Frame capability" {
516       base       64  "Physical base address of region";
517       bits        8  "Size of the region";
518     };
519   \end{lstlisting}
520 \end{description}  
521
522 \noarginvocation{Identify} This invocation returns the physical
523 address and size (in bits) of the frame.
524
525 \subsection{IO}
526 IO capability gives the holder the ability to read and write to IO
527 ports.
528
529 \begin{description}
530 \item[Origin] A single capability created at boot time in the bsp core.
531   
532 \item[Retyability] No
533   
534 \item[Mint parameters] Used to specify the region of io space the capability can access.
535   \begin{itemize}
536   \item Parameter 1: Start of the region
537   \item Parameter 2: End of the region
538   \end{itemize}
539   
540 \item[Interpretation of rights] \note{Explain rights}
541   
542 \item[Transferability to another core] Yes
543
544 \item[Last copy deleted] \note{NYI}
545   
546 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
547   
548   \begin{lstlisting}[language=Mackerel]
549     datatype io_cap "IO capability" {
550       start      16  "Start of the granted IO range";
551       end        16  "End of the granted IO range";
552     };
553   \end{lstlisting}
554 \end{description}
555
556 \begin{invocation}{Outb}
557   \arg IO port number
558   \arg Output data
559 \end{invocation}
560 This invocation writes a byte to the the specified IO port
561
562 \begin{invocation}{Outw}
563   \arg IO port number
564   \arg Output data
565 \end{invocation}
566 This invocation writes a two byte word to the the specified IO port
567
568 \begin{invocation}{Outd}
569   \arg IO port number
570   \arg Output data
571 \end{invocation}
572 This invocation writes a four byte to the the specified IO port
573
574 \begin{invocation}{Inb}
575   \arg IO port number
576 \end{invocation}
577 This invocation returns a byte read from the specified IO port.
578
579 \begin{invocation}{Inw}
580   \arg IO port number
581 \end{invocation}
582 This invocation returns a 16-bit word read from the specified IO port.
583
584 \begin{invocation}{Ind}
585   \arg IO port number
586 \end{invocation}
587 This invocation returns a 32-bit doubleword read from the specified IO port.
588
589 \subsection{IRQ table capability}
590 The IRQ table capability allows the holder to configure the user-level
591 handler dispatcher that will be invoked when the kernel receives
592 device interrupts.
593
594 \begin{description}
595 \item[Origin] Given to the first domain spawned on a core.
596   
597 \item[Retyability] No
598   
599 \item[Mint parameters] None
600   
601 \item[Interpretation of rights] \note{Explain rights}
602   
603 \item[Transferability to another core] No
604
605 \item[Last copy deleted] \note{NYI}
606   
607 \item[Concrete representations] This capability type has no
608   representation associated with it as it is used to simply give
609   permissions to the holders and does not refer to any kernel data
610   structure.
611   \end{description}
612
613 \begin{invocation}{Set}
614   \arg IRQ number
615   \arg CSpace address of asynchronous endpoint capability
616 \end{invocation}
617 This invocation sets the user-level handler endpoint that will receive
618 a message when the given interrupt occurs.  While a handler is set,
619 interrupts will be delivered as IDC messages.
620
621
622 \begin{invocation}{Delete}
623   \arg IRQ number
624 \end{invocation}
625 This invocation clears the handler for the given IRQ.
626
627 \subsection{Kernel Capability}
628 So far, this capability is treated as the magic capability that gives
629 the holder a backdoor into performing special operations in the
630 kernel.
631
632 \begin{description}
633 \item[Origin] Given to the first domain spawned on a core.
634   
635 \item[Retyability] No
636   
637 \item[Mint parameters] None
638   
639 \item[Interpretation of rights] \note{Explain rights}
640   
641 \item[Transferability to another core] No
642
643 \item[Last copy deleted] \note{NYI}
644   
645 \item[Concrete representations] The in-memory representation on x86-64 is as follows:
646   
647   \begin{lstlisting}[language=Mackerel]
648     datatype kernel_cap "Kernel capability" {
649       kernel_id   8  "Id of the Kernel";
650     };
651   \end{lstlisting}
652 \end{description}
653
654 \begin{invocation}{Spawn core}
655   \arg Apic ID of the core to try booting
656   \arg CSpace address of the RAM capability to use to relocate the new kernel
657   \arg CSpace address of the Dispatcher capability of the first domain to run
658   \arg Number of valid bits for the root CNode to associate with the Dispatcher capability
659   \arg CSpace address of the root CNode to associate with the Dispatcher capability
660   \arg CSpace address of the VNode to associate with the Dispatcher capability
661   \arg CSpace address of the dispatcher frame to associate with the Dispatcher capability
662 \end{invocation}
663 The invocation requests the kernel to try booting another core.  The
664 kernel is to be relocated into the given memory region and to run the
665 the given domain.
666
667 \begin{invocation}{Get core ID}
668   \arg None
669 \end{invocation}
670 The invocation returns the APIC ID of the core.
671
672 \begin{invocation}{Identify capability}
673   \arg CSpace address of the capability to identify
674   \arg Number of valid bits in the capability
675   \arg Location of buffer to hold capability representation
676 \end{invocation}
677 The invocation stores the kernel's in-memory representation of the
678 capability into the given buffer.
679
680 \begin{invocation}{Identify CNode, get capability}
681   \arg In memory representation of a CNode capability
682   \arg Slot number of a capability within the CNode capability
683   \arg Location of buffer to hold capability representation
684 \end{invocation}
685 The invocation stores the kernel's in-memory representation of the
686 capability located at the given slot in the given CNode into the given
687 buffer.
688
689 \begin{invocation}{Create capability}
690   \arg In memory representation of a capability
691   \arg CSpace address of the CNode the place the created capability in
692   \arg Number of valid bits in the CSpace address of the CNode
693   \arg Slot number to place the capability in
694 \end{invocation}
695 Creates the given capability in the given slot in the given CNode.
696
697 \begin{invocation}{Create capability}
698   \arg In memory representation of a capability
699   \arg CSpace address of the CNode the place the created capability in
700   \arg Number of valid bits in the CSpace address of the CNode
701   \arg Slot number to place the capability in
702 \end{invocation}
703 Creates the given capability in the given slot in the given CNode.
704
705 \note{The other invocations are outdated and will probably change
706   when the monitors are discussed}