git.barrelfish.org Git - barrelfish/blob - 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 {};