From 1a7ce5183b995fdd78350a9a8a21aec82e94efd3 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Wed, 3 Jul 2024 16:03:27 +1000 Subject: [PATCH] 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 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 --- README.md | 10 ++------ build_sdk.py | 9 +++++++ docs/manual.md | 21 ++++++++++++++-- libmicrokit/include/microkit.h | 2 ++ tool/microkit/src/main.rs | 29 ++++++++++++++++++++++ tool/microkit/src/sel4.rs | 44 +++++++++++++++++++++++++++++++++- tool/microkit/tests/test.rs | 1 + 7 files changed, 105 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 14e9893b5..5179ffc3f 100644 --- a/README.md +++ b/README.md @@ -186,6 +186,7 @@ The currently supported configurations are: * release * debug +* benchmark ## Supported Boards @@ -193,11 +194,4 @@ For documentation on each supported board see the [manual](https://github.com/se ## 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). diff --git a/build_sdk.py b/build_sdk.py index b3d19d553..da61871eb 100644 --- a/build_sdk.py +++ b/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" + }, + ), ) diff --git a/docs/manual.md b/docs/manual.md index 334de9fdb..2021d0d3c 100644 --- a/docs/manual.md +++ b/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). diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 66b86d2d9..2989404e3 100644 --- a/libmicrokit/include/microkit.h +++ b/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 diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 923fe6ff5..2214c6e0d 100644 --- a/tool/microkit/src/main.rs +++ b/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 { diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 36d1d9f49..6da6c130b 100644 --- a/tool/microkit/src/sel4.rs +++ b/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, diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 954261b1f..b399fe716 100644 --- a/tool/microkit/tests/test.rs +++ b/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 =