git.barrelfish.org Git - barrelfish/blob - 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 /* size of a mapping cap:
  37  * if mappings are zero-sized they mess up range queries */
  38 define objsize_mapping 1;
  39
  40 /**
  41     The capabilities of the whole system are listed thereafter.
  42     The minimal definition consists of a name and an empty body.
  43 **/
  44
  45 cap Null is_never_copy {
  46     /* Null/invalid object type */
  47 };
  48
  49 cap Memory abstract {
  50     /**
  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
  54
  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".
  58
  59       Additional equality fields can be specified with an "eq" prefix, as in
  60       "eq genpaddr base;"
  61     **/
  62
  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 */
  66 };
  67
  68
  69
  70 /* Physical address range (root of cap tree) */
  71 cap PhysAddr from_self inherit Memory;
  72
  73 cap Mapping abstract {
  74     "struct capability" cap;
  75     eq lvaddr pte;
  76     uint32 offset;
  77     uint16 pte_count;
  78
  79     address { get_address(cap) };
  80     size { objsize_mapping };
  81 };
  82
  83 cap VNode abstract {
  84     address genpaddr base;  /* Base address of VNode */
  85     size { objsize_vnode };
  86 };
  87
  88 /** The following caps are similar to the previous one **/
  89
  90 /* RAM memory object */
  91 cap RAM from PhysAddr from_self inherit Memory;
  92
  93 /* Abstract CNode, need to define size */
  94 cap CNode abstract {
  95     address lpaddr cnode;               /* Base address of CNode */
  96     caprights rightsmask;               /* Cap access rights */
  97 };
  98
  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 */
 102 };
 103
 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) */
 107 };
 108
 109 cap FCNode {
 110      /* Foreign CNode capability */
 111
 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 */
 118 };
 119
 120 /** Dispatcher is interesting is several ways. **/
 121
 122 /**
 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
 125 **/
 126
 127 cap Dispatcher from RAM {
 128     /* Dispatcher */
 129
 130     /**
 131       The Dispatcher is a special case that can be retyped several
 132       times to an end-point
 133     **/
 134     /** Note: This must be the first statement */
 135     can_retype_multiple;
 136
 137     /**
 138       We allow the use of unknow structures. However, equality will
 139       be defined by address, not by structure.
 140     **/
 141     "struct dcb" dcb;       /* Pointer to kernel DCB */
 142
 143     address { mem_to_phys(dcb) };
 144     size { objsize_dispatcher };
 145 };
 146
 147 cap EndPoint from Dispatcher {
 148     /* IDC endpoint */
 149
 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 */
 153
 154     address { mem_to_phys(listener) };
 155
 156     /** XXX
 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:
 159
 160        address { mem_to_phys(listener + epoffset) };
 161        size { epbuflen };
 162
 163        -MN
 164     **/
 165 };
 166
 167 /** Then, we go back to routine **/
 168
 169 cap Frame from RAM from_self inherit Memory;
 170
 171 cap Frame_Mapping from Frame inherit Mapping;
 172
 173 cap DevFrame from PhysAddr from_self inherit Memory;
 174
 175 cap DevFrame_Mapping from DevFrame inherit Mapping;
 176
 177 cap Kernel is_always_copy {
 178     /* Capability to a kernel */
 179 };
 180
 181
 182 /* x86_64-specific capabilities: */
 183
 184 /* PML4 */
 185 cap VNode_x86_64_pml4 from RAM inherit VNode;
 186
 187 cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping;
 188
 189 /* PDPT */
 190 cap VNode_x86_64_pdpt from RAM inherit VNode;
 191
 192 cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping;
 193
 194 /* Page directory */
 195 cap VNode_x86_64_pdir from RAM inherit VNode;
 196
 197 cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping;
 198
 199 /* Page table */
 200 cap VNode_x86_64_ptable from RAM inherit VNode;
 201
 202 cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping;
 203
 204
 205 /* x86_32-specific capabilities: */
 206
 207 /* PDPT */
 208 cap VNode_x86_32_pdpt from RAM inherit VNode;
 209
 210 cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping;
 211
 212 /* Page directory */
 213 cap VNode_x86_32_pdir from RAM inherit VNode;
 214
 215 cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping;
 216
 217 /* Page table */
 218 cap VNode_x86_32_ptable from RAM inherit VNode;
 219
 220 cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping;
 221
 222 /* ARM specific capabilities: */
 223
 224 /* L1 Page Table */
 225 cap VNode_ARM_l1 from RAM inherit VNode {
 226     size { objsize_vnode_arm_l1 };
 227 };
 228
 229 cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping;
 230
 231 /* L2 Page Table */
 232 cap VNode_ARM_l2 from RAM inherit VNode {
 233     size { objsize_vnode_arm_l2 };
 234 };
 235
 236 cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping;
 237
 238 /* ARM AArch64-specific capabilities: */
 239
 240 /* L0 Page Table */
 241 cap VNode_AARCH64_l0 from RAM inherit VNode;
 242
 243 cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping;
 244
 245 /* L1 Page Table */
 246 cap VNode_AARCH64_l1 from RAM inherit VNode;
 247
 248 cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping;
 249
 250 /* L2 Page Table */
 251 cap VNode_AARCH64_l2 from RAM inherit VNode;
 252
 253 cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping;
 254
 255 /* L3 Page Table */
 256 cap VNode_AARCH64_l3 from RAM inherit VNode;
 257
 258 cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping;
 259
 260 /** IRQTable and IO are slightly different **/
 261
 262 cap IRQTable is_always_copy {
 263     /* IRQ Routing table */
 264     /**
 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
 267        of.
 268     **/
 269 };
 270
 271 cap IRQDest {
 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. */
 275     eq uint64 cpu;
 276     eq uint64 vector;
 277 };
 278
 279 cap IRQSrc from_self {
 280         /* IRQ Source capability.
 281        Represents an interrupt source. It contains a range of interrupt
 282        source numbers. */
 283         eq uint64 vec_start;
 284         eq uint64 vec_end;
 285 };
 286
 287 cap IO {
 288     /* Legacy IO capability */
 289     eq uint16 start;
 290     eq uint16 end;          /* Granted IO range */
 291 };
 292
 293 /* IPI notify caps */
 294 cap Notify_IPI {
 295     eq coreid coreid;
 296     eq uint16 chanid;
 297 };
 298
 299 /* ID capability, system-wide unique */
 300 cap ID {
 301     eq coreid coreid; /* core cap was created */
 302     eq uint32 core_local_id; /* per core unique id */
 303 };
 304
 305 cap PerfMon is_always_copy {
 306 };
 307
 308 /** KernelControlBlock represents a struct kcb which contains all the pointers
 309  *  to core-local global state of the kernel.
 310  **/
 311 cap KernelControlBlock from RAM {
 312     "struct kcb" kcb;
 313
 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 };
 317 };
 318
 319 cap IPI is_always_copy {};