kernel: do not drop RAM caps
[barrelfish] / capabilities / caps.hl
1 /*
2  * Copyright (c) 2009, 2010, 2012, ETH Zurich.
3  * All rights reserved.
4  *
5  * This file is distributed under the terms in the attached LICENSE file.
6  * If you do not find this file, copies can be found by writing to:
7  * ETH Zurich D-INFK, Haldeneggsteig 4, CH-8092 Zurich. Attn: Systems Group.
8  */
9
10 /**
11     Hamlet input file.
12
13     This file defines the Barrelfish capability type system.
14
15     (Meta-)Comments about the syntax are enclosed between /** ... **/
16     Comments of the Hamlet language are enclosed between /* ... */
17 **/
18
19 /** We can define some constants using the "define" construct **/
20
21 /* XXX: these must match the corresponding OBJBITS definitions in barrelfish_kpi/capabilities.h */
22
23 /* Size of CNode entry: */
24 define cte_size 7;
25 /* Size of DCB: */
26 define dispatcher_size 10;
27 /* Size of (x86_64) VNode: */
28 define vnode_size 12; /* BASE_PAGE_BITS */
29 /* size of a kernel control block */
30 define kcb_size 16; /* OBJBITS_KCB */
31
32 /**
33     The capabilities of the whole system are listed thereafter.
34     The minimal definition consists of a name and an empty body.
35 **/
36
37 cap Null is_never_copy {
38     /* Null/invalid object type */
39 };
40
41 cap PhysAddr from_self {
42     /* Physical address range (root of cap tree) */
43
44     /**
45       For a populated cap, we need to give the type and name of each
46       of its fields, such as:
47       "genpaddr base;" for instance
48
49       In order to implement various comparisons, we need to specify a address
50       and size for each type that is backed by memory. The size may be
51       specified directly with "size" or as "size_bits".
52
53       Additional equality fields can be specified with an "eq" prefix, as in
54       "eq genpaddr base;"
55     **/
56
57     address genpaddr base;  /* Base address of untyped region */
58     size_bits uint8 bits;   /* Address bits that untyped region bears */
59
60 };
61
62 /** The following caps are similar to the previous one **/
63
64 cap RAM from PhysAddr from_self {
65     /* RAM memory object */
66
67     address genpaddr base;  /* Base address of untyped region */
68     size_bits uint8 bits; /* Address bits that untyped region bears */
69
70 };
71
72 cap CNode from RAM {
73     /* CNode table, stores further capabilities */
74
75     lpaddr cnode;           /* Base address of CNode */
76     uint8 bits;             /* Number of bits this CNode resolves */
77     caprights rightsmask;
78     uint8 guard_size;       /* Number of bits in guard */
79     caddr guard;            /* Bitmask already resolved when reaching this CNode */
80
81     /**
82       Address and size may also be specified with some very limited
83       expressions.
84     **/
85
86     /* Shouldn't this be mem_to_phys(cnode)? (causes breakage) -MN */
87     address { cnode };
88     size_bits { bits + cte_size };
89
90 };
91
92 cap FCNode {
93      /* Foreign CNode capability */
94
95      eq genpaddr cnode;     /* Base address of CNode */
96      eq uint8 bits;         /* Number of bits this CNode resolves */
97      caprights rightsmask;
98      eq coreid core_id;     /* The core the cap is local on */
99      uint8 guard_size;      /* Number of bits in guard */
100      caddr guard;           /* Bitmask already resolved when reaching this CNode */
101 };
102
103 /** Dispatcher is interesting is several ways. **/
104
105 /**
106   XXX: The whole multi_retype stuff is hack in hamlet that should be removed as
107   soon as parts of an object can be retyped individually. -MN
108 **/
109
110 cap Dispatcher from RAM {
111     /* Dispatcher */
112
113     /**
114       The Dispatcher is a special case that can be retyped several
115       times to an end-point
116     **/
117     /** Note: This must be the first statement */
118     can_retype_multiple;
119
120     /**
121       We allow the use of unknow structures. However, equality will
122       be defined by address, not by structure.
123     **/
124     "struct dcb" dcb;       /* Pointer to kernel DCB */
125
126     address { mem_to_phys(dcb) };
127     size_bits { dispatcher_size };
128 };
129
130 cap EndPoint from Dispatcher {
131     /* IDC endpoint */
132
133     "struct dcb" listener;  /* Dispatcher listening on this endpoint */
134     lvaddr epoffset;        /* Offset of endpoint buffer in disp frame */
135     uint32 epbuflen;        /* Length of endpoint buffer in words */
136
137     address { mem_to_phys(listener) };
138
139     /** XXX
140        Preferable definitions for address and size would be as below. These
141        should be used as soon as the whole multi retype hack stuff is fixed:
142
143        address { mem_to_phys(listener + epoffset) };
144        size { epbuflen };
145
146        -MN
147     **/
148 };
149
150 /** Then, we go back to routine **/
151
152 cap Frame from RAM from_self {
153     /* Mappable memory frame */
154
155     address genpaddr base;  /* Physical base address of frame */
156     size_bits uint8 bits;      /* Address bits this frame bears */
157 };
158
159 cap DevFrame from PhysAddr from_self {
160     /* Mappable device frame */
161
162     address genpaddr base;  /* Physical base address of frame */
163     size_bits uint8 bits;      /* Address bits this frame bears */
164 };
165
166
167 cap Kernel is_always_copy {
168     /* Capability to a kernel */
169 };
170
171
172
173 /* x86_64-specific capabilities: */
174
175 cap VNode_x86_64_pml4 from RAM {
176     /* PML4 */
177
178     address genpaddr base;  /* Base address of VNode */
179     size_bits { vnode_size };
180 };
181
182 cap VNode_x86_64_pdpt from RAM {
183     /* PDPT */
184
185     address genpaddr base;  /* Base address of VNode */
186     size_bits { vnode_size };
187 };
188
189 cap VNode_x86_64_pdir from RAM {
190     /* Page directory */
191
192     address genpaddr base;  /* Base address of VNode */
193     size_bits { vnode_size };
194 };
195
196 cap VNode_x86_64_ptable from RAM {
197     /* Page table */
198
199     address genpaddr base;  /* Base address of VNode */
200     size_bits { vnode_size };
201 };
202
203
204 /* x86_32-specific capabilities: */
205
206 cap VNode_x86_32_pdpt from RAM {
207     /* PDPT */
208
209     address genpaddr base;  /* Base address of VNode */
210     size_bits { vnode_size };
211 };
212
213 cap VNode_x86_32_pdir from RAM {
214     /* Page directory */
215
216     address genpaddr base;  /* Base address of VNode */
217     size_bits { vnode_size };
218 };
219
220 cap VNode_x86_32_ptable from RAM {
221     /* Page table */
222
223     address genpaddr base;  /* Base address of VNode */
224     size_bits { vnode_size };
225 };
226
227 /* ARM specific capabilities: */
228
229 cap VNode_ARM_l1 from RAM {
230     /* L1 Page Table */
231
232     address genpaddr base;  /* Base address of VNode */
233     size_bits { vnode_size };
234 };
235
236 cap VNode_ARM_l2 from RAM {
237     /* L2 Page Table */
238     address genpaddr base;  /* Base address of VNode */
239     size_bits { vnode_size };
240 };
241
242 /** IRQTable and IO are slightly different **/
243
244 cap IRQTable is_always_copy {
245     /* IRQ Routing table */
246     /**
247        When testing two IRQTable caps for is_copy, we always return True: all
248        IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort
249        of.
250     **/
251 };
252
253 cap IO {
254     /* Legacy IO capability */
255     eq uint16 start;
256     eq uint16 end;          /* Granted IO range */
257 };
258
259 /* really RCK notify caps */
260 cap Notify_RCK {
261     eq coreid coreid;
262     eq uint16 chanid;
263 };
264
265 /* IPI notify caps */
266 cap Notify_IPI {
267     eq coreid coreid;
268     eq uint16 chanid;
269 };
270
271 /* ID capability, system-wide unique */
272 cap ID {
273     eq coreid coreid; /* core cap was created */
274     eq uint32 core_local_id; /* per core unique id */
275 };
276
277 cap PerfMon is_always_copy {
278 };
279
280 /** KernelControlBlock represents a struct kcb which contains all the pointers
281  *  to core-local global state of the kernel.
282  **/
283 cap KernelControlBlock from RAM {
284     "struct kcb" kcb;
285
286     address { mem_to_phys(kcb) };
287     /* base page size for now so we can map the kcb in boot driver */
288     size_bits { kcb_size };
289 };
290
291 cap IPI is_always_copy {};