Add 'benchmark' configuration

This patch adds a new configuration for each platform called
'benchmark'.

The purpose of this is to enable Microkit systems to leverage the
benchmark configuration of seL4 that tracks things like kernel entries
and CPU utilisation. This also exports the PMU to user-space.

This is not ideal,
which is why [RFC-16](seL4/rfcs#22) exists.
However, we need to be able to do benchmarking for projects like the
seL4 Device Driver Framework in the meantime. It may take a while
to get the RFC approved and implemented which is why we are adding
this 'temporary' configuration.

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Author: Ivan-Velickovic

README.md

@@ -185,18 +185,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

@@ -187,6 +187,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

@@ -33,6 +33,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;
@@ -2058,6 +2059,30 @@ fn build_system(kernel_config: &Config,
         }));
     }
 
+    // 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 {
@@ -2499,6 +2524,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 {
@@ -584,6 +585,15 @@ 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, dest_depth, src_root, src_obj, src_depth, rights, badge } => {
                 arg_strs.push(Invocation::fmt_field("dest_index", dest_index));
                 arg_strs.push(Invocation::fmt_field("dest_depth", dest_depth));
@@ -628,7 +638,8 @@ impl Invocation {
             InvocationLabel::IrqSetIrqHandler => "IRQ Handler",
             InvocationLabel::ArmPageTableMap => "Page Table",
             InvocationLabel::ArmPageMap => "Page",
-            InvocationLabel::CnodeMint => "CNode",
+            InvocationLabel::CnodeMint |
+            InvocationLabel::CnodeCopy => "CNode",
             InvocationLabel::SchedControlConfigureFlags => "SchedControl",
             InvocationLabel::ArmVcpuSetTcb => "VCPU",
             _ => panic!("Internal error: unexpected label when getting object type '{:?}'", self.label)
@@ -649,6 +660,7 @@ impl Invocation {
             InvocationLabel::IrqSetIrqHandler => "SetNotification",
             InvocationLabel::ArmPageTableMap |
             InvocationLabel::ArmPageMap => "Map",
+            InvocationLabel::CnodeCopy => "Copy",
             InvocationLabel::CnodeMint => "Mint",
             InvocationLabel::SchedControlConfigureFlags => "ConfigureFlags",
             InvocationLabel::ArmVcpuSetTcb => "VCPUSetTcb",
@@ -672,6 +684,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,
             InvocationArgs::ArmVcpuSetTcb { .. } => InvocationLabel::ArmVcpuSetTcb,
@@ -728,6 +741,12 @@ impl InvocationArgs {
                                             vec![vspace]
                                         ),
             InvocationArgs::PageMap { page, vspace, vaddr, 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, dest_depth, src_root, src_obj, src_depth, rights, badge } =>
                                         (
                                             cnode,
@@ -822,6 +841,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: sysxml::PlatformDescription = sysxml::PlatformDescription::new(&DEFAULT_KERNEL_CONFIG);