Add 'benchmark' configuration

README.md

@@ -186,18 +186,12 @@ The currently supported configurations are:
 
 * release
 * debug
+* benchmark
 
 ## Supported Boards
 
 For documentation on each supported board see the [manual](https://github.com/seL4/microkit/blob/main/docs/manual.md#board-support-packages-bsps).
 
 ## Supported Configurations
 
-## Release
-
-In release configuration the loader, kernel and monitor do *not* perform any direct serial output.
-
-
-## Debug
-
-The debug configuration includes basic print output form the loader, kernel and monitor.
+For documentation on each supported board see the [manual](https://github.com/seL4/microkit/blob/main/docs/manual.md#configurations-config).

build_sdk.py

@@ -189,6 +189,15 @@ class ConfigInfo:
             "KernelVerificationBuild": False
         }
     ),
+    ConfigInfo(
+        name="benchmark",
+        debug=False,
+        kernel_options={
+            "KernelArmExportPMUUser": True,
+            "KernelDebugBuild": False,
+            "KernelBenchmarks": "track_utilisation"
+        },
+    ),
 )
 
 

docs/manual.md

@@ -313,8 +313,8 @@ handler via the `fault` entry point. It is then up to the parent to decide how t
 Microkit is distributed as a software development kit (SDK).
 
 The SDK includes support for one or more *boards*.
-Two *configurations* are supported for each board: *debug* and *release*.
-The *debug* configuration includes a debug build of the seL4 kernel to allow console debug output using the kernel's UART driver.
+Three *configurations* are supported for each board: *debug*, *release*, and *benchmark*.
+See [the Configurations section](#config) for more details.
 
 The SDK contains:
 
@@ -337,6 +337,23 @@ The Microkit tool should be invoked by the system build process to transform a s
 
 The ELF files provided as program images should be standard ELF files and have been linked against the provided libmicrokit.
 
+## Configurations {#config}
+
+## Debug
+
+The *debug* configuration includes a debug build of the seL4 kernel to allow console debug output using the kernel's UART driver.
+
+## Release
+
+The *release* configuration is a release build of the seL4 kernel and is intended for production builds. The loader, monitor, and
+kernel do *not* perform any serial output.
+
+## Benchmark
+
+The *benchmark* configuration uses a build of the seL4 kernel that exports the hardware's performance monitoring unit (PMU) to PDs.
+The kernel also tracks information about CPU utilisation. This benchmark configuration exists due a limitation of the seL4 kernel
+and is intended to be removed once [RFC-16 is implemented](https://github.com/seL4/rfcs/pull/22).
+
 ## System Requirements
 
 The Microkit tool requires Linux (x86-64), macOS (x86-64 or AArch64).

libmicrokit/include/microkit.h

@@ -16,6 +16,8 @@ typedef unsigned int microkit_child;
 typedef seL4_MessageInfo_t microkit_msginfo;
 
 #define MONITOR_EP 5
+/* Only valid in the 'benchmark' configuration */
+#define TCB_CAP 6
 #define BASE_OUTPUT_NOTIFICATION_CAP 10
 #define BASE_ENDPOINT_CAP 74
 #define BASE_IRQ_CAP 138

tool/microkit/src/main.rs

@@ -45,6 +45,7 @@ const FAULT_EP_CAP_IDX: u64 = 2;
 const VSPACE_CAP_IDX: u64 = 3;
 const REPLY_CAP_IDX: u64 = 4;
 const MONITOR_EP_CAP_IDX: u64 = 5;
+const TCB_CAP_IDX: u64 = 6;
 
 const BASE_OUTPUT_NOTIFICATION_CAP: u64 = 10;
 const BASE_OUTPUT_ENDPOINT_CAP: u64 = BASE_OUTPUT_NOTIFICATION_CAP + 64;
@@ -2337,6 +2338,33 @@ fn build_system(
         }));
     }
 
