Updated caps.hl for new hamlet.
authorMark Nevill <nevillm@ethz.ch>
Thu, 19 Jan 2012 21:00:42 +0000 (22:00 +0100)
committerMark Nevill <nevillm@ethz.ch>
Thu, 19 Jan 2012 21:00:42 +0000 (22:00 +0100)
capabilities/caps.hl

index 4fe269b..8672071 100644 (file)
     Comments of the Hamlet language are enclosed between /* ... */
 **/
 
-
-/** cap_raw_word maps to CAP_RAW_WORD,
-    as defined in include/barrelfish/kpi/capabilities.h **/
-
-/* Maximum words in the type-specific part of a capability
-   representation: */
-/* XXX: FIXME: x86-64-specific! */
-param cap_raw_word 3;
-
-
 /** We can define some constants using the "define" construct **/
 
 /* XXX: these must match the corresponding OBJBITS definitions in barrelfish_kpi/capabilities.h */
 
 /* Size of CNode entry: */
-define cnode_size 6;
+define cte_size 6;
 /* Size of DCB: */
 define dispatcher_size 9;
 /* Size of (x86_64) VNode: */
 define vnode_size 12; /* BASE_PAGE_BITS */
 
-/** 
+/**
+   XXX: this is for the Dispatcher/Endpoint hack (see corresponding cap
+   definitions) and should be removed as soon as that is resolved -MN
+**/
+define zero 0;
+
+/**
     The capabilities of the whole system are listed thereafter.
-    The minimal definition consists of a name and an empty body. 
+    The minimal definition consists of a name and an empty body.
 **/
 
