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 */ 26define objsize_l2cnode 16384; 27/* Size of DCB: */ 28define objsize_dispatcher 1024; 29/* Size of (x86_64) VNode: */ 30define objsize_vnode 4096; /* BASE_PAGE_SIZE */ 31/* Size of ARMv7 VNodes */ 32define objsize_vnode_arm_l1 16384; 33define objsize_vnode_arm_l2 1024; 34/* size of a kernel control block */ 35define objsize_kcb 65536; /* OBJSIZE_KCB */ 36/* size of a mapping cap: 37 * if mappings are zero-sized they mess up range queries */ 38define 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 45cap Null is_never_copy { 46 /* Null/invalid object type */ 47}; 48 49cap 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) */ 71cap PhysAddr from_self inherit Memory; 72 73cap Mapping abstract { 74 "struct capability" cap; 75 eq "struct cte" ptable; 76 /* We currently never use the offset into the source capability, so remove 77 * it to make room for a more expressive way of referring to the pte */ 78 /* uint32 offset; */ 79 eq uint16 entry; 80 uint16 pte_count; 81 82 address { get_address(cap) }; 83 size { objsize_mapping }; 84}; 85 86cap VNode abstract { 87 address genpaddr base; /* Base address of VNode */ 88 size { objsize_vnode }; 89}; 90 91/** The following caps are similar to the previous one **/ 92 93/* RAM memory object */ 94cap RAM from PhysAddr from_self inherit Memory; 95 96/* Abstract CNode, need to define size */ 97cap CNode abstract { 98 address lpaddr cnode; /* Base address of CNode */ 99 caprights rightsmask; /* Cap access rights */ 100}; 101 102/* Level 1 CNode table, resizable */ 103cap L1CNode from RAM inherit CNode { 104 size gensize allocated_bytes; /* Allocated size of L1 CNode in bytes */ 105}; 106 107/* Level 2 CNode table, resolves 8 bits of cap address */ 108cap L2CNode from RAM inherit CNode { 109 size { objsize_l2cnode }; /* Size of L2 CNode in bytes (16kB) */ 110}; 111 112cap FCNode { 113 /* Foreign CNode capability */ 114 115 eq genpaddr cnode; /* Base address of CNode */ 116 eq uint8 bits; /* Number of bits this CNode resolves */ 117 caprights rightsmask; 118 eq coreid core_id; /* The core the cap is local on */ 119 uint8 guard_size; /* Number of bits in guard */ 120 caddr guard; /* Bitmask already resolved when reaching this CNode */ 121}; 122 123/** Dispatcher is interesting is several ways. **/ 124 125/** 126 XXX: The whole multi_retype stuff is hack in hamlet that should be removed as 127 soon as parts of an object can be retyped individually. -MN 128**/ 129 130cap Dispatcher from RAM { 131 /* Dispatcher */ 132 133 /** 134 The Dispatcher is a special case that can be retyped several 135 times to an end-point 136 **/ 137 /** Note: This must be the first statement */ 138 can_retype_multiple; 139 140 /** 141 We allow the use of unknow structures. However, equality will 142 be defined by address, not by structure. 143 **/ 144 "struct dcb" dcb; /* Pointer to kernel DCB */ 145 146 address { mem_to_phys(dcb) }; 147 size { objsize_dispatcher }; 148}; 149 150cap EndPoint from Dispatcher { 151 /* IDC endpoint */ 152 153 "struct dcb" listener; /* Dispatcher listening on this endpoint */ 154 lvaddr epoffset; /* Offset of endpoint buffer in disp frame */ 155 uint32 epbuflen; /* Length of endpoint buffer in words */ 156 157 address { mem_to_phys(listener) }; 158 159 /** XXX 160 Preferable definitions for address and size would be as below. These 161 should be used as soon as the whole multi retype hack stuff is fixed: 162 163 address { mem_to_phys(listener + epoffset) }; 164 size { epbuflen }; 165 166 -MN 167 **/ 168}; 169 170/** Then, we go back to routine **/ 171 172cap Frame from RAM from_self inherit Memory; 173 174cap Frame_Mapping from Frame inherit Mapping; 175 176cap DevFrame from PhysAddr from_self inherit Memory; 177 178cap DevFrame_Mapping from DevFrame inherit Mapping; 179 180cap Kernel is_always_copy { 181 /* Capability to a kernel */ 182}; 183 184 185/* x86_64-specific capabilities: */ 186 187/* PML4 */ 188cap VNode_x86_64_pml4 from RAM inherit VNode; 189 190cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping; 191 192/* PDPT */ 193cap VNode_x86_64_pdpt from RAM inherit VNode; 194 195cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping; 196 197/* Page directory */ 198cap VNode_x86_64_pdir from RAM inherit VNode; 199 200cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping; 201 202/* Page table */ 203cap VNode_x86_64_ptable from RAM inherit VNode; 204 205cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping; 206 207 208/* x86_32-specific capabilities: */ 209 210/* PDPT */ 211cap VNode_x86_32_pdpt from RAM inherit VNode; 212 213cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping; 214 215/* Page directory */ 216cap VNode_x86_32_pdir from RAM inherit VNode; 217 218cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping; 219 220/* Page table */ 221cap VNode_x86_32_ptable from RAM inherit VNode; 222 223cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping; 224 225/* ARM specific capabilities: */ 226 227/* L1 Page Table */ 228cap VNode_ARM_l1 from RAM inherit VNode { 229 size { objsize_vnode_arm_l1 }; 230}; 231 232cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping; 233 234/* L2 Page Table */ 235cap VNode_ARM_l2 from RAM inherit VNode { 236 size { objsize_vnode_arm_l2 }; 237}; 238 239cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping; 240 241/* ARM AArch64-specific capabilities: */ 242 243/* L0 Page Table */ 244cap VNode_AARCH64_l0 from RAM inherit VNode; 245 246cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping; 247 248/* L1 Page Table */ 249cap VNode_AARCH64_l1 from RAM inherit VNode; 250 251cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping; 252 253/* L2 Page Table */ 254cap VNode_AARCH64_l2 from RAM inherit VNode; 255 256cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping; 257 258/* L3 Page Table */ 259cap VNode_AARCH64_l3 from RAM inherit VNode; 260 261cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping; 262 263/** IRQTable and IO are slightly different **/ 264 265cap IRQTable is_always_copy { 266 /* IRQ Routing table */ 267 /** 268 When testing two IRQTable caps for is_copy, we always return True: all 269 IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort 270 of. 271 **/ 272}; 273 274cap IRQDest { 275 /* IRQ Destination capability. 276 Represents a slot in a CPUs int vector table. 277 Can be connected to a LMP endpoint to recv this interrupt. */ 278 eq uint64 cpu; 279 eq uint64 vector; 280}; 281 282cap IRQSrc from_self { 283 /* IRQ Source capability. 284 Represents an interrupt source. It contains a range of interrupt 285 source numbers. */ 286 eq uint64 vec_start; 287 eq uint64 vec_end; 288}; 289 290cap IO { 291 /* Legacy IO capability */ 292 eq uint16 start; 293 eq uint16 end; /* Granted IO range */ 294}; 295 296/* IPI notify caps */ 297cap Notify_IPI { 298 eq coreid coreid; 299 eq uint16 chanid; 300}; 301 302/* ID capability, system-wide unique */ 303cap ID { 304 eq coreid coreid; /* core cap was created */ 305 eq uint32 core_local_id; /* per core unique id */ 306}; 307 308cap PerfMon is_always_copy { 309}; 310 311/** KernelControlBlock represents a struct kcb which contains all the pointers 312 * to core-local global state of the kernel. 313 **/ 314cap KernelControlBlock from RAM { 315 "struct kcb" kcb; 316 317 address { mem_to_phys(kcb) }; 318 /* base page size for now so we can map the kcb in boot driver */ 319 size { objsize_kcb }; 320}; 321 322cap IPI is_always_copy {}; 323 324cap ProcessManager is_always_copy { 325 // Capability to act as process manager, i.e. create new domain caps. 326}; 327 328cap Domain from ProcessManager { 329 eq coreid coreid; /* Core where the domain was created. */ 330 eq uint32 core_local_id; /* Core-local ID of the domain. */ 331};