/* * Copyright (c) 2009, 2010, 2012, 2015, 2016, ETH Zurich. * Copyright (c) 2015, 2016 Hewlett Packard Enterprise Development LP. * All rights reserved. * * This file is distributed under the terms in the attached LICENSE file. * If you do not find this file, copies can be found by writing to: * ETH Zurich D-INFK, Universitaetstrasse 6, CH-8092 Zurich. Attn: Systems Group. */ /** Hamlet input file. This file defines the Barrelfish capability type system. (Meta-)Comments about the syntax are enclosed between /** ... **/ Comments of the Hamlet language are enclosed between /* ... */ **/ /** We can define some constants using the "define" construct **/ /* XXX: these must match the corresponding OBJBITS definitions in * barrelfish_kpi/capabilities.h */ /* Size of L2 CNode: L2 resolves 8 bits of Cap address space */ define objsize_l2cnode 16384; /* Size of DCB: */ define objsize_dispatcher 1024; /* Size of (x86_64) VNode: */ define objsize_vnode 4096; /* BASE_PAGE_SIZE */ /* Size of ARMv7 VNodes */ define objsize_vnode_arm_l1 16384; define objsize_vnode_arm_l2 1024; /* size of a kernel control block */ define objsize_kcb 131072; /* 128*1024, OBJSIZE_KCB */ /* size of a mapping cap: * if mappings are zero-sized they mess up range queries */ define objsize_mapping 1; /** The capabilities of the whole system are listed thereafter. The minimal definition consists of a name and an empty body. **/ cap Null is_never_copy { /* Null/invalid object type */ }; cap Memory abstract { /** For a populated cap, we need to give the type and name of each of its fields, such as: "genpaddr base;" for instance In order to implement various comparisons, we need to specify a address and size for each type that is backed by memory. The size may be specified directly with "size" or as "size_bits". Additional equality fields can be specified with an "eq" prefix, as in "eq genpaddr base;" **/ address genpaddr base; /* Physical base address of Memory object */ size gensize bytes; /* Size of region in bytes */ pasid pasid; /* Physical Address Space ID */ }; /* Physical address range (root of cap tree) */ cap PhysAddr from_self inherit Memory; cap Mapping abstract { "struct capability" cap; eq "struct cte" ptable; /* We currently never use the offset into the source capability, so remove * it to make room for a more expressive way of referring to the pte */ /* uint32 offset; */ eq uint16 entry; uint16 pte_count; address { get_address(cap) }; size { objsize_mapping }; }; cap VNode abstract { address genpaddr base; /* Base address of VNode */ size { objsize_vnode }; }; /** The following caps are similar to the previous one **/ /* RAM memory object */ cap RAM from PhysAddr from_self inherit Memory; /* Abstract CNode, need to define size */ cap CNode abstract { address lpaddr cnode; /* Base address of CNode */ caprights rightsmask; /* Cap access rights */ }; /* Level 1 CNode table, resizable */ cap L1CNode from RAM inherit CNode { size gensize allocated_bytes; /* Allocated size of L1 CNode in bytes */ }; /* Level 2 CNode table, resolves 8 bits of cap address */ cap L2CNode from RAM inherit CNode { size { objsize_l2cnode }; /* Size of L2 CNode in bytes (16kB) */ }; cap FCNode { /* Foreign CNode capability */ eq genpaddr cnode; /* Base address of CNode */ eq uint8 bits; /* Number of bits this CNode resolves */ caprights rightsmask; eq coreid core_id; /* The core the cap is local on */ uint8 guard_size; /* Number of bits in guard */ caddr guard; /* Bitmask already resolved when reaching this CNode */ }; /** Dispatcher is interesting is several ways. **/ /** XXX: The whole multi_retype stuff is hack in hamlet that should be removed as soon as parts of an object can be retyped individually. -MN **/ cap Dispatcher from RAM { /* Dispatcher */ /** The Dispatcher is a special case that can be retyped several times to an end-point **/ /** Note: This must be the first statement */ can_retype_multiple; /** We allow the use of unknow structures. However, equality will be defined by address, not by structure. **/ "struct dcb" dcb; /* Pointer to kernel DCB */ address { mem_to_phys(dcb) }; size { objsize_dispatcher }; }; cap EndPointLMP from Dispatcher { /* IDC endpoint */ "struct dcb" listener; /* Dispatcher listening on this endpoint */ lvaddr epoffset; /* Offset of endpoint buffer in disp frame */ uint32 epbuflen; /* Length of endpoint buffer in words */ uint16 iftype; /* interface of the endpoint */ address { mem_to_phys(listener) }; /** XXX Preferable definitions for address and size would be as below. These should be used as soon as the whole multi retype hack stuff is fixed: address { mem_to_phys(listener + epoffset) }; size { epbuflen }; -MN **/ }; /** Then, we go back to routine **/ cap Frame from RAM from_self inherit Memory; cap Frame_Mapping from Frame inherit Mapping; cap EndPointUMP from RAM inherit Memory { uint16 iftype; }; cap EndPointUMP_Mapping from EndpointUMP inherit Mapping; cap DevFrame from PhysAddr from_self inherit Memory; cap DevFrame_Mapping from DevFrame inherit Mapping; cap Kernel is_always_copy { /* Capability to a kernel */ }; /* x86_64-specific capabilities: */ /* PML5 */ cap VNode_x86_64_pml5 from RAM inherit VNode; cap VNode_x86_64_pml5_Mapping from VNode_x86_64_pml5 inherit Mapping; /* PML4 */ cap VNode_x86_64_pml4 from RAM inherit VNode; cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping; /* PDPT */ cap VNode_x86_64_pdpt from RAM inherit VNode; cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping; /* Page directory */ cap VNode_x86_64_pdir from RAM inherit VNode; cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping; /* Page table */ cap VNode_x86_64_ptable from RAM inherit VNode; cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping; /* Extended page table types for x86 nested paging */ cap VNode_x86_64_ept_pml4 from RAM inherit VNode; cap VNode_x86_64_ept_pml4_Mapping from VNode_x86_64_ept_pml4 inherit Mapping; cap VNode_x86_64_ept_pdpt from RAM inherit VNode; cap VNode_x86_64_ept_pdpt_Mapping from VNode_x86_64_ept_pdpt inherit Mapping; cap VNode_x86_64_ept_pdir from RAM inherit VNode; cap VNode_x86_64_ept_pdir_Mapping from VNode_x86_64_ept_pdir inherit Mapping; cap VNode_x86_64_ept_ptable from RAM inherit VNode; cap VNode_x86_64_ept_ptable_Mapping from VNode_x86_64_ept_ptable inherit Mapping; /* Intel VT-d */ cap VNode_VTd_root_table from RAM inherit VNode; cap VNode_VTd_root_table_Mapping from VNode_VTd_root_table inherit Mapping; cap VNode_VTd_ctxt_table from RAM inherit VNode; cap VNode_VTd_ctxt_table_Mapping from VNode_VTd_ctxt_table inherit Mapping; /* cap IntelVTd from PhysAddr from_self inherit Memory; */ /* x86_32-specific capabilities: */ /* PDPT */ cap VNode_x86_32_pdpt from RAM inherit VNode; cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping; /* Page directory */ cap VNode_x86_32_pdir from RAM inherit VNode; cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping; /* Page table */ cap VNode_x86_32_ptable from RAM inherit VNode; cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping; /* ARM specific capabilities: */ /* L1 Page Table */ cap VNode_ARM_l1 from RAM inherit VNode { size { objsize_vnode_arm_l1 }; }; cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping; /* L2 Page Table */ cap VNode_ARM_l2 from RAM inherit VNode { size { objsize_vnode_arm_l2 }; }; cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping; /* ARM AArch64-specific capabilities: */ /* L0 Page Table */ cap VNode_AARCH64_l0 from RAM inherit VNode; cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping; /* L1 Page Table */ cap VNode_AARCH64_l1 from RAM inherit VNode; cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping; /* L2 Page Table */ cap VNode_AARCH64_l2 from RAM inherit VNode; cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping; /* L3 Page Table */ cap VNode_AARCH64_l3 from RAM inherit VNode; cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping; /** IRQTable and IO are slightly different **/ cap IRQTable is_always_copy { /* IRQ Routing table */ /** When testing two IRQTable caps for is_copy, we always return True: all IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort of. **/ }; cap IRQDest { /* IRQ Destination capability. Represents a slot in a CPUs int vector table. Can be connected to a LMP endpoint to recv this interrupt. */ eq uint64 cpu; eq uint64 vector; }; cap IRQSrc from_self { /* IRQ Source capability. Represents an interrupt source. It contains a range of interrupt source numbers. */ eq uint64 vec_start; eq uint64 vec_end; }; cap IO { /* Legacy IO capability */ eq uint16 start; eq uint16 end; /* Granted IO range */ }; /* IPI notify caps */ cap Notify_IPI { eq coreid coreid; eq uint16 chanid; }; /* ID capability, system-wide unique */ cap ID { eq coreid coreid; /* core cap was created */ eq uint32 core_local_id; /* per core unique id */ }; cap PerfMon is_always_copy { }; /** KernelControlBlock represents a struct kcb which contains all the pointers * to core-local global state of the kernel. **/ cap KernelControlBlock from RAM { "struct kcb" kcb; address { mem_to_phys(kcb) }; /* base page size for now so we can map the kcb in boot driver */ size { objsize_kcb }; }; cap IPI is_always_copy {}; cap ProcessManager is_always_copy { // Capability to act as process manager, i.e. create new domain caps. }; cap Domain from ProcessManager { eq coreid coreid; /* Core where the domain was created. */ eq uint32 core_local_id; /* Core-local ID of the domain. */ }; /* cap ProtectionDomainManager is_always_copy { // Capability to act as device manager, i.e. create new device id caps }; cap ProtectionDomain from IOMMUDomainManager { uint16 id; uint16 type }; */ cap DeviceIDManager is_always_copy { // Capability to act as device manager, i.e. create new device id caps }; cap DeviceID from DeviceIDManager { uint16 segment; uint8 bus; uint8 device; uint8 function; uint8 type; uint16 flags; };