IRQ: Allow retyping of IRQSrc capability
[barrelfish] / capabilities / caps.hl
1 /*
2  * Copyright (c) 2009, 2010, 2012, 2015, 2016, ETH Zurich.
3  * Copyright (c) 2015, 2016 Hewlett Packard Enterprise Development LP.
4  * All rights reserved.
5  *
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.
9  */
10
11 /**
12     Hamlet input file.
13
14     This file defines the Barrelfish capability type system.
15
16     (Meta-)Comments about the syntax are enclosed between /** ... **/
17     Comments of the Hamlet language are enclosed between /* ... */
18 **/
19
20 /** We can define some constants using the "define" construct **/
21
22 /* XXX: these must match the corresponding OBJBITS definitions in
23  * barrelfish_kpi/capabilities.h */
24
25 /* Size of L2 CNode: L2 resolves 8 bits of Cap address space */
26 define objsize_l2cnode 16384;
27 /* Size of DCB: */
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
37 /**
38     The capabilities of the whole system are listed thereafter.
39     The minimal definition consists of a name and an empty body.
40 **/
41
42 cap Null is_never_copy {
43     /* Null/invalid object type */
44 };
45
46 cap Memory abstract {
47     /**
48       For a populated cap, we need to give the type and name of each
49       of its fields, such as:
50       "genpaddr base;" for instance
51
52       In order to implement various comparisons, we need to specify a address
53       and size for each type that is backed by memory. The size may be
54       specified directly with "size" or as "size_bits".
55
56       Additional equality fields can be specified with an "eq" prefix, as in
57       "eq genpaddr base;"
58     **/
59
60     address genpaddr base;  /* Physical base address of Memory object */
61     pasid pasid;            /* Physical Address Space ID */
62     size gensize bytes;     /* Size of region in bytes */
63 };
64
65
66
67 /* Physical address range (root of cap tree) */
68 cap PhysAddr from_self inherit Memory;
69
70 cap Mapping abstract {
71     "struct capability" cap;
72     eq lvaddr pte;
73     uint32 offset;
74     uint16 pte_count;
75
76     address { get_address(cap) };
77 };
78
79 cap VNode abstract {
80     address genpaddr base;  /* Base address of VNode */
81     size { objsize_vnode };
82 };
83
84 /** The following caps are similar to the previous one **/
85
86 /* RAM memory object */
87 cap RAM from PhysAddr from_self inherit Memory;
88
89 /* Abstract CNode, need to define size */
90 cap CNode abstract {
91     address lpaddr cnode;               /* Base address of CNode */
92     caprights rightsmask;               /* Cap access rights */
93 };
94
95 /* Level 1 CNode table, resizable */
96 cap L1CNode from RAM inherit CNode {
97     size gensize allocated_bytes;       /* Allocated size of L1 CNode in bytes */
98 };
99
100 /* Level 2 CNode table, resolves 8 bits of cap address */
101 cap L2CNode from RAM inherit CNode {
102     size { objsize_l2cnode };                 /* Size of L2 CNode in bytes (16kB) */
103 };
104
105 cap FCNode {
106      /* Foreign CNode capability */
107
108      eq genpaddr cnode;     /* Base address of CNode */
109      eq uint8 bits;         /* Number of bits this CNode resolves */
110      caprights rightsmask;
111      eq coreid core_id;     /* The core the cap is local on */
112      uint8 guard_size;      /* Number of bits in guard */
113      caddr guard;           /* Bitmask already resolved when reaching this CNode */
114 };
115
116 /** Dispatcher is interesting is several ways. **/
117
118 /**
119   XXX: The whole multi_retype stuff is hack in hamlet that should be removed as
120   soon as parts of an object can be retyped individually. -MN
121 **/
122
123 cap Dispatcher from RAM {
124     /* Dispatcher */
125
126     /**
127       The Dispatcher is a special case that can be retyped several
128       times to an end-point
129     **/
130     /** Note: This must be the first statement */
131     can_retype_multiple;
132
133     /**
134       We allow the use of unknow structures. However, equality will
135       be defined by address, not by structure.
136     **/
137     "struct dcb" dcb;       /* Pointer to kernel DCB */
138
139     address { mem_to_phys(dcb) };
140     size { objsize_dispatcher };
141 };
142
143 cap EndPoint from Dispatcher {
144     /* IDC endpoint */
145
146     "struct dcb" listener;  /* Dispatcher listening on this endpoint */
147     lvaddr epoffset;        /* Offset of endpoint buffer in disp frame */
148     uint32 epbuflen;        /* Length of endpoint buffer in words */
149
150     address { mem_to_phys(listener) };
151
152     /** XXX
153        Preferable definitions for address and size would be as below. These
154        should be used as soon as the whole multi retype hack stuff is fixed:
155
156        address { mem_to_phys(listener + epoffset) };
157        size { epbuflen };
158
159        -MN
160     **/
161 };
162
163 /** Then, we go back to routine **/
164
165 cap Frame from RAM from_self inherit Memory;
166
167 cap Frame_Mapping from Frame inherit Mapping;
168
169 cap DevFrame from PhysAddr from_self inherit Memory;
170
171 cap DevFrame_Mapping from DevFrame inherit Mapping;
172
173 cap Kernel is_always_copy {
174     /* Capability to a kernel */
175 };
176
177
178 /* x86_64-specific capabilities: */
179
180 /* PML4 */
181 cap VNode_x86_64_pml4 from RAM inherit VNode;
182
183 cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping;
184
185 /* PDPT */
186 cap VNode_x86_64_pdpt from RAM inherit VNode;
187
188 cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping;
189
190 /* Page directory */
191 cap VNode_x86_64_pdir from RAM inherit VNode;
192
193 cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping;
194
195 /* Page table */
196 cap VNode_x86_64_ptable from RAM inherit VNode;
197
198 cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping;
199
200
201 /* x86_32-specific capabilities: */
202
203 /* PDPT */
204 cap VNode_x86_32_pdpt from RAM inherit VNode;
205
206 cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping;
207
208 /* Page directory */
209 cap VNode_x86_32_pdir from RAM inherit VNode;
210
211 cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping;
212
213 /* Page table */
214 cap VNode_x86_32_ptable from RAM inherit VNode;
215
216 cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping;
217
218 /* ARM specific capabilities: */
219
220 /* L1 Page Table */
221 cap VNode_ARM_l1 from RAM inherit VNode {
222     size { objsize_vnode_arm_l1 };
223 };
224
225 cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping;
226
227 /* L2 Page Table */
228 cap VNode_ARM_l2 from RAM inherit VNode {
229     size { objsize_vnode_arm_l2 };
230 };
231
232 cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping;
233
234 /* ARM AArch64-specific capabilities: */
235
236 /* L0 Page Table */
237 cap VNode_AARCH64_l0 from RAM inherit VNode;
238
239 cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping;
240
241 /* L1 Page Table */
242 cap VNode_AARCH64_l1 from RAM inherit VNode;
243
244 cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping;
245
246 /* L2 Page Table */
247 cap VNode_AARCH64_l2 from RAM inherit VNode;
248
249 cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping;
250
251 /* L3 Page Table */
252 cap VNode_AARCH64_l3 from RAM inherit VNode;
253
254 cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping;
255
256 /** IRQTable and IO are slightly different **/
257
258 cap IRQTable is_always_copy {
259     /* IRQ Routing table */
260     /**
261        When testing two IRQTable caps for is_copy, we always return True: all
262        IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort
263        of.
264     **/
265 };
266
267 cap IRQDest {
268         /* IRQ Destination capability.
269        Represents a slot in a CPUs int vector table.
270        Can be connected to a LMP endpoint to recv this interrupt. */
271     eq uint64 cpu;
272     eq uint64 vector;
273 };
274
275 cap IRQSrc from_self {
276         /* IRQ Source capability.
277        Represents an interrupt source. It contains a range of interrupt
278        source numbers. */ 
279         eq uint64 vec_start;
280         eq uint64 vec_end;
281 };
282
283 cap IO {
284     /* Legacy IO capability */
285     eq uint16 start;
286     eq uint16 end;          /* Granted IO range */
287 };
288
289 /* IPI notify caps */
290 cap Notify_IPI {
291     eq coreid coreid;
292     eq uint16 chanid;
293 };
294
295 /* ID capability, system-wide unique */
296 cap ID {
297     eq coreid coreid; /* core cap was created */
298     eq uint32 core_local_id; /* per core unique id */
299 };
300
301 cap PerfMon is_always_copy {
302 };
303
304 /** KernelControlBlock represents a struct kcb which contains all the pointers
305  *  to core-local global state of the kernel.
306  **/
307 cap KernelControlBlock from RAM {
308     "struct kcb" kcb;
309
310     address { mem_to_phys(kcb) };
311     /* base page size for now so we can map the kcb in boot driver */
312     size { objsize_kcb };
313 };
314
315 cap IPI is_always_copy {};