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
  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 {};