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 =