2 * Copyright (c) 2009, 2010, 2012, 2015, 2016, ETH Zurich.
3 * Copyright (c) 2015, 2016 Hewlett Packard Enterprise Development LP.
6 * This file is distributed under the terms in the attached LICENSE file.
7 * If you do not find this file, copies can be found by writing to:
8 * ETH Zurich D-INFK, Universitaetstr. 6, CH-8092 Zurich. Attn: Systems Group.
14 This file defines the Barrelfish capability type system.
16 (Meta-)Comments about the syntax are enclosed between /** ... **/
17 Comments of the Hamlet language are enclosed between /* ... */
20 /** We can define some constants using the "define" construct **/
22 /* XXX: these must match the corresponding OBJBITS definitions in
23 * barrelfish_kpi/capabilities.h */
25 /* Size of L2 CNode: L2 resolves 8 bits of Cap address space */
26 define objsize_l2cnode 16384;
28 define objsize_dispatcher 1024;
29 /* Size of (x86_64) VNode: */
30 define objsize_vnode 4096; /* BASE_PAGE_SIZE */
31 /* Size of ARMv7 VNodes */
32 define objsize_vnode_arm_l1 16384;
33 define objsize_vnode_arm_l2 1024;
34 /* size of a kernel control block */
35 define objsize_kcb 65536; /* OBJSIZE_KCB */
36 /* size of a mapping cap:
37 * if mappings are zero-sized they mess up range queries */
38 define objsize_mapping 1;
41 The capabilities of the whole system are listed thereafter.
42 The minimal definition consists of a name and an empty body.
45 cap Null is_never_copy {
46 /* Null/invalid object type */
51 For a populated cap, we need to give the type and name of each
52 of its fields, such as:
53 "genpaddr base;" for instance
55 In order to implement various comparisons, we need to specify a address
56 and size for each type that is backed by memory. The size may be
57 specified directly with "size" or as "size_bits".
59 Additional equality fields can be specified with an "eq" prefix, as in
63 address genpaddr base; /* Physical base address of Memory object */
64 pasid pasid; /* Physical Address Space ID */
65 size gensize bytes; /* Size of region in bytes */
70 /* Physical address range (root of cap tree) */
71 cap PhysAddr from_self inherit Memory;
73 cap Mapping abstract {
74 "struct capability" cap;
79 address { get_address(cap) };
80 size { objsize_mapping };
84 address genpaddr base; /* Base address of VNode */
85 size { objsize_vnode };
88 /** The following caps are similar to the previous one **/
90 /* RAM memory object */
91 cap RAM from PhysAddr from_self inherit Memory;
93 /* Abstract CNode, need to define size */
95 address lpaddr cnode; /* Base address of CNode */
96 caprights rightsmask; /* Cap access rights */
99 /* Level 1 CNode table, resizable */
100 cap L1CNode from RAM inherit CNode {
101 size gensize allocated_bytes; /* Allocated size of L1 CNode in bytes */
104 /* Level 2 CNode table, resolves 8 bits of cap address */
105 cap L2CNode from RAM inherit CNode {
106 size { objsize_l2cnode }; /* Size of L2 CNode in bytes (16kB) */
110 /* Foreign CNode capability */
112 eq genpaddr cnode; /* Base address of CNode */
113 eq uint8 bits; /* Number of bits this CNode resolves */
114 caprights rightsmask;
115 eq coreid core_id; /* The core the cap is local on */
116 uint8 guard_size; /* Number of bits in guard */
117 caddr guard; /* Bitmask already resolved when reaching this CNode */
120 /** Dispatcher is interesting is several ways. **/
123 XXX: The whole multi_retype stuff is hack in hamlet that should be removed as
124 soon as parts of an object can be retyped individually. -MN
127 cap Dispatcher from RAM {
131 The Dispatcher is a special case that can be retyped several
132 times to an end-point
134 /** Note: This must be the first statement */
138 We allow the use of unknow structures. However, equality will
139 be defined by address, not by structure.
141 "struct dcb" dcb; /* Pointer to kernel DCB */
143 address { mem_to_phys(dcb) };
144 size { objsize_dispatcher };
147 cap EndPoint from Dispatcher {
150 "struct dcb" listener; /* Dispatcher listening on this endpoint */
151 lvaddr epoffset; /* Offset of endpoint buffer in disp frame */
152 uint32 epbuflen; /* Length of endpoint buffer in words */
154 address { mem_to_phys(listener) };
157 Preferable definitions for address and size would be as below. These
158 should be used as soon as the whole multi retype hack stuff is fixed:
160 address { mem_to_phys(listener + epoffset) };
167 /** Then, we go back to routine **/
169 cap Frame from RAM from_self inherit Memory;
171 cap Frame_Mapping from Frame inherit Mapping;
173 cap DevFrame from PhysAddr from_self inherit Memory;
175 cap DevFrame_Mapping from DevFrame inherit Mapping;
177 cap Kernel is_always_copy {
178 /* Capability to a kernel */
182 /* x86_64-specific capabilities: */
185 cap VNode_x86_64_pml4 from RAM inherit VNode;
187 cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping;
190 cap VNode_x86_64_pdpt from RAM inherit VNode;
192 cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping;
195 cap VNode_x86_64_pdir from RAM inherit VNode;
197 cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping;
200 cap VNode_x86_64_ptable from RAM inherit VNode;
202 cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping;
205 /* x86_32-specific capabilities: */
208 cap VNode_x86_32_pdpt from RAM inherit VNode;
210 cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping;
213 cap VNode_x86_32_pdir from RAM inherit VNode;
215 cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping;
218 cap VNode_x86_32_ptable from RAM inherit VNode;
220 cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping;
222 /* ARM specific capabilities: */
225 cap VNode_ARM_l1 from RAM inherit VNode {
226 size { objsize_vnode_arm_l1 };
229 cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping;
232 cap VNode_ARM_l2 from RAM inherit VNode {
233 size { objsize_vnode_arm_l2 };
236 cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping;
238 /* ARM AArch64-specific capabilities: */
241 cap VNode_AARCH64_l0 from RAM inherit VNode;
243 cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping;
246 cap VNode_AARCH64_l1 from RAM inherit VNode;
248 cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping;
251 cap VNode_AARCH64_l2 from RAM inherit VNode;
253 cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping;
256 cap VNode_AARCH64_l3 from RAM inherit VNode;
258 cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping;
260 /** IRQTable and IO are slightly different **/
262 cap IRQTable is_always_copy {
263 /* IRQ Routing table */
265 When testing two IRQTable caps for is_copy, we always return True: all
266 IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort
272 /* IRQ Destination capability.
273 Represents a slot in a CPUs int vector table.
274 Can be connected to a LMP endpoint to recv this interrupt. */
279 cap IRQSrc from_self {
280 /* IRQ Source capability.
281 Represents an interrupt source. It contains a range of interrupt
288 /* Legacy IO capability */
290 eq uint16 end; /* Granted IO range */
293 /* IPI notify caps */
299 /* ID capability, system-wide unique */
301 eq coreid coreid; /* core cap was created */
302 eq uint32 core_local_id; /* per core unique id */
305 cap PerfMon is_always_copy {
308 /** KernelControlBlock represents a struct kcb which contains all the pointers
309 * to core-local global state of the kernel.
311 cap KernelControlBlock from RAM {
314 address { mem_to_phys(kcb) };
315 /* base page size for now so we can map the kcb in boot driver */
316 size { objsize_kcb };
319 cap IPI is_always_copy {};