Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for domain scheduling #175

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions build_sdk.py
Original file line number Diff line number Diff line change
Expand Up @@ -552,6 +552,7 @@ def main() -> None:
parser.add_argument("--skip-docs", action="store_true", help="Docs will not be built")
parser.add_argument("--skip-tar", action="store_true", help="SDK and source tarballs will not be built")
parser.add_argument("--version", default=VERSION, help="SDK version")
parser.add_argument("--experimental-domain-support", action="store_true", help="Enable experimental support for seL4's domain scheduler")

args = parser.parse_args()

Expand All @@ -577,6 +578,11 @@ def main() -> None:
else:
selected_configs = SUPPORTED_CONFIGS

if args.experimental_domain_support:
for config in selected_configs:
config.kernel_options["KernelNumDomains"] = 256
config.kernel_options["KernelDomainSchedule"] = Path("domain_schedule.c")

sel4_dir = args.sel4.expanduser()
if not sel4_dir.exists():
raise Exception(f"sel4_dir: {sel4_dir} does not exist")
Expand Down
24 changes: 24 additions & 0 deletions docs/manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,7 @@ This document attempts to clearly describe all of these terms, however as the co
* [notification](#notification)
* [interrupt](#irq)
* [fault](#fault)
* [domain scheduling](#domain)

## System {#system}

Expand Down Expand Up @@ -173,6 +174,10 @@ Runnable PDs of the same priority are scheduled in a round-robin manner.

The **passive** determines whether the PD is passive. A passive PD will have its scheduling context revoked after initialisation and then bound instead to the PD's notification object. This means the PD will be scheduled on receiving a notification, whereby it will run on the notification's scheduling context. When the PD receives a *protected procedure* by another PD or a *fault* caused by a child PD, the passive PD will run on the scheduling context of the callee.

#### Domain scheduling (experimental)

If the SDK is built with experimental domain support, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. Which domain is active at any given point in time is determined by the [domain schedule](#domain).

## Virtual Machine {#vm}

A *virtual machine* (VM) is a runtime abstraction for running guest operating systems in Microkit. It is similar
Expand Down Expand Up @@ -311,6 +316,10 @@ protection domain. The same applies for a virtual machine.
This means that whenever a fault is caused by a child, it will be delivered to the parent PD instead of the system fault
handler via the `fault` entry point. It is then up to the parent to decide how the fault is handled.

## Domain scheduling (experimental) {#domain}

Microkit can be built with experimental support for a method of temporally isolating different groups of PDs called domain scheduling. On a Microkit system, only one domain is active at a time, and the kernel alternates between domains according to a round-robin schedule. A domain schedule consists of an ordered list of domains, each with an associated length of time to run. The kernel will then activate a domain for the specified length of time; after that time has passed, it will deactivate that domain and activate the next domain for its length of time, and so on, proceeding through the list until it wraps back to the first domain. PDs are assigned to domains, such that when a certain domain is active, only PDs belonging to that domain will be scheduled to run.

# SDK {#sdk}

Microkit is distributed as a software development kit (SDK).
Expand Down Expand Up @@ -630,6 +639,7 @@ Within the `system` root element the following child elements are supported:
* `protection_domain`
* `memory_region`
* `channel`
* `domain_schedule` (if SDK is built with domain scheduling support)

## `protection_domain`

Expand All @@ -646,6 +656,7 @@ It supports the following attributes:
* `stack_size`: (optional) Number of bytes that will be used for the PD's stack.
Must be be between 4KiB and 16MiB and be 4K page-aligned. Defaults to 4KiB.
* `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform. Only available when the kernel has been configured with `KernelAllowSMCCalls`. Defaults to false.
* `domain`: (optional, experimental) Specifies the name of the scheduling domain the PD belongs to.

Additionally, it supports the following child elements:

Expand Down Expand Up @@ -736,6 +747,19 @@ The `end` element has the following attributes:
The `id` is passed to the PD in the `notified` and `protected` entry points.
The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions.

## `domain_schedule` (experimental)

The `domain_schedule` element has has a list of up to 256 `domain` child elements. Each child specifies information about a particular domain, and the order of the child elements specifies the order in which the domains will be scheduled.

The `domain` element has the following attributes:

* `name`: Name of the domain.
* `length`: Length of time the domain will run each time it is active, in microseconds.

The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element.

The `domain_schedule` element is only valid if the SDK is built with the `--experimental-domain-support` flag.

# Board Support Packages {#bsps}

This chapter describes the board support packages that are available in the SDK.
Expand Down
16 changes: 16 additions & 0 deletions domain_schedule.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
/*
* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/

/*
* This domain schedule is intended to be filled in via ELF patching
*/

#include <config.h>
#include <object/structures.h>
#include <model/statedata.h>

dschedule_t ksDomSchedule[256];
word_t ksDomScheduleLength;
36 changes: 35 additions & 1 deletion tool/microkit/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ const INIT_VSPACE_CAP_ADDRESS: u64 = 3;
const IRQ_CONTROL_CAP_ADDRESS: u64 = 4; // Singleton
const INIT_ASID_POOL_CAP_ADDRESS: u64 = 6;
const SMC_CAP_ADDRESS: u64 = 15;
const DOMAIN_CAP_ADDRESS: u64 = 11;

// const ASID_CONTROL_CAP_ADDRESS: u64 = 5; // Singleton
// const IO_PORT_CONTROL_CAP_ADDRESS: u64 = 7; // Null on this platform
Expand Down Expand Up @@ -895,6 +896,7 @@ fn build_system(
cap_address_names.insert(INIT_ASID_POOL_CAP_ADDRESS, "ASID Pool: init".to_string());
cap_address_names.insert(IRQ_CONTROL_CAP_ADDRESS, "IRQ Control".to_string());
cap_address_names.insert(SMC_CAP_IDX, "SMC".to_string());
cap_address_names.insert(DOMAIN_CAP_ADDRESS, "Domain Cap".to_string());

let system_cnode_bits = system_cnode_size.ilog2() as u64;

Expand Down Expand Up @@ -2699,6 +2701,19 @@ fn build_system(
system_invocations.push(tcb_cap_copy_invocation);
}

for (pd_idx, pd) in system.protection_domains.iter().enumerate() {
if let Some(domain_id) = pd.domain_id {
system_invocations.push(Invocation::new(
config,
InvocationArgs::DomainSetSet {
domain_set: DOMAIN_CAP_ADDRESS,
domain: domain_id as u8,
tcb: pd_tcb_objs[pd_idx].cap_addr,
},
));
}
}

// Set VSpace and CSpace
let mut pd_set_space_invocation = Invocation::new(
config,
Expand Down Expand Up @@ -3345,6 +3360,7 @@ fn main() -> Result<(), String> {
arm_pa_size_bits,
arm_smc,
riscv_pt_levels: Some(RiscvVirtualMemory::Sv39),
domain_scheduler: json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")? != 1,
};

if let Arch::Aarch64 = kernel_config.arch {
Expand Down Expand Up @@ -3378,9 +3394,27 @@ fn main() -> Result<(), String> {
system_invocation_count_symbol_name: "system_invocation_count",
};

let kernel_elf = ElfFile::from_path(&kernel_elf_path)?;
let mut kernel_elf = ElfFile::from_path(&kernel_elf_path)?;
let mut monitor_elf = ElfFile::from_path(&monitor_elf_path)?;

if let Some(domain_schedule) = &system.domain_schedule {
let schedule = &domain_schedule.schedule;
kernel_elf.write_symbol(
"ksDomScheduleLength",
&(schedule.len() as u64).to_le_bytes(),
)?;

let mut out = Vec::new();
out.reserve_exact(schedule.len() * 16);
JE-Archer marked this conversation as resolved.
Show resolved Hide resolved

for timeslice in schedule.iter() {
out.extend(timeslice.id.to_le_bytes());
out.extend(timeslice.length.to_le_bytes());
}

kernel_elf.write_symbol("ksDomSchedule", &out)?;
}

if monitor_elf.segments.iter().filter(|s| s.loadable).count() > 1 {
eprintln!(
"Monitor ({}) has {} segments, it must only have one",
Expand Down
Loading
Loading