389 lines
11 KiB
Plaintext
389 lines
11 KiB
Plaintext
/*
|
|
* 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;
|
|
};
|