-cap Null {
-     /* Null/invalid object type */
-     is_never_copy;
+cap Null is_never_copy {
+    /* Null/invalid object type */
 };
 
-cap PhysAddr {
-     /* Physical address range (root of cap tree) */
-    
-     /**
-       When a cap can *uniquely* retype to others,
-       we specify that using "retype_to".
-
-       This is used to implement "is_well_founded" and
-       "is_revoked_first",
-       in kernel/capabilities.c
-
-       In order to implement "is_ancestor",
-       in kernel/mbc.c,
-       we need to specify which fields of the child caps are to be
-       compared for inclusion. When provided a tuple (base, offset),
-       the formula is:
-       "parent->base >= child->base &&
-        child->base + (1ul << child->offset) <= 
-         parent->base + (1ul << parent->offset)"
-     **/
-     retype_to { 
-        RAM: { base, bits },
-        DevFrame: { base, bits },
-        PhysAddr: { base, bits }
-     };
-
-     /**
-       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 "is_copy", 
-       in kernel/mdb.c,
-       we need to specify which fields are part of the equality
-       relation, using the command:
-       "eq genpaddr base;" for instance
-     **/
-
-     eq genpaddr base; /* Base address of untyped region */
-     eq uint8 bits;    /* Address bits that untyped region bears */
+cap PhysAddr from_self {
+    /* Physical address range (root of cap tree) */
+
+    /**
+      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;  /* Base address of untyped region */
+    size_bits uint8 bits;   /* Address bits that untyped region bears */
 
 };
 
 
 /** The following caps are similar to the previous one **/
 
-cap RAM {
-     /* RAM memory object */
-
-     retype_to {
-         RAM: { base, bits },
-        Frame: { base, bits },
-        Dispatcher: { mem_to_phys(dcb), dispatcher_size },
-        CNode: { cnode, cnode_size + bits }, 
-        VNode_x86_64_pml4: { base, vnode_size },
-        VNode_x86_64_pdpt: { base, vnode_size },
-        VNode_x86_64_pdir: { base, vnode_size },
-        VNode_x86_64_ptable: { base, vnode_size },
-        VNode_x86_32_pdpt: { base, vnode_size },
-        VNode_x86_32_pdir: { base, vnode_size },
-        VNode_x86_32_ptable: { base, vnode_size },
-        VNode_ARM_l1:      { base, vnode_size },
-        VNode_ARM_l2:      { base, vnode_size }
-     };
-
-     eq genpaddr base; /* Base address of untyped region */
-     eq uint8 bits;    /* Address bits that untyped region bears */
+cap RAM from PhysAddr from_self {
+    /* RAM memory object */
+
+    address genpaddr base;  /* Base address of untyped region */
+    size_bits uint8 bits; /* Address bits that untyped region bears */
+
 };
 
 
-cap CNode {
-     /* CNode table, stores further capabilities */
+cap CNode from RAM {
+    /* CNode table, stores further capabilities */
 
-     eq lpaddr cnode;  /* Base address of CNode */
-     eq uint8 bits;     /* Number of bits this CNode resolves */
-     caprights rightsmask;
-     uint8 guard_size;  /* Number of bits in guard */
-     caddr guard;       /* Bitmask already resolved when reaching this CNode */
+    lpaddr cnode;           /* Base address of CNode */
+    uint8 bits;             /* Number of bits this CNode resolves */
+    caprights rightsmask;
+    uint8 guard_size;       /* Number of bits in guard */
+    caddr guard;            /* Bitmask already resolved when reaching this CNode */
+
+    /**
+      Address and size may also be specified with some very limited
+      expressions.
+    **/
+
+    address { cnode };
+    size_bits { bits + cte_size };
 
 };
 
 cap FCNode {
      /* Foreign CNode capability */
 
-     eq genpaddr cnode;         /* Base address of CNode */
-     eq uint8 bits;             /* Number of bits this CNode resolves */
+     eq genpaddr cnode;            /* Base address of CNode */
+     eq uint8 bits;                /* Number of bits this CNode resolves */
      caprights rightsmask;
-     eq uint8 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 */
+     eq uint8 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. **/
 
-cap Dispatcher {
-     /* Dispatcher */
+/**
+  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
+**/
 
-     /** 
-       The Dispatcher is a special case that can be retyped several
-       times to an end-point 
+cap Dispatcher from RAM {
+    /* Dispatcher */
 
-       The comparison function for a singleton ptr, the formula is
-       simply:
-       "parent->ptr == child->ptr"
-     **/
+    /**
+      The Dispatcher is a special case that can be retyped several
+      times to an end-point
 
-     retype_multi_to {
-         EndPoint: { listener }
-     };
+      The comparison function for a singleton ptr, the formula is
+      simply:
+      "parent->ptr == child->ptr"
+    **/
+    /** 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.
-     **/
+    /**
+      We allow the use of unknow structures. However, equality will
+      be defined by address, not by structure.
+    **/
 
-     eq "struct dcb" dcb;    /* Pointer to kernel DCB */
+    "struct dcb" dcb;       /* Pointer to kernel DCB */
+
+    address { mem_to_phys(dcb) };
+    size_bits { dispatcher_size };
 };
 
 /** Then, we go back to routine **/
 
-cap EndPoint {
-     /* IDC endpoint */
+cap EndPoint from Dispatcher {
+    /* IDC endpoint */
 
-     eq "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 */
-};
+    "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 */
 
+    address { mem_to_phys(listener) };
+    /* XXX: see note before dispatcher -MN */
+    size { zero };
 
-cap Frame {
-     /* Mappable memory frame */
+    /**
+       preferable definitions for address and size, should be used as soon as
+       the whole multi retype hack stuff is fixed:
 
-     retype_to { 
-         Frame: { base, bits }
-     };
+       address { mem_to_phys(listener + epoffset) };
+       size { epbuflen };
 
-     eq genpaddr base;         /* Physical base address of frame */
-     eq uint8 bits;         /* Address bits this frame bears */
+       -MN
+    **/
 };
 
-cap DevFrame {
-     /* Mappable device frame */
 
-     retype_to { 
-         DevFrame: { base, bits }
-     };
+cap Frame from RAM from_self {
+    /* Mappable memory frame */
+
+    address genpaddr base;  /* Physical base address of frame */
+    size_bits uint8 bits;      /* Address bits this frame bears */
+};
+
+cap DevFrame from PhysAddr from_self {
+    /* Mappable device frame */
 
-     eq genpaddr base;         /* Physical base address of frame */
-     eq uint8 bits;         /* Address bits this frame bears */
+    address genpaddr base;  /* Physical base address of frame */
+    size_bits uint8 bits;      /* Address bits this frame bears */
 };
 
 
-cap Kernel {
-     /* Capability to a kernel */
-    is_always_copy;
+cap Kernel is_always_copy {
+    /* Capability to a kernel */
 };
 
 
 
 /* x86_64-specific capabilities: */
 
-cap VNode_x86_64_pml4 {
-     /* PML4 */
+cap VNode_x86_64_pml4 from RAM {
+    /* PML4 */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
-cap VNode_x86_64_pdpt {
-     /* PDPT */
+cap VNode_x86_64_pdpt from RAM {
+    /* PDPT */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
-cap VNode_x86_64_pdir {
-     /* Page directory */
+cap VNode_x86_64_pdir from RAM {
+    /* Page directory */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
-cap VNode_x86_64_ptable {
-     /* Page table */
+cap VNode_x86_64_ptable from RAM {
+    /* Page table */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
 
 /* x86_32-specific capabilities: */
 
-cap VNode_x86_32_pdpt {
-     /* PDPT */
+cap VNode_x86_32_pdpt from RAM {
+    /* PDPT */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
-cap VNode_x86_32_pdir {
-     /* Page directory */
+cap VNode_x86_32_pdir from RAM {
+    /* Page directory */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
-cap VNode_x86_32_ptable {
-     /* Page table */
+cap VNode_x86_32_ptable from RAM {
+    /* Page table */
 
-     eq genpaddr base;         /* Base address of VNode */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
 /* ARM specific capabilities: */
 
-cap VNode_ARM_l1 {
-     /* L1 Page Table */
-     eq genpaddr base;         /* Base address of VNode */
+cap VNode_ARM_l1 from RAM {
+    /* L1 Page Table */
+
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
-cap VNode_ARM_l2 {
-     /* L2 Page Table */
-     eq genpaddr base;         /* Base address of VNode */   
+cap VNode_ARM_l2 from RAM {
+    /* L2 Page Table */
+    address genpaddr base;  /* Base address of VNode */
+    size_bits { vnode_size };
 };
 
 /** IRQTable and IO are slightly different **/
 
-cap IRQTable {
-     /* IRQ Routing table */
-
-     /**
-        When testing two IRQTable caps for is_copy,
-       in kernel/mdb.c,
-
-       we always return True: all IRQ entries originate from a
-       single, primitive Cap. Grand'pa Cap, sort of.
-     **/
-
-     is_always_copy;
-
-     /* Empty payload*/
+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 IO {
-     /* Legacy IO capability */
-     eq uint16 start;
-     eq uint16 end;     /* Granted IO range */
+    /* Legacy IO capability */
+    eq uint16 start;
+    eq uint16 end;          /* Granted IO range */
 };
 
 /* really RCK notify caps */
@@ -308,9 +287,8 @@ cap BMPEndPoint {
     eq uint16 chanid;
 };
 
-cap BMPTable {
+cap BMPTable is_always_copy {
     /* BMP association table */
-    is_always_copy;
 };
 
 cap Domain {
@@ -318,6 +296,5 @@ cap Domain {
     eq uint32 domainid;
 };
 
-cap PerfMon {
-       is_always_copy;
+cap PerfMon is_always_copy {
 };