+    // In the benchmark configuration, we allow PDs to access their own TCB.
+    // This is necessary for accessing kernel's benchmark API.
+    if kernel_config.benchmark {
+        let mut tcb_cap_copy_invocation = Invocation::new(InvocationArgs::CnodeCopy {
+            cnode: cnode_objs[0].cap_addr,
+            dest_index: TCB_CAP_IDX,
+            dest_depth: PD_CAP_BITS,
+            src_root: root_cnode_cap,
+            src_obj: pd_tcb_objs[0].cap_addr,
+            src_depth: kernel_config.cap_address_bits,
+            rights: Rights::All as u64,
+        });
+        tcb_cap_copy_invocation.repeat(
+            system.protection_domains.len() as u32,
+            InvocationArgs::CnodeCopy {
+                cnode: 1,
+                dest_index: 0,
+                dest_depth: 0,
+                src_root: 0,
+                src_obj: 1,
+                src_depth: 0,
+                rights: 0,
+            },
+        );
+        system_invocations.push(tcb_cap_copy_invocation);
+    }
+
     // Set VSpace and CSpace
     let num_set_space_invocations = system.protection_domains.len() + virtual_machines.len();
     let mut set_space_invocation = Invocation::new(InvocationArgs::TcbSetSpace {
@@ -2894,6 +2922,7 @@ fn main() -> Result<(), String> {
         fan_out_limit: json_str_as_u64(&kernel_config_json, "RETYPE_FAN_OUT_LIMIT")?,
         arm_pa_size_bits: 40,
         hypervisor: json_str_as_bool(&kernel_config_json, "ARM_HYPERVISOR_SUPPORT")?,
+        benchmark: args.config == "benchmark",
     };
 
     match kernel_config.arch {

tool/microkit/src/sel4.rs

@@ -48,6 +48,7 @@ pub struct Config {
     pub fan_out_limit: u64,
     pub hypervisor: bool,
     pub arm_pa_size_bits: usize,
+    pub benchmark: bool,
 }
 
 pub enum Arch {
@@ -686,6 +687,23 @@ impl Invocation {
                 arg_strs.push(Invocation::fmt_field("attr", attr));
                 (page, cap_lookup.get(&page).unwrap().as_str())
             }
+            InvocationArgs::CnodeCopy {
+                cnode,
+                dest_index,
+                dest_depth,
+                src_root,
+                src_obj,
+                src_depth,
+                rights,
+            } => {
+                arg_strs.push(Invocation::fmt_field("dest_index", dest_index));
+                arg_strs.push(Invocation::fmt_field("dest_depth", dest_depth));
+                arg_strs.push(Invocation::fmt_field_cap("src_root", src_root, cap_lookup));
+                arg_strs.push(Invocation::fmt_field_cap("src_obj", src_obj, cap_lookup));
+                arg_strs.push(Invocation::fmt_field("src_depth", src_depth));
+                arg_strs.push(Invocation::fmt_field("rights", rights));
+                (cnode, cap_lookup.get(&cnode).unwrap().as_str())
+            }
             InvocationArgs::CnodeMint {
                 cnode,
                 dest_index,
@@ -759,7 +777,7 @@ impl Invocation {
             InvocationLabel::IrqSetIrqHandler => "IRQ Handler",
             InvocationLabel::ArmPageTableMap => "Page Table",
             InvocationLabel::ArmPageMap => "Page",
-            InvocationLabel::CnodeMint => "CNode",
+            InvocationLabel::CnodeCopy | InvocationLabel::CnodeMint => "CNode",
             InvocationLabel::SchedControlConfigureFlags => "SchedControl",
             InvocationLabel::ArmVcpuSetTcb => "VCPU",
             _ => panic!(
@@ -782,6 +800,7 @@ impl Invocation {
             InvocationLabel::ArmIrqIssueIrqHandlerTrigger => "Get",
             InvocationLabel::IrqSetIrqHandler => "SetNotification",
             InvocationLabel::ArmPageTableMap | InvocationLabel::ArmPageMap => "Map",
+            InvocationLabel::CnodeCopy => "Copy",
             InvocationLabel::CnodeMint => "Mint",
             InvocationLabel::SchedControlConfigureFlags => "ConfigureFlags",
             InvocationLabel::ArmVcpuSetTcb => "VCPUSetTcb",
@@ -810,6 +829,7 @@ impl InvocationArgs {
             InvocationArgs::IrqHandlerSetNotification { .. } => InvocationLabel::IrqSetIrqHandler,
             InvocationArgs::PageTableMap { .. } => InvocationLabel::ArmPageTableMap,
             InvocationArgs::PageMap { .. } => InvocationLabel::ArmPageMap,
+            InvocationArgs::CnodeCopy { .. } => InvocationLabel::CnodeCopy,
             InvocationArgs::CnodeMint { .. } => InvocationLabel::CnodeMint,
             InvocationArgs::SchedControlConfigureFlags { .. } => {
                 InvocationLabel::SchedControlConfigureFlags
@@ -924,6 +944,19 @@ impl InvocationArgs {
                 rights,
                 attr,
             } => (page, vec![vaddr, rights, attr], vec![vspace]),
+            InvocationArgs::CnodeCopy {
+                cnode,
+                dest_index,
+                dest_depth,
+                src_root,
+                src_obj,
+                src_depth,
+                rights,
+            } => (
+                cnode,
+                vec![dest_index, dest_depth, src_obj, src_depth, rights],
+                vec![src_root],
+            ),
             InvocationArgs::CnodeMint {
                 cnode,
                 dest_index,
@@ -1033,6 +1066,15 @@ pub enum InvocationArgs {
         rights: u64,
         attr: u64,
     },
+    CnodeCopy {
+        cnode: u64,
+        dest_index: u64,
+        dest_depth: u64,
+        src_root: u64,
+        src_obj: u64,
+        src_depth: u64,
+        rights: u64,
+    },
     CnodeMint {
         cnode: u64,
         dest_index: u64,

tool/microkit/tests/test.rs

@@ -17,6 +17,7 @@ const DEFAULT_KERNEL_CONFIG: sel4::Config = sel4::Config {
     fan_out_limit: 256,
     hypervisor: true,
     arm_pa_size_bits: 40,
+    benchmark: false,
 };
 
 const DEFAULT_PLAT_DESC: sdf::PlatformDescription =